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 b54c6c83..ddd48d9a 100644 --- a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props +++ b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props @@ -39,4 +39,4 @@ R{"a"}=? [ F s>2 ] R{"a"}=? [ S ]; // RESULT: 0.0 -R{"a"}=? [ S ] +R{"a_state"}=? [ S ] diff --git a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm index 439cf0af..acc00cb9 100644 --- a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm +++ b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm @@ -28,3 +28,11 @@ s=2 : 5; s=4 : 3; [r] true : 17; endrewards + +rewards "s" + true : s; +endrewards + +rewards "s3" + s>=3 : s; +endrewards diff --git a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm.props b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm.props index 73f6751d..e18c21f8 100644 --- a/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm.props +++ b/prism-tests/functionality/verify/ctmcs/rewards/ctmc_rewards2.sm.props @@ -7,6 +7,10 @@ R{"r2"}=? [ F s>2 ] // RESULT: 13/60 R{"time"}=? [ F s>2 ] +// RESULT: 1 +R{"time"}=? [ S ] + + // RESULT: Infinity R{"r"}=? [ F s>3 ] @@ -21,3 +25,29 @@ R{"r"}=? [ C ] // RESULT: 44/3 R{"r"}=? [ S ] + + +// RESULT: 1/15 +R{"s"}=? [ F s>=2 ] + +// RESULT: Infinity +R{"s"}=? [ F s>=5 ] + +// RESULT: Infinity +R{"s"}=? [ C ] + +// RESULT: 3.25 +R{"s"}=? [ S ] + + +// RESULT: 0 +R{"s3"}=? [ F s>=2 ] + +// RESULT: Infinity +R{"s3"}=? [ F s>=5 ] + +// RESULT: Infinity +R{"s3"}=? [ C ] + +// RESULT: 37/12 +R{"s3"}=? [ S ]