From 54522409446e22cdc986f14716bdad3a4e7466fc Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 13 Aug 2021 09:53:04 +0200 Subject: [PATCH] removed unnecessary testcases (e.g. there are no atomic label formulas in game formulas since they must have a coalition of players and an operator) --- .../storm/parser/GameFormulaParserTest.cpp | 66 ------------------- 1 file changed, 66 deletions(-) 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;