PTA tests: Improve result precision, run with exact engine

Provide exact result specs for recently introduced F<=t PTA properties. Run the tests additionally with the exact engine.
5 years ago · 658f654ae6
4 changed files with 5 additions and 3 deletions
--- a/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props
+++ b/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props
@ -3,7 +3,7 @@
 "eventually": Pmin=? [ F "done" ];

 // Minimum probability that a leader has been elected by time T
-// RESULT (delay=30): 0.851563
+// RESULT (delay=30): 0.8515625
 "deadline_min": Pmin=? [ F<=5000 "done" ];

 // Maximum probability that a leader has been elected by time T
--- a/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props.args
+++ b/prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props.args
@ -1,4 +1,5 @@
 -const delay=30 -const L=2 -ptamethod digital
 -const delay=30 -const L=2 -ptamethod digital -ex
+-const delay=30 -const L=2 -ptamethod digital -exact
 -const delay=30 -const L=2 -ptamethod games
 #-const delay=30 -const L=2 -ptamethod backwards
--- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props
+++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props
@ -17,6 +17,6 @@ const int T = 150;

 // Maximum probability of configuring IP address incorrectly by time T
 // RESULT (T=100): 6.51605e-4
-// RESULT (T=150): 0.00107253
-// RESULT (T=200): 0.00122154
+// RESULT (T=150): 0.001072525539875
+// RESULT (T=200): 0.001221541934004246875
 "deadline": Pmax=? [ F<=T s=2 & ip=2 ];
--- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args
+++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props.args
@ -1,4 +1,5 @@
 -const L=2 -ptamethod digital -e 1e-8
 -const L=2 -ptamethod digital -e 1e-8 -ex
+-const L=2 -ptamethod digital -exact
 -const L=2 -ptamethod games
 -const L=2 -ptamethod backwards