search

moves-rwth / storm

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

Monotonicity analysis - Dot file generation #147

Closed Sara-Iftikhar closed 2 years ago

Sara-Iftikhar commented 2 years ago

I have a DTMC model. I want to do monotonicity analysis of my model and want to generate the dot output file. By following this link, I am using the cammand;

$ storm-pars --prism model.prism --monotonicity-analysis --bisimulation --mon:dotOutput

But I am unable to find the resultant file anywhere in my path, even if I provide the file name.

Please correct me if I am making a mistake in the command.

jipspel commented 2 years ago

Thanks for your question! In your command the property and region are missing. The property is needed to compute the =) and =( states, the region is needed to check for the monotonicity. See also this link

sjunges commented 2 years ago

I assume that this issue has been solved. If not, feel free to reopen.