From 2cb079156ab08db6956738bbcb445a9db62bea0c Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Wed, 25 Jul 2018 20:44:35 +0200 Subject: [PATCH] prism-tests: tweak result values for test cases (better tests of the exact engine) Some of the result values for the test cases were floating-point approximations, which results in 'close but inaccurate' errors when running the test cases against the exact engine. We replace those results either with the exact values or mark the approximated results with ~... (mostly for a few CTMC properties, where the exact results are a bit unwieldly). --- prism-tests/bugfixes/ctmc-until.sm.props | 4 ++-- prism-tests/bugfixes/rewpoliter.nm.props | 2 +- prism-tests/contrib/garavel/HG-01.pm.props | 6 ++--- prism-tests/contrib/garavel/HG-02.pm.props | 24 +++++++++---------- prism-tests/contrib/garavel/HG-03.pm.props | 12 +++++----- prism-tests/contrib/garavel/HG-06.pm.props | 2 +- prism-tests/contrib/garavel/HG-07.pm.props | 12 +++++----- prism-tests/contrib/garavel/HG-08.pm.props | 2 +- prism-tests/contrib/garavel/HG-11.pm.props | 6 ++--- prism-tests/contrib/garavel/HG-12.pm.props | 4 ++-- prism-tests/contrib/garavel/HG-13.pm.props | 8 +++---- prism-tests/contrib/garavel/HG-17.pm.props | 8 +++---- prism-tests/contrib/garavel/HG-18.pm.props | 4 ++-- prism-tests/contrib/garavel/HG-19.pm.props | 8 +++---- prism-tests/contrib/garavel/HG-20.pm.props | 8 +++---- prism-tests/contrib/garavel/HG-22.pm.props | 8 +++---- prism-tests/contrib/garavel/HG-26.pm.props | 4 ++-- .../ctmcs/rewards/ctmc_rewards.sm.props | 4 ++-- .../verify/multiple_bsccs_ss2.sm.props | 4 ++-- .../verify/ptas/reach/zeroconf.nm.props | 2 +- 20 files changed, 66 insertions(+), 66 deletions(-) diff --git a/prism-tests/bugfixes/ctmc-until.sm.props b/prism-tests/bugfixes/ctmc-until.sm.props index 4528effe..a9ad911c 100644 --- a/prism-tests/bugfixes/ctmc-until.sm.props +++ b/prism-tests/bugfixes/ctmc-until.sm.props @@ -1,6 +1,6 @@ -// RESULT: 0.6213837 +// RESULT: ~0.6213837 P=? [ !"down" U "fail_sensors" ] // test case for lower bound until problem (explicit engine, fixed in SVN 11768) -// RESULT: 0.6213837 +// RESULT: ~0.6213837 P=? [ !"down" U>=0 "fail_sensors" ] diff --git a/prism-tests/bugfixes/rewpoliter.nm.props b/prism-tests/bugfixes/rewpoliter.nm.props index a07e641c..71790712 100644 --- a/prism-tests/bugfixes/rewpoliter.nm.props +++ b/prism-tests/bugfixes/rewpoliter.nm.props @@ -1,2 +1,2 @@ -// RESULT: 34.833333 +// RESULT: 209/6 Rmin=? [ F state=4 ] diff --git a/prism-tests/contrib/garavel/HG-01.pm.props b/prism-tests/contrib/garavel/HG-01.pm.props index c75e20ff..0caca61d 100644 --- a/prism-tests/contrib/garavel/HG-01.pm.props +++ b/prism-tests/contrib/garavel/HG-01.pm.props @@ -5,13 +5,13 @@ const int x = 5; P>0.1 [ F s=7 & d=x ] // Probability of throwing 6? -// RESULT: 0.16666650772094727 +// RESULT: 1/6 P=? [ F s=7 & d=6 ] // Probability of throwing x? -// RESULT: 0.16666650772094727 +// RESULT: 1/6 P=? [ F s=7 & d=x ] // Expected number of coin flips to complete? -// RESULT: 3.6666650772094727 +// RESULT: 11/3 R=? [ F s=7 ] diff --git a/prism-tests/contrib/garavel/HG-02.pm.props b/prism-tests/contrib/garavel/HG-02.pm.props index 6db18d32..b1e1e75f 100644 --- a/prism-tests/contrib/garavel/HG-02.pm.props +++ b/prism-tests/contrib/garavel/HG-02.pm.props @@ -1,37 +1,37 @@ const int x; // unused (Hubert Garavel) -// RESULT : 0.16666650772094727 +// RESULT : 1/6 P=? [ F s=7 & d=1 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 P=? [ F s=7 & d=2 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 P=? [ F s=7 & d=3 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 P=? [ F s=7 & d=4 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 P=? [ F s=7 & d=5 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 P=? [ F s=7 & d=6 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [ s=7 & d=1 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [ s=7 & d=2 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [ s=7 & d=3 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [ s=7 & d=4 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [ s=7 & d=5 ] -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [ s=7 & d=6 ] diff --git a/prism-tests/contrib/garavel/HG-03.pm.props b/prism-tests/contrib/garavel/HG-03.pm.props index 96606bc1..1dbc75a1 100644 --- a/prism-tests/contrib/garavel/HG-03.pm.props +++ b/prism-tests/contrib/garavel/HG-03.pm.props @@ -1,27 +1,27 @@ // Probability of throwing 1? -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [s=7 & d=1 ] // Probability of throwing 2? -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [s=7 & d=2 ] // Probability of throwing 3? -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [s=7 & d=3 ] // Probability of throwing 4? -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [s=7 & d=4 ] // Probability of throwing 5? -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [s=7 & d=5 ] // Probability of throwing 6? -// RESULT : 0.16666650772094727 +// RESULT : 1/6 S=? [s=7 & d=6 ] diff --git a/prism-tests/contrib/garavel/HG-06.pm.props b/prism-tests/contrib/garavel/HG-06.pm.props index 95528fa3..e7be412f 100644 --- a/prism-tests/contrib/garavel/HG-06.pm.props +++ b/prism-tests/contrib/garavel/HG-06.pm.props @@ -1,4 +1,4 @@ const int x = 3; -// RESULT : 0.16666650772094727 +// RESULT : 1/6 P=? [ F s=7 & value=x ] diff --git a/prism-tests/contrib/garavel/HG-07.pm.props b/prism-tests/contrib/garavel/HG-07.pm.props index dd52b799..ebdeeb4f 100644 --- a/prism-tests/contrib/garavel/HG-07.pm.props +++ b/prism-tests/contrib/garavel/HG-07.pm.props @@ -1,18 +1,18 @@ -// RESULT: 0.16666650772094727 +// RESULT: 1/6 S=? [ s=7 & value=1 ] -// RESULT: 0.16666650772094727 +// RESULT: 1/6 S=? [ s=7 & value=2 ] -// RESULT: 0.16666650772094727 +// RESULT: 1/6 S=? [ s=7 & value=3 ] -// RESULT: 0.16666650772094727 +// RESULT: 1/6 S=? [ s=7 & value=4 ] -// RESULT: 0.16666650772094727 +// RESULT: 1/6 S=? [ s=7 & value=5 ] -// RESULT: 0.16666650772094727 +// RESULT: 1/6 S=? [ s=7 & value=6 ] diff --git a/prism-tests/contrib/garavel/HG-08.pm.props b/prism-tests/contrib/garavel/HG-08.pm.props index 0af96b58..011cfef3 100644 --- a/prism-tests/contrib/garavel/HG-08.pm.props +++ b/prism-tests/contrib/garavel/HG-08.pm.props @@ -1,5 +1,5 @@ const int x = 4; -// RESULT : 0.33333301544189453 +// RESULT : 1/3 Pmin=? [ F s=x ] diff --git a/prism-tests/contrib/garavel/HG-11.pm.props b/prism-tests/contrib/garavel/HG-11.pm.props index 407464ef..27fd1109 100644 --- a/prism-tests/contrib/garavel/HG-11.pm.props +++ b/prism-tests/contrib/garavel/HG-11.pm.props @@ -1,10 +1,10 @@ -// RESULT : 0.4999999961139362 +// RESULT : 0.5 S=?[x = 0] -// RESULT : 0.26499994880454214 +// RESULT : 0.265 S=?[x != y] -// RESULT : 0.3895499480066543 +// RESULT : 0.38955 S=?[x != z] diff --git a/prism-tests/contrib/garavel/HG-12.pm.props b/prism-tests/contrib/garavel/HG-12.pm.props index e5502092..ee2f453f 100644 --- a/prism-tests/contrib/garavel/HG-12.pm.props +++ b/prism-tests/contrib/garavel/HG-12.pm.props @@ -1,6 +1,6 @@ -// RESULT : 0.8333333333333334 +// RESULT : 5/6 S=? [s=0] -// RESULT : 0.16666666666666666 +// RESULT : 1/6 S=? [s=1] diff --git a/prism-tests/contrib/garavel/HG-13.pm.props b/prism-tests/contrib/garavel/HG-13.pm.props index c37a5fc6..c2fc54de 100644 --- a/prism-tests/contrib/garavel/HG-13.pm.props +++ b/prism-tests/contrib/garavel/HG-13.pm.props @@ -1,13 +1,13 @@ -// RESULT : 0.26499994923594816 +// RESULT : 0.265 S=? [ x!=y ] -// RESULT : 0.1943750119614966 +// RESULT : 0.194375 S=? [ y!=z ] -// RESULT : 0.22656244390682956 +// RESULT : 0.2265625 S=? [x!=z & x!=y] -// RESULT : 0.038437505329118646 +// RESULT : 0.0384375 S=? [x=z & x!=y] diff --git a/prism-tests/contrib/garavel/HG-17.pm.props b/prism-tests/contrib/garavel/HG-17.pm.props index e7322e3a..c4fb1e4c 100644 --- a/prism-tests/contrib/garavel/HG-17.pm.props +++ b/prism-tests/contrib/garavel/HG-17.pm.props @@ -1,12 +1,12 @@ -// RESULT : 0.03000000042158528 +// RESULT : 0.03 S=? [e1] -// RESULT : 0.029200001350718534 +// RESULT : 0.0292 S=? [e2] -// RESULT : 0.05740099996352296 +// RESULT : 0.057401 S=? [(!ee1 & e2)|(ee1&!e2)] -// RESULT : 8.99500015350916E-4 +// RESULT : 8.995E-4 S=? [(ee1 & e2)] diff --git a/prism-tests/contrib/garavel/HG-18.pm.props b/prism-tests/contrib/garavel/HG-18.pm.props index 00728df3..7bee1bdc 100644 --- a/prism-tests/contrib/garavel/HG-18.pm.props +++ b/prism-tests/contrib/garavel/HG-18.pm.props @@ -1,9 +1,9 @@ // Steady state probability of being in State 0 -// RESULT : 0.8333333333333334 +// RESULT : 5/6 S=? [s=0 ] // Steady state probability of being in State 1 -// RESULT : 0.16666666666666666 +// RESULT : 1/6 S=? [s=1 ] diff --git a/prism-tests/contrib/garavel/HG-19.pm.props b/prism-tests/contrib/garavel/HG-19.pm.props index cc90ca68..3991d3a6 100644 --- a/prism-tests/contrib/garavel/HG-19.pm.props +++ b/prism-tests/contrib/garavel/HG-19.pm.props @@ -1,13 +1,13 @@ -// RESULT : 0.530487009959398 +// RESULT : ~0.530487009959398 S=? [x = 0] -// RESULT : 0.5220657596380086 +// RESULT : ~0.5220657596380086 S=? [x = y] -// RESULT : 0.3406646324774578 +// RESULT : ~0.3406646324774578 S=? [y = z] -// RESULT : 0.4177711482230605 +// RESULT : ~0.4177711482230605 S=? [x = z] diff --git a/prism-tests/contrib/garavel/HG-20.pm.props b/prism-tests/contrib/garavel/HG-20.pm.props index 092190b3..a4910898 100644 --- a/prism-tests/contrib/garavel/HG-20.pm.props +++ b/prism-tests/contrib/garavel/HG-20.pm.props @@ -1,16 +1,16 @@ //Error after line 1 -// RESULT : 0.26499994880454214 +// RESULT : 0.265 S=? [ x!=y ] //between the output of line1 and line 2 -// RESULT : 0.2119125122358965 +// RESULT : 0.2119125 S=? [ y!=z ] // after l1 + l2 with single transmission error either in l1 or l2 -// RESULT : 0.22131869228765 +// RESULT : 0.22131875 S=? [x!=z & x!=y] //after l1+l2 with double transmission error in line1 and line 2 -// RESULT : 0.04368125651689213 +// RESULT : 0.04368125 S=? [x=z & x!=y] diff --git a/prism-tests/contrib/garavel/HG-22.pm.props b/prism-tests/contrib/garavel/HG-22.pm.props index 561d44e7..3572687d 100644 --- a/prism-tests/contrib/garavel/HG-22.pm.props +++ b/prism-tests/contrib/garavel/HG-22.pm.props @@ -1,13 +1,13 @@ //Project 3, Question 4 -// RESULT : 0.029999999815139608 +// RESULT : 0.03 S=? [ error1 ] -// RESULT : 0.029199999289065463 +// RESULT : 0.0292 S=? [ error2 ] -// RESULT : 0.05740100062966204 +// RESULT : 0.057401 S=? [ (!error1prev & error2) | (error1prev & !error2) ] -// RESULT : 8.994999945407273E-4 +// RESULT : 8.995E-4 S=? [ error1prev & error2 ] diff --git a/prism-tests/contrib/garavel/HG-26.pm.props b/prism-tests/contrib/garavel/HG-26.pm.props index afaa19d8..aba14a89 100644 --- a/prism-tests/contrib/garavel/HG-26.pm.props +++ b/prism-tests/contrib/garavel/HG-26.pm.props @@ -1,13 +1,13 @@ // long run probability that s = 0 -// RESULT: 0.6209277663961226 +// RESULT: ~0.6209277663961226 S=? [s = 0] // = b / (a+b) // long run probability that s = 1 -// RESULT: 0.3790722336038772 +// RESULT: ~0.3790722336038772 S=? [s = 1] // = a / (a+b) diff --git a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props index d4d4feaa..b54c6c83 100644 --- a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props +++ b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props @@ -30,9 +30,9 @@ R{"a"}=? [ I=1 ] R{"a"}=? [ F s=0 ] // RESULT: 3.4 R{"a"}=? [ F s=1 ] -// RESULT: 11.11429 +// RESULT: 389/35 R{"a"}=? [ F s=2 ] -// RESULT: 12.11429 +// RESULT: 424/35 R{"a"}=? [ F s>2 ] // RESULT: 0.0 diff --git a/prism-tests/functionality/verify/multiple_bsccs_ss2.sm.props b/prism-tests/functionality/verify/multiple_bsccs_ss2.sm.props index 12c7bb58..2606fb8c 100644 --- a/prism-tests/functionality/verify/multiple_bsccs_ss2.sm.props +++ b/prism-tests/functionality/verify/multiple_bsccs_ss2.sm.props @@ -1,6 +1,6 @@ // Use GS because Jacobi converges v slowly - // RESULT: 0.16524722795153043 + // RESULT: 3150000/19062347 S=? [ na=2 ]; - // RESULT: 8.535277424128644 + // RESULT: 162702420/19062347 R=? [ S ]; diff --git a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props index 7f2c74aa..0051b4b6 100644 --- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props +++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props @@ -1,3 +1,3 @@ // Maximum probability of configuring IP address incorrectly -// RESULT: 0.001301514 +// RESULT: 130321/100130321 "incorrect": Pmax=? [ F s=2 & ip=2 ];