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).
8 years ago · 2cb079156a
20 changed files with 66 additions and 66 deletions
--- 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" ]
--- 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 ]
--- 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 ]
--- 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 ]
--- 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 ]


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

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

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

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

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

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