From fe7e39923977e33626ae1b4f11278261a78699a5 Mon Sep 17 00:00:00 2001 From: nicodelpiano Date: Wed, 29 Jun 2016 12:02:17 -0300 Subject: [PATCH 1/2] Exact arithmetic tests for both MDPs and DTMCs. --- .../dtmcs/exact-arithmetic/two_dice_knuth.pm | 52 +++++++++++++++++++ .../exact-arithmetic/two_dice_knuth.pm.props | 29 +++++++++++ .../two_dice_knuth.pm.props.args | 1 + .../mdps/exact-arithmetic/mdp_exact10.nm | 21 ++++++++ .../exact-arithmetic/mdp_exact10.nm.props | 41 +++++++++++++++ .../mdp_exact10.nm.props.args | 1 + 6 files changed, 145 insertions(+) create mode 100644 functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm create mode 100644 functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props create mode 100644 functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props.args create mode 100644 functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm create mode 100644 functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props create mode 100644 functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props.args diff --git a/functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm b/functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm new file mode 100644 index 0000000..7aff1bf --- /dev/null +++ b/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 diff --git a/functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props b/functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props new file mode 100644 index 0000000..07578d5 --- /dev/null +++ b/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) diff --git a/functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props.args b/functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props.args new file mode 100644 index 0000000..4d6b84a --- /dev/null +++ b/functionality/verify/dtmcs/exact-arithmetic/two_dice_knuth.pm.props.args @@ -0,0 +1 @@ +-s -m -h -ex -exact-lp -precision 128 diff --git a/functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm b/functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm new file mode 100644 index 0000000..ec21c6d --- /dev/null +++ b/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 0.5:(x'=n-1) + 0.5:(x'=n+1); +[] x>0 & x 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 diff --git a/functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props b/functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props new file mode 100644 index 0000000..00353b9 --- /dev/null +++ b/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); diff --git a/functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props.args b/functionality/verify/mdps/exact-arithmetic/mdp_exact10.nm.props.args new file mode 100644 index 0000000..d816ea5 --- /dev/null +++ b/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 From f71c416b307bb5aaf40b53e2224cab1fd5fd7248 Mon Sep 17 00:00:00 2001 From: nicodelpiano Date: Thu, 18 Aug 2016 23:37:19 -0300 Subject: [PATCH 2/2] new mdp test --- .../mdps/exact-arithmetic/cert-example.nm | 11 +++++ .../exact-arithmetic/cert-example.nm.props | 41 +++++++++++++++++++ .../cert-example.nm.props.args | 1 + 3 files changed, 53 insertions(+) create mode 100644 functionality/verify/mdps/exact-arithmetic/cert-example.nm create mode 100644 functionality/verify/mdps/exact-arithmetic/cert-example.nm.props create mode 100644 functionality/verify/mdps/exact-arithmetic/cert-example.nm.props.args diff --git a/functionality/verify/mdps/exact-arithmetic/cert-example.nm b/functionality/verify/mdps/exact-arithmetic/cert-example.nm new file mode 100644 index 0000000..0e91d7e --- /dev/null +++ b/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 diff --git a/functionality/verify/mdps/exact-arithmetic/cert-example.nm.props b/functionality/verify/mdps/exact-arithmetic/cert-example.nm.props new file mode 100644 index 0000000..7b916ae --- /dev/null +++ b/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 diff --git a/functionality/verify/mdps/exact-arithmetic/cert-example.nm.props.args b/functionality/verify/mdps/exact-arithmetic/cert-example.nm.props.args new file mode 100644 index 0000000..87c64aa --- /dev/null +++ b/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