storm icon indicating copy to clipboard operation
storm copied to clipboard

Scheduler export warning confusion

Open sjunges opened this issue 2 years ago • 0 comments

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.

sjunges avatar Jul 28 '22 12:07 sjunges