From 11b9c605154e24cb7fd5aed3087a0fe4ffb01d6d Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 13 Jul 2017 12:12:41 +0200 Subject: [PATCH] Adapted fragment checker test to new multiobjective-fragment specification --- src/test/storm/logic/FragmentCheckerTest.cpp | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 643742bbf..c846f7f68 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -145,26 +145,17 @@ TEST(FragmentCheckerTest, MultiObjective) { std::shared_ptr formula; ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); + EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C]")); - EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0.5,1] \"label\"]")); - EXPECT_TRUE(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\"])")); 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\"])]")); + 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\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));