storm
storm copied to clipboard
Scheduler export warning confusion
In the following example, storm warns that only partial choice information even thoug both suggested options are available.
Command line arguments: --prism examples/grid_slip_forward.prism -const N=8 --prop 'Pmax=? [GF "station" ]' '--io:exportscheduler' sched.json --buildchoicelab --buildchoiceorig
...
Model checking property "1": Pmax=? [G F "station"] ...
Exporting scheduler ... WARN (model-handling.h:1133): No information of state valuations available. The scheduler output will use internal state ids. You might be interested in building the model with state valuations using --buildstateval.
WARN (model-handling.h:1140): Only partial choice information is available. You might want to build the model with choice origins using --buildchoicelab or --buildchoiceorig.
Write to file sched.json.