diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp index 82979d17f..4d7f1ea08 100644 --- a/src/test/storm/parser/GameFormulaParserTest.cpp +++ b/src/test/storm/parser/GameFormulaParserTest.cpp @@ -255,4 +255,27 @@ TEST(GameFormulaParserTest, CommentTest) { EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula()); ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula()); +} + +TEST(GameFormulaParserTest, WrongFormatTest) { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareIntegerVariable("y"); + + storm::parser::FormulaParser formulaParser(manager); + std::string input = "<> P>0.5 [ a ]"; + std::shared_ptr formula(nullptr); + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<

> P=0.5 [F \"a\"]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<> P>0.5 [F !(x = 0)]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<< p1, p2 >> P>0.5 [F !y]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<< 1,2,3 >> P>0.5 [F y!=0)]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); } \ No newline at end of file