prismmodelchecker / prism

The main development version of the PRISM model checker.
http://www.prismmodelchecker.org/
GNU General Public License v2.0
157 stars 73 forks source link

Parametric model-checking with many parameters #213

Closed carlhenrikrolf closed 1 year ago

carlhenrikrolf commented 1 year ago

I am trying to perform parametric model-checking, where each transition has a confidence interval. According to the manual, it is only possible to input these confidence intervals through the command line, i.e.

prism model.prism constraints.props -param p0_0=lb0_0:ub0_0,...,pn_n=lbn_n:ubn_n

where lb is the lower bound and ub is upper bound on the confidence interval. This works for very small Markov chains, but the number of parameters grow quickly, which leads to the bash error Argument list too long. I wonder if there is a workaround for this problem. For example, is there an extension that allows you to load the parameters as a file instead? Or, can it be solved by using, for example, Storm(py)?

davexparker commented 1 year ago

(resolved offline)