From d8592bffa2fbb5c3c613a5f67688953002f94909 Mon Sep 17 00:00:00 2001
From: lukpo <lukas.posch@student.tugraz.at>
Date: Thu, 12 Aug 2021 09:56:33 +0200
Subject: [PATCH] shielding check for FragmentCheckerTest Rpatl

---
 src/test/storm/logic/FragmentCheckerTest.cpp | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp
index 866e63fb0..056c84a88 100644
--- a/src/test/storm/logic/FragmentCheckerTest.cpp
+++ b/src/test/storm/logic/FragmentCheckerTest.cpp
@@ -195,4 +195,14 @@ TEST(FragmentCheckerTest, Rpatl) {
 
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F [2,5] \"label\"]"));
     EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
+
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PostSafety, gamma=0.749> <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]"));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
+
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.749> <<a,b,c>> Pmax=? [G <=5 \"label\"]"));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
+
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shieldFileName, Optimal> <<p1,p2>> Pmin=? [G [0,1] \"label\"]"));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
+
 }