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.

[linusheck]

However the output does not match the expected output in the tutorial here.

It seems that the exact brp model differs, as the number of states is different (351 states in your case and 135 states in the tutorial). Otherwise the outputs seem very similar to me. Where did you get the brp.pm model?

[anirjoshi]

Hi, @linusheck Its been quiet some time since I've used this tool. But I believe I just followed the instructions to install and test the Docker. I've described it in the first post on this thread https://github.com/moves-rwth/storm/issues/592#issue-2460390189. Please let me know if this is enough, and any additional information is required, I can perhaps try to dig that up.

[linusheck]

I didn't realize the issue is super old, sorry! Then I guess we can close it? Were you successful?

[anirjoshi]

Hi, it looks like according to the latest comment [aug-2024] the output of the tool did not match the expected output as mentioned https://github.com/moves-rwth/storm/issues/592#issuecomment-2283499725. I believed it remained unresolved, and I used some other method for solving my problem and did not end up using the tool.

[linusheck]

Hi, I'm not sure what you mean with

the output of the tool did not match the expected output as mentioned

in which sense did it not match the expected output?

[sjunges]

If the difference is just that another file was used, then I think we can close the issue :-)