Access parametric model checking via Eclipse/Java

[Kenneth Johnson]

Dear Prism Model Checking Group:

I am having some problems invoking Prism's parametric model-checking functionality through Eclipse.

I have Prism 4.7 installed and can invoke standard model checking to obtain e.g. probability values etc by adding the appropriate JAR file dependencies to the Eclipse project.

However, when I try parametric model checking, (via the main method below), it returns the exception

Exception in thread "main" java.lang.NullPointerException: Cannot invoke "parser.Values.removeValue(String)" because "<local7>" is null
at prism.Prism.modelCheckParametric(Prism.java:3448)
at parametric.ParametricTestClient.main(ParametricTestClient.java:60)

But when I run parametric model checking by the command line, it returns the expected output (below)

Thank you for your help!

Best regards

Ken

prism simple.pm simple.pctl -param 'p1=0.0:1.0,p2=0.0:1.0'

 --------

Parametric model checking: P=? [ F (state=3) ]

Building model (parametric engine)...

Computing reachable states...
Reachable states exploration and model construction done in 0.007 secs.

States:      4 (1 initial)
Transitions: 6

Time for model construction: 0.008 seconds.

Time for model checking: 0.023 seconds.

Result (probability): ([0.0,1.0],[0.0,1.0]): { ( -1 ) p2 * p1 + 1  }


public static void main(String[] args)
{

Prism prism = null;
PrismLog prismMainLog;
prismMainLog = new PrismFileLog("prismLogFile.txt");
prism = new Prism(prismMainLog);

String fileContents = "dtmc\n"
+ "const double p1;\n"
+ "const double p2;\n"
+ "module simple\n"
+ "    state : [0..3] init 0;\n"
+ "    [action1] (state=0) -> p1:(state'=1) + (1-p1):(state'=3);\n"
+ "    [action2] (state=1) -> p2:(state'=2) + (1-p2):(state'=3);\n"
+ "    [fail] (state=3) -> true;\n"
+ "endmodule\n";

try {
prism.initialise();
String[] paramNames = new String[]{"p1","p2"};
String[] paramLowerBounds = new String[]{"0","0"};
String[] paramUpperBounds = new String[]{"1","1"};

ModulesFile modulesFile = prism.parseModelString(fileContents);
prism.loadPRISMModel(modulesFile);
PropertiesFile propertiesFile = prism.parsePropertiesString(modulesFile,"P=?[F(state=3)]");

prism.Result fromPrismResult = prism.modelCheckParametric(propertiesFile,propertiesFile.getPropertyObject(0),
paramNames, paramLowerBounds, paramUpperBounds);

System.out.println(fromPrismResult);

} catch (PrismException e)
{
e.printStackTrace();
}
}

[Dave Parker]

Hi Kenneth,

For the parametric case, you need to tell PRISM to initialise constants,
even when they are all being left as parameters. Add:

prism.setPRISMModelConstants(null, true);

after your line:

prism.loadPRISMModel(modulesFile);

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker/f7a8735c-2a8b-4122-b72a-3032b008d5dbn%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/f7a8735c-2a8b-4122-b72a-3032b008d5dbn%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Kenneth Johnson]

Hi Dave -- thank you for your quick reply -- It works now, after adding the jas and log4j jar files to my dependencies

Thank you!

Ken

[Kenneth Johnson]

Hi all, 

Just following up on this query. Is there a standard way to evaluate expressions obtained from parametric model checking?

I have checked on the Java Algebra System website, but I haven't found something I could use to supply values to variables and evaluate the expression.

Currently, I am doing this slightly ad-hoc, e.g. changing the expression ( -1 ) p * q + p + q to ( -1 )*p * q + p + q and evaluating with ScriptEngine. 

Best regards

Ken

[Dave Parker]

Hi Ken,

Yes, you should be able to do this programmatically (but it's a bit
involved). The result field of the Result object returned by model
checking will contain a ParamResult object in this case. That contains a
RegionValues object, which is map from regions of the parameter space to
the corresponding symbolic expressions representing the result. The
latter is given for all states so is in a StateValues object. You can
access the expression for the initial state with
getValue(model.getFirstInitialState()), which is a Function object.
Then, finally, you can evaluate that, passing a Point object which
contains the parameter values.

Hope that helps!

Best wishes,

Dave

> > prism simple.pm <http://simple.pm> simple.pctl -param

> https://groups.google.com/d/msgid/prismmodelchecker/f7a8735c-2a8b-4122-b72a-3032b008d5dbn%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/f7a8735c-2a8b-4122-b72a-3032b008d5dbn%40googlegroups.com> <https://groups.google.com/d/msgid/prismmodelchecker/f7a8735c-2a8b-4122-b72a-3032b008d5dbn%40googlegroups.com?utm_medium=email&utm_source=footer <https://groups.google.com/d/msgid/prismmodelchecker/f7a8735c-2a8b-4122-b72a-3032b008d5dbn%40googlegroups.com?utm_medium=email&utm_source=footer>>.

>
> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchec...@googlegroups.com
> <mailto:prismmodelchec...@googlegroups.com>.
> To view this discussion on the web, visit

> https://groups.google.com/d/msgid/prismmodelchecker/9e21a2ef-8d38-4f5d-bb46-e8df907f5c27n%40googlegroups.com <https://groups.google.com/d/msgid/prismmodelchecker/9e21a2ef-8d38-4f5d-bb46-e8df907f5c27n%40googlegroups.com?utm_medium=email&utm_source=footer>.