From 1c16c17a57dda221ae3ee4e5aef65e129779076e Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 14 Apr 2021 16:26:55 +0200 Subject: [PATCH] FragmentCheckerTest: Fixed a few more testcaes that now correspond to invalid formulae. --- src/test/storm/logic/FragmentCheckerTest.cpp | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 2fccdb1e8..c0f10a5ed 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -153,10 +153,7 @@ TEST(FragmentCheckerTest, MultiObjective) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])")); 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\"])")); + 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\"], R<=4[F \"label\"])")); @@ -165,9 +162,6 @@ TEST(FragmentCheckerTest, MultiObjective) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], multi(P<0.6 [F \"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\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));