Browse Source

Fixed a FragmentCheckerTest case which considered a formula that is now considered invalid.

tempestpy_adaptions
Tim Quatmann 4 years ago
committed by Stefan Pranger
parent
commit
8c669b9e8b
  1. 2
      src/test/storm/logic/FragmentCheckerTest.cpp

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

@ -150,7 +150,7 @@ TEST(FragmentCheckerTest, MultiObjective) {
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])"));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])]")); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\"] & \"label\" & R<=4[F \"label\"])]"));

Loading…
Cancel
Save