Browse Source

Bounded LTL formula check for FragmentCheckerTest Rpatl

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

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

@ -193,6 +193,6 @@ TEST(FragmentCheckerTest, Rpatl) {
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<player1>> R=? [C<=3]")); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<player1>> R=? [C<=3]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, rpatl)); EXPECT_FALSE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F \"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));
} }
Loading…
Cancel
Save