Exact arithmetic tests for both MDPs and DTMCs.

functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm

@@ -0,0 +1,52 @@
+// optimal program for the sum of two dice
+
+dtmc
+
+module sum_of_two_dice
+
+	// local state
+	s : [0..34] init 0;
+	// total of two dice
+	d : [0..12] init 0;
+
+	[] s=0  -> 0.5 : (s'=1)  + 0.5 : (s'=2);
+	[] s=1  -> 0.5 : (s'=3)  + 0.5 : (s'=4);
+	[] s=2  -> 0.5 : (s'=5)  + 0.5 : (s'=6);
+	[] s=3  -> 0.5 : (s'=7)  + 0.5 : (s'=34) & (d'=6);
+	[] s=4  -> 0.5 : (s'=8)  + 0.5 : (s'=34) & (d'=7);
+	[] s=5  -> 0.5 : (s'=9)  + 0.5 : (s'=34) & (d'=8);
+	[] s=6  -> 0.5 : (s'=10) + 0.5 : (s'=11);
+	[] s=7  -> 0.5 : (s'=12) + 0.5 : (s'=34) & (d'=4);
+	[] s=8  -> 0.5 : (s'=13) + 0.5 : (s'=34) & (d'=5);
+	[] s=9  -> 0.5 : (s'=14) + 0.5 : (s'=34) & (d'=9);
+	[] s=10 -> 0.5 : (s'=15) + 0.5 : (s'=34) & (d'=10);
+	[] s=11 -> 0.5 : (s'=16) + 0.5 : (s'=17);
+	[] s=12 -> 0.5 : (s'=18) + 0.5 : (s'=34) & (d'=3);
+	[] s=13 -> 0.5 : (s'=19) + 0.5 : (s'=34) & (d'=5);
+	[] s=14 -> 0.5 : (s'=20) + 0.5 : (s'=34) & (d'=7);
+	[] s=15 -> 0.5 : (s'=21) + 0.5 : (s'=34) & (d'=9);
+	[] s=16 -> 0.5 : (s'=22) + 0.5 : (s'=34) & (d'=11);
+	[] s=17 -> 0.5 : (s'=23) + 0.5 : (s'=24);
+	[] s=18 -> 0.5 : (s'=25) + 0.5 : (s'=34) & (d'=2);
+	[] s=19 -> 0.5 : (s'=26) + 0.5 : (s'=34) & (d'=3);
+	[] s=20 -> 0.5 : (s'=27) + 0.5 : (s'=34) & (d'=4);
+	[] s=21 -> 0.5 : (s'=34) & (d'=5) + 0.5 : (s'=34) & (d'=9);
+	[] s=22 -> 0.5 : (s'=28) + 0.5 : (s'=34) & (d'=10);
+	[] s=23 -> 0.5 : (s'=29) + 0.5 : (s'=34) & (d'=11);
+	[] s=24 -> 0.5 : (s'=30) + 0.5 : (s'=34) & (d'=12);
+	[] s=25 -> 0.5 : (s'=1)  + 0.5 : (s'=34) & (d'=2);
+	[] s=26 -> 0.5 : (s'=31) + 0.5 : (s'=34) & (d'=3);
+	[] s=27 -> 0.5 : (s'=32) + 0.5 : (s'=34) & (d'=6);
+	[] s=28 -> 0.5 : (s'=34) & (d'=7) + 0.5 : (s'=34) & (d'=8);
+	[] s=29 -> 0.5 : (s'=33) + 0.5 : (s'=34) & (d'=11);
+	[] s=30 -> 0.5 : (s'=2)  + 0.5 : (s'=34) & (d'=12);
+	[] s=31 -> 0.5 : (s'=34) & (d'=2) + 0.5 : (s'=34) & (d'=4);
+	[] s=32 -> 0.5 : (s'=34) & (d'=6) + 0.5 : (s'=34) & (d'=8);
+	[] s=33 -> 0.5 : (s'=34) & (d'=10) + 0.5 : (s'=34) & (d'=12);
+	[] s=34 -> (s'=34);
+
+endmodule
+
+rewards "coin_flips"
+	[] s<34 : 1;
+endrewards

functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props

@@ -0,0 +1,29 @@
+// RESULT: 1/9
+P=? [ F d=5 ];
+
+// RESULT: 4/21
+filter(state, P=?[F d = 5], s=1)
+
+// RESULT: 1/168
+filter(state, P=?[F d = 5], s=3)
+
+// RESULT: 0.375
+filter(state, P=?[F d = 5], s=4)
+
+// RESULT: 2/21
+filter(state, P=?[F d = 5], s=25)
+
+// RESULT: 0
+P=? [ F d=37 ];
+
+// RESULT: 1/12
+P=? [ F d=10 ];
+
+// RESULT: 1/4
+filter(state, P=? [F d=10], s=29)
+
+// RESULT: 1/2
+filter(state, P=? [F d=10], s=10)
+
+// RESULT: 1
+filter(state, P=? [F d=0], s=0)

functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props.args

@@ -0,0 +1 @@
+-s -m -h -ex -exact-lp -precision 128

functionality/verify/mdps/exact-arithmetic/cert-example.nm

@@ -0,0 +1,11 @@
+mdp
+
+module main
+
+x: [0..13] init 0;
+
+[] (x!=3) & (x!=13) & (x!=2) -> 0.5:(x'=x+1) + 0.5:(x'=3);
+[] (x=2) -> 0.5:(x'=4) + 0.5:(x'=3);
+[] (x=3) | (x=13) -> (x'=x);
+
+endmodule

functionality/verify/mdps/exact-arithmetic/cert-example.nm.props

@@ -0,0 +1,41 @@
+// RESULT: 1
+Pmax=? [ F x=0 ];
+
+// RESULT: 1/4096
+Pmax=? [ F x=13 ];
+
+// RESULT: 1/2048
+filter(state, Pmax=? [ F x=13 ], x=1);
+
+// RESULT: 1/1024
+filter(state, Pmax=? [ F x=13 ], x=2);
+
+// RESULT: 1/512
+filter(state, Pmax=? [ F x=13 ], x=4);
+
+// RESULT: 1/256
+filter(state, Pmax=? [ F x=13 ], x=5);
+
+// RESULT: 1/128
+filter(state, Pmax=? [ F x=13 ], x=6);
+
+// RESULT: 1/64
+filter(state, Pmax=? [ F x=13 ], x=7);
+
+// RESULT: 1/32
+filter(state, Pmax=? [ F x=13 ], x=8);
+
+// RESULT: 1/16
+filter(state, Pmax=? [ F x=13 ], x=9);
+
+// RESULT: 1/8
+filter(state, Pmax=? [ F x=13 ], x=10);
+
+// RESULT: 1/4
+filter(state, Pmax=? [ F x=13 ], x=11);
+
+// RESULT: 1/2
+filter(state, Pmax=? [ F x=13 ], x=12);
+
+// RESULT: 1
+filter(state, Pmax=? [ F x=13 ], x=13

functionality/verify/mdps/exact-arithmetic/cert-example.nm.props.args

@@ -0,0 +1 @@
+-s -m -h -ex -exact-lp -exportadv cert_example.tra -precision 128

functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm

@@ -0,0 +1,21 @@
+// Simple MDP example for testing exact arithmetic
+// The expected results are of the form (2^(k-1) + 1) / 2^k for 0<k<n
+
+mdp
+
+const int n = 10;
+
+module main
+
+x : [0..2*n] init n;
+
+[] x=n -> 0.5:(x'=n-1) + 0.5:(x'=n+1);
+[] x>0 & x<n -> 0.5:(x'=x-1) + 0.5:(x'=n);
+[] x>n & x<2*n -> 0.5:(x'=x+1) + 0.5:(x'=n);
+[] x=0 | x=2*n -> 1.0:(x'=x);
+
+endmodule
+
+rewards
+  true : 1;
+endrewards

functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props

@@ -0,0 +1,41 @@
+// RESULT: 1/2
+Pmax=? [ F x=0 ];
+
+// RESULT: 1/2
+Pmin=? [ F x=0 ];
+
+// RESULT: 3/4
+filter(max, Pmax=? [ F x=0 ], x=1)
+
+// RESULT: 1/4
+filter(max, Pmax=? [ F x=0 ], x=19)
+
+// RESULT: 1/2
+filter(max, Pmax=? [ F x=10 ], x=19)
+
+// RESULT: 2/3
+Pmax=? [ F x=1 ];
+
+// RESULT: 1
+Pmax=? [ F x=10 ];
+
+// RESULT: 1/2
+Pmax=? [ F x=20 ];
+
+// RESULT: 3/4
+filter(state, Pmax=? [F x=10], x=2);
+
+// RESULT: 7/8
+filter(state, Pmax=? [F x=10], x=3);
+
+// RESULT: 15/16
+filter(state, Pmax=? [F x=10], x=4);
+
+// RESULT: 511/512
+filter(state, Pmax=? [F x=10], x=11);
+
+// RESULT: 31/32
+filter(state, Pmax=? [F x=10], x=15);
+
+// RESULT: 0
+filter(state, Pmax=? [F x=10], x=20);

functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props.args

@@ -0,0 +1 @@
+-s -m -h -ex -exact-lp -exportadv mdp_exact10.tra -precision 128