From 3c34373a824213d0b89b367fc4935b6bbe664c9a Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 26 Jul 2018 11:08:20 +0200
Subject: [PATCH] =?UTF-8?q?test=20cases:=20add=20a=20few=20more=20R=3D=3F[?=
 =?UTF-8?q?F],=20R=3D=3F[S],=20R=3D=3F[C]=20properties=20for=20CTMCs?=

(with reward structures without transition rewards)
---
 .../ctmcs/rewards/ctmc_rewards.sm.props       |  2 +-
 .../verify/ctmcs/rewards/ctmc_rewards2.sm     |  8 +++++
 .../ctmcs/rewards/ctmc_rewards2.sm.props      | 30 +++++++++++++++++++
 3 files changed, 39 insertions(+), 1 deletion(-)

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 ]