diff --git a/prism-tests/functionality/verify/param/param-consts.prism b/prism-tests/functionality/verify/param/param-consts.prism new file mode 100644 index 00000000..58206c5d --- /dev/null +++ b/prism-tests/functionality/verify/param/param-consts.prism @@ -0,0 +1,18 @@ +// Test of constants in parametric model checking +// (specifically, when a parameter is used indirectly, +// within the definition of another constant) + +dtmc + +const double p; +const double q = 1 - p; + +module M + + // local state + s : [0..7] init 0; + + [] s=0 -> q : (s'=1) + 1-q : (s'=2); + [] s>0 -> true; + +endmodule diff --git a/prism-tests/functionality/verify/param/param-consts.prism.props b/prism-tests/functionality/verify/param/param-consts.prism.props new file mode 100644 index 00000000..c38b46ce --- /dev/null +++ b/prism-tests/functionality/verify/param/param-consts.prism.props @@ -0,0 +1,5 @@ +// RESULT: 1-p +P=? [ F s=1 ]; + +// RESULT: p +P=? [ F s=2 ]; diff --git a/prism-tests/functionality/verify/param/param-consts.prism.props.args b/prism-tests/functionality/verify/param/param-consts.prism.props.args new file mode 100644 index 00000000..7210805c --- /dev/null +++ b/prism-tests/functionality/verify/param/param-consts.prism.props.args @@ -0,0 +1 @@ +-param p