diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 983f64cae..ae7d8e0f7 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -351,10 +351,9 @@ namespace storm { debug(labelFormula); debug(expressionFormula); debug(rewardPathFormula); - debug(reachabilityRewardFormula); debug(cumulativeRewardFormula); debug(instantaneousRewardFormula); - */ + */ // Enable error reporting. qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); diff --git a/test/functional/logic/FragmentCheckerTest.cpp b/test/functional/logic/FragmentCheckerTest.cpp index 6f21467af..bb5d358c9 100644 --- a/test/functional/logic/FragmentCheckerTest.cpp +++ b/test/functional/logic/FragmentCheckerTest.cpp @@ -1,14 +1,132 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/FormulaParser.h" -#include "src/logic/FragmentSpecification.h" +#include "src/logic/FragmentChecker.h" #include "src/exceptions/WrongFormatException.h" -TEST(FragmentCheckerTest, PctlTest) { +TEST(FragmentCheckerTest, Propositional) { + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification prop = storm::logic::propositional(); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true | \"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("!true")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F true]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, prop)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("false | P>0.5 [G \"label\"]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, prop)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, prop)); +} + +TEST(FragmentCheckerTest, Pctl) { + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification pctl = storm::logic::pctl(); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl)); +} + +TEST(FragmentCheckerTest, Prctl) { + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification prctl = storm::logic::prctl(); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, prctl)); +} + +TEST(FragmentCheckerTest, Csl) { + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification csl = storm::logic::csl(); + + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); + EXPECT_FALSE(checker.conformsToSpecification(*formula, csl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); +} + +TEST(FragmentCheckerTest, Csrl) { + storm::logic::FragmentChecker checker; + storm::logic::FragmentSpecification csrl = storm::logic::csrl(); + storm::parser::FormulaParser formulaParser; + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - std::string input = "\"label\""; - std::shared_ptr formula(nullptr); - ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); }