diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index cc8c7014a..f07807dae 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -3,72 +3,6 @@ #include "storm/logic/FragmentSpecification.h" #include "storm/storage/expressions/ExpressionManager.h" -TEST(GameFormulaParserTest, LabelTest) { - storm::parser::FormulaParser formulaParser; - - std::string input = "<> Pmax=? [F \"label\"]"; - - std::shared_ptr gameFormula(nullptr); - ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - - EXPECT_TRUE(gameFormula->isStateFormula()); - EXPECT_TRUE(gameFormula->isUnaryStateFormula()); - EXPECT_TRUE(gameFormula->isGameFormula()); -} - -TEST(GameFormulaParserTest, ComplexLabelTest) { - storm::parser::FormulaParser formulaParser; - - std::string input = "<> Pmin=? [X !(\"a\" & \"b\") | \"a\" & !\"c\"]"; - - std::shared_ptr gameFormula(nullptr); - ASSERT_NO_THROW(gameFormula = formulaParser.parseSingleFormulaFromString(input)); - - EXPECT_TRUE(gameFormula->isStateFormula()); - EXPECT_TRUE(gameFormula->isUnaryStateFormula()); - EXPECT_TRUE(gameFormula->isGameFormula()); -} - -TEST(GameFormulaParserTest, ExpressionTest) { - std::shared_ptr manager(new storm::expressions::ExpressionManager()); - manager->declareBooleanVariable("x"); - manager->declareIntegerVariable("y"); - - storm::parser::FormulaParser formulaParser(manager); - - std::string input = "<> Pmin=? [G !(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()); -} - -TEST(GameFormulaParserTest, LabelAndExpressionTest) { - std::shared_ptr manager(new storm::expressions::ExpressionManager()); - manager->declareBooleanVariable("x"); - manager->declareIntegerVariable("y"); - - storm::parser::FormulaParser formulaParser(manager); - - 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;