moves-rwth / storm

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

Added `--permute` option to re-order the states after building. #537

Closed tquatmann closed 1 month ago

tquatmann commented 1 month ago

This is useful to, e.g., investigate how much algorithm performance is affected by the order of the states.

Example:



$ ./storm --qvbsroot ~/git/qcomp/benchmarks --qvbs consensus 5 steps_min  --permute bfs   | grep "Time for model checking" -B1
Result (for initial states): 768.0679927
Time for model checking: 0.201s.

$ ./storm --qvbsroot ~/git/qcomp/benchmarks --qvbs consensus 5 steps_min  --permute reverse-bfs   | grep "Time for model checking" -B1
Result (for initial states): 768.0918665
Time for model checking: 0.861s.

$  ./storm --qvbsroot ~/git/qcomp/benchmarks --qvbs consensus 5 steps_min  --permute random 1234   | grep "Time for model checking" -B1
Result (for initial states): 768.0830197
Time for model checking: 0.394s.
sjunges commented 1 month ago

LGTM, very cool functionality :-)