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 ddd48d9a..0c05baa3 100644 --- a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props +++ b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props @@ -11,7 +11,7 @@ R{"a"}=? [ C<=10 ]; // RESULT: 12.11429 R{"a"}=? [ C<=100 ]; -// RESULT: 12.11429 +// RESULT: 12.114285714285716 R{"a"}=? [ C ]; // RESULT: Infinity diff --git a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props index 0272d15c..eba817a3 100644 --- a/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props +++ b/prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props @@ -16,7 +16,7 @@ Pmax=? [ F s=2 & ip=L ]; const int T = 150; // Maximum probability of configuring IP address incorrectly by time T -// RESULT (T=100): 6.51605e-4 -// RESULT (T=150): 0.001072525539875 -// RESULT (T=200): 0.001221541934004246875 +// RESULT (T=100): 130321/200000000 +// RESULT (T=150): 8580204319/8000000000000 +// RESULT (T=200): 390893418881359/320000000000000000 "deadline": Pmax=? [ F<=T s=2 & ip=2 ];