From 9a0be7e9ca21d7c8d741c202b7651721413ad60d Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 3 Sep 2021 15:15:25 +0200 Subject: [PATCH] added first rpatl fragment checker tests Conflicts: src/test/storm/logic/FragmentCheckerTest.cpp --- src/test/storm/logic/FragmentCheckerTest.cpp | 89 +++++++++++++------- 1 file changed, 57 insertions(+), 32 deletions(-) diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index c0f10a5ed..9f2df5ccd 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -12,16 +12,16 @@ TEST(FragmentCheckerTest, Propositional) { storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true | \"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("!true")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); @@ -42,10 +42,10 @@ TEST(FragmentCheckerTest, Pctl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification pctl = storm::logic::pctl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl)); @@ -63,19 +63,19 @@ TEST(FragmentCheckerTest, Prctl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification prctl = storm::logic::prctl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); @@ -90,19 +90,19 @@ TEST(FragmentCheckerTest, Csl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csl = storm::logic::csl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, csl)); @@ -114,25 +114,25 @@ TEST(FragmentCheckerTest, Csrl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csrl = storm::logic::csrl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); } @@ -140,32 +140,57 @@ TEST(FragmentCheckerTest, Csrl) { TEST(FragmentCheckerTest, MultiObjective) { storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective(); - + storm::parser::FormulaParser formulaParser; std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, 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\"], R<=4[F \"label\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, 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 ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - +} + +TEST(FragmentCheckerTest, Rpatl) { + auto expManager = std::make_shared(); + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification rpatl = storm::logic::rpatl(); + + storm::parser::FormulaParser formulaParser(expManager); + std::shared_ptr formula; + + ASSERT_ANY_THROW(formula = formulaParser.parseSingleFormulaFromString("<> \"label\"")); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1>> P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2>> Pmin=? [ \"label1\" U \"label2\" ]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> Rmax=? [ LRA ]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> R=? [C<=3]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); }