diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 4d7f1ea08..cc8c7014a 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -278,4 +278,34 @@ 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(); + 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