From f1aa210b5a548fea67094a09338f6302c3292ebe Mon Sep 17 00:00:00 2001
From: lukpo <lukas.posch@student.tugraz.at>
Date: Thu, 12 Aug 2021 10:00:44 +0200
Subject: [PATCH] shielding check for FragmentCheckerTest Prctl

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

diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp
index 056c84a88..762f26f73 100644
--- a/src/test/storm/logic/FragmentCheckerTest.cpp
+++ b/src/test/storm/logic/FragmentCheckerTest.cpp
@@ -84,6 +84,15 @@ TEST(FragmentCheckerTest, Prctl) {
 
     ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
     EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
+
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PostSafety, gamma=0.678> Pmax=? [\"label1\" U [5,7] \"label2\"]"));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
+
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.9> Pmax=? [G <=10 \"label\"]"));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
+
+    ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shieldFileName, Optimal> Pmin=? [F <5 \"label\"]"));
+    EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
 }
 
 TEST(FragmentCheckerTest, Csl) {