Unify value function

[Zinoex]

Until now, we had a separate value function for reach-avoid and for reward specifications (for each model type), which was a violation of DRY and more unmaintainable. With the introduction of the postprocess! function (called immediately after a value iteration step) in this PR, we can unify the two types of value functions (still separate for each model) and reduce the copies of the value iteration to maintain.

postprocess! does the following:

• For reachability, it assigns the reach set the value of 1.
• For reach-avoid, it assigns the reach set the value of 1 and the avoid set the value of 0.
• For a reward specification, it multiplies the current reward with the discount factor and adds the stepwise reward (in that order).

An additional benefit of this approach is that we decouple the specification and the system (again), since it no longer requires that the terminal set for reachability/reach-avoid only has a loop to itself (simplifying the safety checks introduced in #34).

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 74.30%. Comparing base (9ebafb7) to head (84a97b3).

❗ Current head 84a97b3 differs from pull request most recent head 3f95d73. Consider uploading reports for the commit 3f95d73 to get more accurate results

Additional details and impacted files

@@            Coverage Diff             @@
##             main      #36      +/-   ##
==========================================
- Coverage   75.00%   74.30%   -0.70%     
==========================================
  Files          20       20              
  Lines        1476     1413      -63     
==========================================
- Hits         1107     1050      -57     
+ Misses        369      363       -6     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[jmskov]

Works as expected and changes are clean.