Browse Source

shielding check for FragmentCheckerTest Rpatl

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
commit
d8592bffa2
  1. 10
      src/test/storm/logic/FragmentCheckerTest.cpp

10
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\"]")); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F [2,5] \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); 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));
} }
Loading…
Cancel
Save