diff --git a/prism-tests/functionality/verify/sim/chain.prism b/prism-tests/functionality/verify/sim/chain.prism new file mode 100644 index 00000000..c7f3c5f0 --- /dev/null +++ b/prism-tests/functionality/verify/sim/chain.prism @@ -0,0 +1,17 @@ +// Completely deterministic model +// used to do some sanity checks on statistical model checking + +dtmc + +const int N = 10; + +module M + + x : [0..N]; + + [] x (x'=x+1); + [] x=N -> true; + +endmodule + +label "end" = x=N; diff --git a/prism-tests/functionality/verify/sim/chain.prism.props b/prism-tests/functionality/verify/sim/chain.prism.props new file mode 100644 index 00000000..0daa4b22 --- /dev/null +++ b/prism-tests/functionality/verify/sim/chain.prism.props @@ -0,0 +1,15 @@ +const int K = 0; + +label "not_end" = x