From 980f1864afed4db4ec9c6a398f156b6c0562f7e8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Jul 2017 16:54:08 +0200 Subject: [PATCH] test cases --- src/test/storm/parser/FormulaParserTest.cpp | 29 +++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/src/test/storm/parser/FormulaParserTest.cpp b/src/test/storm/parser/FormulaParserTest.cpp index 012555e8b..6269a082c 100644 --- a/src/test/storm/parser/FormulaParserTest.cpp +++ b/src/test/storm/parser/FormulaParserTest.cpp @@ -71,6 +71,35 @@ TEST(FormulaParserTest, ProbabilityOperatorTest) { EXPECT_FALSE(formula->asProbabilityOperatorFormula().hasOptimalityType()); } +TEST(FormulaParserTest, UntilOperatorTest) { + // API does not allow direct test of until, so we have to pack it in a probability operator. + storm::parser::FormulaParser formulaParser; + + std::string input = "P<0.9 [\"a\" U \"b\"]"; + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested1 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested1.isUntilFormula()); + EXPECT_FALSE(nested1.isBoundedUntilFormula()); + + input = "P<0.9 [\"a\" U<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested2 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested2.isBoundedUntilFormula()); + EXPECT_TRUE(nested2.asBoundedUntilFormula().getTimeBoundReference().isTimeBound()); + EXPECT_EQ(3, nested2.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + + input = "P<0.9 [\"a\" U{\"rewardname\"}<=3 \"b\"]"; + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + auto const& nested3 = formula->asProbabilityOperatorFormula().getSubformula(); + EXPECT_TRUE(nested3.isBoundedUntilFormula()); + EXPECT_TRUE(nested3.asBoundedUntilFormula().getTimeBoundReference().isRewardBound()); // This will fail, as we have not finished the parser. + //EXPECT_EQ("rewardname", nested3.asBoundedUntilFormula().getTimeBoundReference().getRewardName()); + EXPECT_EQ(3, nested3.asBoundedUntilFormula().getUpperBound().evaluateAsInt()); + // TODO: Extend as soon as it does not crash anymore. +} + + TEST(FormulaParserTest, RewardOperatorTest) { storm::parser::FormulaParser formulaParser;