search

moves-rwth / storm

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

Export probabilities / expected rewards for all states for properties with `=?` #526

Closed linusheck closed 2 months ago

linusheck commented 2 months ago

I was wondering whether it's possible to export the values for all states in a simple sparse model checking query (i.e., the result vector). I haven't found an option to do so. If it's currently not possible, I might implement it.

volkm commented 2 months ago

Does it have to be from the commandline? Stormpy supports obtaining the result vector.

linusheck commented 2 months ago

It's good to know this is possible in stormpy, then I can solve my immediate problem :) I think it's still a good idea to add a command line option for this though, I can take a look at it.

tquatmann commented 2 months ago

Yes, this is possible, but the command line is a bit clumsy (of course):

storm --prism ~/git/qcomp/benchmarks/dtmc/crowds/crowds.prism -const TotalRuns=3,CrowdSize=4 --prop 'filter(values, P=? [ F (observe0 > 1)], true)' --exportresult result.json

Notice the filter(values, ... , true) around the property, which tells Storm that we are interested in the values for all states that satisfy true. Then, the --exportresult result.json creates a json file. You can also replace true by any other PCTL-like formula (that evaluates to something Boolean) which will then store the result only for those states where the formula evaluates to true. You can also add --buildstateval for more information of the state space in the result.json file.

linusheck commented 2 months ago

Thanks! I guess this issue works as documentation on how to do this, if someone is also searching.