Running parametric model on Docker

[anirjoshi]

Hello, I am trying to run storm on parametric models. I am using Storm on a Docker from the instructions mentioned here. However when I try to follow the instructions listed here to run a parametric model, I get an issue.

On running the command: ./storm-pars --mode feasibility --feasibility:method pla --prism brp.pm --prop 'P<=0.01 [F s=5]' --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9"

I get the following issue:

Storm-pars 1.8.1

Date: Mon Aug 12 08:43:00 2024
Command line arguments: --mode feasibility '--feasibility:method' pla --prism ./brp.pm --prop 'P<=0.01 [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9'
Current working directory: /opt/storm/build/bin

ERROR (SettingsManager.cpp:116): Unknown option '--mode'. Did you mean '--sigmode'?

##### Suggested options:
--[bisimulation:]sigmode <mode> Sets the signature computation mode. <mode> (in {eager, lazy}; default: eager): The mode to use.

ERROR (cli.cpp:182): Unable to parse command line options. Type './storm-pars --help' or './storm-pars --help all' for help.

By changing the --mode option to --sigmode, I get the following command: ./storm-pars --sigmode feasibility --feasibility:method pla --prism ./brp.pm --prop 'P<=0.01 [F s=5]' --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9"

Here I get the following issue:

Storm-pars 1.8.1

Date: Mon Aug 12 08:44:28 2024
Command line arguments: --sigmode feasibility '--feasibility:method' pla --prism ./brp.pm --prop 'P<=0.01 [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9'
Current working directory: /opt/storm/build/bin

ERROR (SettingsManager.cpp:504): Value 'feasibility' is invalid for argument <mode> of option:
--[bisimulation:]sigmode <mode> Sets the signature computation mode. <mode> (in {eager, lazy}; default: eager): The mode to use.
ERROR (cli.cpp:182): Unable to parse command line options. Type './storm-pars --help' or './storm-pars --help all' for help.

[sjunges]

Hey,

this is indeed a bit unfortunate. We are in the progress of updating our support for parametric engines and updated the website to reflect the HEAD in preparation of our upcoming release.

The suggested solution would be to use docker pull movesrwth/storm:ci which reflects the latest version of Storm.

Personally, I think we should even recommend using docker pull movesrwth/stormpy:ci as it includes the python bindings, in case that becomes relevant for you.

[anirjoshi]

Hello @sjunges, thank you for the quick response. The command ./storm-pars --mode feasibility --feasibility:method pla --prism brp.pm --prop 'P<=0.01 [F s=5]' --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9" now seems to run. However the output does not match the expected output in the tutorial here. The output that I get is:

Storm-pars 1.8.2 (dev)

Date: Mon Aug 12 09:27:27 2024
Command line arguments: --mode feasibility '--feasibility:method' pla --prism brp.pm --prop 'P<=0.01 [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9'
Current working directory: /opt/storm/build/bin

Time for model input parsing: 0.053s.

Time for model construction: 0.153s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     351
Transitions:    788
Reward Models:  none
State Labels:   3 labels
   * deadlock -> 10 item(s)
   * init -> 1 item(s)
   * (s = 5) -> 36 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Time for model simplification: 0.009s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     70
Transitions:    345
Reward Models:  none
State Labels:   4 labels
   * (s = 5) -> 1 item(s)
   * deadlock -> 1 item(s)
   * target -> 1 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 

Time for model preprocessing: 0.010s.

-------------------------------------------------------------- 
Model type:     DTMC (sparse)
States:     70
Transitions:    345
Reward Models:  none
State Labels:   4 labels
   * (s = 5) -> 1 item(s)
   * deadlock -> 1 item(s)
   * target -> 1 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 
Find feasible solution for  P=? [F (s = 5)] within region 1/10<=pL<=9/10,1/10<=pK<=9/10;
Result at initial state: 4359708261538689/576460752303423488 ( approx. 0.00756288827) at [pL=2/5, pK=4/5].
Time for model checking: 0.032s.