From 45319ca2da06177e199918dd3c207712e077da14 Mon Sep 17 00:00:00 2001 From: lukpo Date: Thu, 12 Aug 2021 16:18:33 +0200 Subject: [PATCH] WIP GameFormulaParserTest.cpp --- .../storm/parser/GameFormulaParserTest.cpp | 148 +++++++++++++++--- 1 file changed, 125 insertions(+), 23 deletions(-) diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 2f867a494..c2d3291a5 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -1,31 +1,32 @@ #include "test/storm_gtest.h" -#include "storm-config.h" #include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/FragmentSpecification.h" -#include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" -// TODO: write this to <> inputs (games)! - TEST(GameFormulaParserTest, LabelTest) { storm::parser::FormulaParser formulaParser; - std::string input = "<> \"label\""; - std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + std::string input = "<> Pmax=? [F \"label\"]"; + + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isAtomicLabelFormula()); + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); } TEST(GameFormulaParserTest, ComplexLabelTest) { storm::parser::FormulaParser formulaParser; - std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\""; - std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + std::string input = "<> Pmin=? [X !(\"a\" & \"b\") | \"a\" & !\"c\"]"; + + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); - EXPECT_TRUE(formula->isBinaryBooleanStateFormula()); + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); } TEST(GameFormulaParserTest, ExpressionTest) { @@ -35,12 +36,14 @@ TEST(GameFormulaParserTest, ExpressionTest) { storm::parser::FormulaParser formulaParser(manager); - std::string input = "!(x | y > 3)"; - std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + std::string input = "<> Pmin=? [G !(x | y > 3)]"; + + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); - EXPECT_TRUE(formula->isUnaryBooleanStateFormula()); + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); } TEST(GameFormulaParserTest, LabelAndExpressionTest) { @@ -50,13 +53,112 @@ TEST(GameFormulaParserTest, LabelAndExpressionTest) { storm::parser::FormulaParser formulaParser(manager); - std::string input = "!\"a\" | x | y > 3"; + std::string input = "<> Pmax=? [\"b\" U !\"a\" | x | y > 3]"; + std::shared_ptr gameFormula(nullptr); + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); + + input = "<> Pmax=? [x | y > 3 | !\"a\" U \"b\"]"; + ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); + + EXPECT_TRUE(gameFormula->isStateFormula()); + EXPECT_TRUE(gameFormula->isUnaryStateFormula()); + EXPECT_TRUE(gameFormula->isGameFormula()); +} + +TEST(GameFormulaParserTest, OnePlayerCoalitionTest) { + storm::parser::FormulaParser formulaParser; + + std::string player = "p1"; + std::string input = "<<" + player + ">>" + " Pmax=? [F \"label\"]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + + auto const& gameFormula = formula->asGameFormula(); + auto const& playerCoalition = gameFormula.getCoalition(); + //ASSERT_NO_THROW(auto const& players = playerCoalition.getPlayers()); + + std::ostringstream stream; + stream << playerCoalition; + std::string playerCoalitionString = stream.str(); + + EXPECT_EQ(player, playerCoalitionString); +} + +TEST(GameFormulaParserTest, PlayersCoalitionTest) { + storm::parser::FormulaParser formulaParser; + + std::string player = "p1, p2, p3, p4, p5"; + std::string input = "<<" + player + ">>" + " Pmin=? [X \"label\"]"; + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); + auto const& gameFormula = formula->asGameFormula(); + auto const& playerCoalition = gameFormula.getCoalition(); + EXPECT_EQ(5ul, playerCoalition.getPlayers().size()); + + std::ostringstream stream; + stream << playerCoalition; + std::string playerCoalitionString = stream.str(); + + std::string playerWithoutWhiteSpace = "p1,p2,p3,p4,p5"; + + EXPECT_EQ(playerWithoutWhiteSpace, playerCoalitionString); +} - input = "x | y > 3 | !\"a\""; +TEST(GameFormulaParserTest, ProbabilityOperatorTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<> Pmax=? [\"a\" U \"b\"]"; + std::shared_ptr formula(nullptr); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); - EXPECT_TRUE(formula->isInFragment(storm::logic::propositional())); -} \ No newline at end of file + + auto const& gameFormula = formula->asGameFormula(); + auto const& probFormula = gameFormula.getSubformula(); + + EXPECT_TRUE(probFormula.isProbabilityOperatorFormula()); + EXPECT_FALSE(probFormula.asProbabilityOperatorFormula().hasBound()); + EXPECT_TRUE(probFormula.asProbabilityOperatorFormula().hasOptimalityType()); +} + +// TODO: NextOperatorTest + +TEST(GameFormulaParserTest, UntilOperatorTest) { + storm::parser::FormulaParser formulaParser; + + std::string input = "<

> Pmax=? [\"a\" U \"b\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& gameFormula1 = formula->asGameFormula(); + auto const& probFormula1 = gameFormula1.getSubformula(); + auto const& rawFormula1 = probFormula1.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula1.isUntilFormula()); + EXPECT_FALSE(rawFormula1.isBoundedUntilFormula()); + + input = "<

> Pmax=? [\"a\" U <= 4 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& gameFormula2 = formula->asGameFormula(); + auto const& probFormula2 = gameFormula2.getSubformula(); + auto const& rawFormula2 = probFormula2.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula2.isBoundedUntilFormula()); + EXPECT_TRUE(rawFormula2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_EQ(0, rawFormula2.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_EQ(4, rawFormula2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + + input = "<> Pmin=? [ (a&b) U [5,9] (b|c) ]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& gameFormula3 = formula->asGameFormula(); + auto const& probFormula3 = gameFormula3.getSubformula(); + auto const& rawFormula3 = probFormula3.asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(rawFormula3.isBoundedUntilFormula()); + EXPECT_TRUE(rawFormula3.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_EQ(5, rawFormula3.asBoundedUntilFormula().getLowerBound().evaluateAsInt()); + EXPECT_EQ(9, rawFormula3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); +} + +