test cases: add a few more R=?[F], R=?[S], R=?[C] properties for CTMCs

(with reward structures without transition rewards)

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 ]

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

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 ]