search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
138 stars 75 forks source link

Two Monotonicity Bugfixes #632

Closed SvStein closed 3 days ago

SvStein commented 1 week ago
  1. Bug: Not all states were added to the order properly when using PLA bounds. They were simply set to done when all their successors could be ordered via PLA bounds, but not put into the order. They were at best only added trivially (between top and bottom) when required later as another state's successor. These states are now no longer set to done so that the main loop will still consider them and integrate them into the order properly.
  2. Bug: The zeroconf benchmark only resulted in no increasing parameter (with PLA) or one increasing parameter (without PLA), whereas the correct (and previously attained) result is that both parameters are increasing. The order was correct and did lend itself to concluding the correct result but local monotonicity was not checked at all states, specifically not those from the statesToHandle vector (whose purpose is currently unclear). This restriction was now lifted so that local monotonicity is checked on these too if the order has been expanded with them.
linusheck commented 4 days ago

LGTM. Am I allowed to just merge it @tquatmann ? :)