Browse Source

Improve accuracy of reference result in a few test cases.

accumulation-v4.7
Dave Parker 6 years ago
parent
commit
3eea76efd8
  1. 2
      prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props
  2. 6
      prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props

2
prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props

@ -11,7 +11,7 @@ R{"a"}=? [ C<=10 ];
// RESULT: 12.11429 // RESULT: 12.11429
R{"a"}=? [ C<=100 ]; R{"a"}=? [ C<=100 ];
// RESULT: 12.11429
// RESULT: 12.114285714285716
R{"a"}=? [ C ]; R{"a"}=? [ C ];
// RESULT: Infinity // RESULT: Infinity

6
prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props

@ -16,7 +16,7 @@ Pmax=? [ F s=2 & ip=L ];
const int T = 150; const int T = 150;
// Maximum probability of configuring IP address incorrectly by time T // 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 ]; "deadline": Pmax=? [ F<=T s=2 & ip=2 ];
Loading…
Cancel
Save