diff --git a/prism-tests/functionality/verify/param/param-simple.prism b/prism-tests/functionality/verify/param/param-simple.prism new file mode 100644 index 00000000..e4d5fbf9 --- /dev/null +++ b/prism-tests/functionality/verify/param/param-simple.prism @@ -0,0 +1,16 @@ +// Trivial test of parametric model checking +// (also tests a bugfix in the results testing when the result is just a lone parameter) + +dtmc + +const double p; + +module M + + // local state + s : [0..7] init 0; + + [] s=0 -> p : (s'=1) + 1-p : (s'=2); + [] s>0 -> true; + +endmodule diff --git a/prism-tests/functionality/verify/param/param-simple.prism.props b/prism-tests/functionality/verify/param/param-simple.prism.props new file mode 100644 index 00000000..0ed5ab32 --- /dev/null +++ b/prism-tests/functionality/verify/param/param-simple.prism.props @@ -0,0 +1,5 @@ +// RESULT: p +P=? [ F s=1 ]; + +// RESULT: 1-p +P=? [ F s=2 ]; diff --git a/prism-tests/functionality/verify/param/param-simple.prism.props.args b/prism-tests/functionality/verify/param/param-simple.prism.props.args new file mode 100644 index 00000000..7210805c --- /dev/null +++ b/prism-tests/functionality/verify/param/param-simple.prism.props.args @@ -0,0 +1 @@ +-param p diff --git a/prism/src/param/ParamResult.java b/prism/src/param/ParamResult.java index 931dff01..5e738f86 100644 --- a/prism/src/param/ParamResult.java +++ b/prism/src/param/ParamResult.java @@ -148,7 +148,7 @@ public class ParamResult for (String p : modelBuilder.getParameterNames()) { constantList.addConstant(new ExpressionIdent(p), null, TypeDouble.getInstance()); } - exprExpected.findAllConstants(constantList); + exprExpected = (Expression) exprExpected.findAllConstants(constantList); exprExpected.typeCheck(); // replace constants in the expression that have a value