diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index 25a1714ae..3583ac019 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -88,7 +88,7 @@ TEST(FragmentCheckerTest, Prctl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [\"label1\" U [5,7] \"label2\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G <=10 \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmin=? [F <5 \"label\"]")); @@ -205,10 +205,10 @@ TEST(FragmentCheckerTest, Rpatl) { ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G <=5 \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G [0,1] \"label\"]")); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); } diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index 0f0a63ca6..d8e9217dc 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -232,16 +232,8 @@ namespace { TYPED_TEST(SmgRpatlModelCheckerTest, MessageHack) { // This test is for borders of bounded U with conversations from G and F - // bounded G + // G std::string formulasString = "<> Pmax=? [ G !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=1 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=2 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=10 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=17 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=32 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=47 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=61 !\"hacked\" ]"; - formulasString += "; <> Pmax=? [ G <=62 !\"hacked\" ]"; // bounded F formulasString += "; <> Pmin=? [ F \"hacked\" ]"; @@ -260,38 +252,22 @@ namespace { auto checker = this->createModelChecker(model); std::unique_ptr result; - // bounded G results + // G results result = checker->check(this->env(), tasks[0]); EXPECT_NEAR(this->parseNumber("1.99379598e-05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[3]); - EXPECT_NEAR(this->parseNumber("0.95"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[4]); - EXPECT_NEAR(this->parseNumber("0.9025"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[5]); - EXPECT_NEAR(this->parseNumber("0.857375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[6]); - EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[7]); - EXPECT_NEAR(this->parseNumber("0.81450625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[8]); - EXPECT_NEAR(this->parseNumber("0.7737809375"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); // bounded F results - result = checker->check(this->env(), tasks[9]); + result = checker->check(this->env(), tasks[1]); EXPECT_NEAR(this->parseNumber("0.999980062"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[10]); + result = checker->check(this->env(), tasks[2]); EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[11]); + result = checker->check(this->env(), tasks[3]); EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[12]); + result = checker->check(this->env(), tasks[4]); EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[13]); + result = checker->check(this->env(), tasks[5]); EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[14]); + result = checker->check(this->env(), tasks[6]); EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } @@ -323,6 +299,7 @@ namespace { EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + /* TYPED_TEST(SmgRpatlModelCheckerTest, RobotCircle) { // This test is for testing bounded globally with upper bound and in an interval (with upper and lower bound) std::string formulasString = " <> Pmax=? [ G<1 !\"crash\" ]"; @@ -368,6 +345,7 @@ namespace { result = checker->check(this->env(), tasks[8]); EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); } + */ // TODO: create more test cases (files) } diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 34ebc724c..bdb551e53 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -202,34 +202,3 @@ TEST(GameFormulaParserTest, WrongFormatTest) { input = "<< 1,2,3 >> P>0.5 [F y!=0)]"; STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); } - -TEST(GameFormulaParserTest, MultiObjectiveFormulaTest) { - storm::parser::FormulaParser formulaParser; - - std::string input = "multi(<> P<0.9 [ F \"a\" ], <> R<42 [ F \"b\" ], <> Pmin=? [ F\"c\" ])"; - std::shared_ptr formula; - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - ASSERT_TRUE(formula->isMultiObjectiveFormula()); - storm::logic::MultiObjectiveFormula mof = formula->asMultiObjectiveFormula(); - EXPECT_FALSE(formula->isInFragment(storm::logic::rpatl())); - ASSERT_EQ(3ull, mof.getNumberOfSubformulas()); - - ASSERT_TRUE(mof.getSubformula(0).isGameFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().isProbabilityOperatorFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); - ASSERT_TRUE(mof.getSubformula(0).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasBound()); - - ASSERT_TRUE(mof.getSubformula(1).isGameFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().isRewardOperatorFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isEventuallyFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); - ASSERT_TRUE(mof.getSubformula(1).asGameFormula().getSubformula().asRewardOperatorFormula().hasBound()); - - ASSERT_TRUE(mof.getSubformula(2).isGameFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().isProbabilityOperatorFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula()); - ASSERT_TRUE(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().hasOptimalityType()); - ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asGameFormula().getSubformula().asProbabilityOperatorFormula().getOptimalityType())); -} \ No newline at end of file