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 ];