Browse Source

shielding check for FragmentCheckerTest Prctl

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

9
src/test/storm/logic/FragmentCheckerTest.cpp

@ -84,6 +84,15 @@ TEST(FragmentCheckerTest, Prctl) {
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); 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) { TEST(FragmentCheckerTest, Csl) {

Loading…
Cancel
Save