Browse Source

More convenient syntax for time bounded formulas, and respective test

cases.
tempestpy_adaptions
Lanchid 12 years ago
parent
commit
39ff3240d3
  1. 3
      src/formula/TimeBoundedOperator.h
  2. 20
      src/parser/CslParser.cpp
  3. 16
      test/parser/CslParserTest.cpp

3
src/formula/TimeBoundedOperator.h

@ -87,7 +87,8 @@ public:
virtual std::string toString() const {
std::string result = "[";
result += std::to_string(lowerBound);
result += ";";
result += ",";
result += std::to_string(upperBound);
result += "]";
return result;
}

20
src/parser/CslParser.cpp

@ -100,8 +100,14 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
//This block defines rules for parsing probabilistic path formulas
pathFormula = (timeBoundedEventually | eventually | globally | timeBoundedUntil | until);
pathFormula.name("path formula");
timeBoundedEventually = (qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::TimeBoundedEventually<double>>(qi::_1, qi::_2, qi::_3)];
timeBoundedEventually = (
(qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::TimeBoundedEventually<double>>(qi::_1, qi::_2, qi::_3)] |
(qi::lit("F") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)[qi::_val =
phoenix::new_<storm::formula::TimeBoundedEventually<double>>(0, qi::_1, qi::_2)] |
(qi::lit("F") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)[qi::_val =
phoenix::new_<storm::formula::TimeBoundedEventually<double>>(qi::_1, std::numeric_limits<double>::infinity(), qi::_2)]
);
timeBoundedEventually.name("path formula (for probabilistic operator)");
eventually = (qi::lit("F") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
@ -109,8 +115,14 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
globally = (qi::lit("G") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
globally.name("path formula (for probabilistic operator)");
timeBoundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)
[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)];
timeBoundedUntil = (
(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)
[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)] |
(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit("<=") | qi::lit("<")) > qi::double_ > stateFormula)
[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(0, qi::_2, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)] |
(stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> (qi::lit(">=") | qi::lit(">")) > qi::double_ > stateFormula)
[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, std::numeric_limits<double>::infinity(), phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3)]
);
timeBoundedUntil.name("path formula (for probabilistic operator)");
until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];

16
test/parser/CslParserTest.cpp

@ -65,7 +65,7 @@ TEST(CslParserTest, parseProbabilisticFormulaTest) {
TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
storm::parser::CslParser* cslParser = nullptr;
ASSERT_NO_THROW(
cslParser = new storm::parser::CslParser("S >= 15 [ a & b ]")
cslParser = new storm::parser::CslParser("S >= 15 [ P < 0.2 [ a U<=3 b ] ]")
);
ASSERT_NE(cslParser->getFormula(), nullptr);
@ -75,7 +75,7 @@ TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
ASSERT_EQ(storm::formula::StateBoundOperator<double>::GREATER_EQUAL, op->getComparisonOperator());
ASSERT_EQ(15.0, op->getBound());
ASSERT_EQ("S >= 15.000000 [(a & b)]", cslParser->getFormula()->toString());
ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", cslParser->getFormula()->toString());
delete cslParser->getFormula();
delete cslParser;
@ -100,13 +100,13 @@ TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
storm::parser::CslParser* cslParser = nullptr;
ASSERT_NO_THROW(
cslParser = new storm::parser::CslParser("P = ? [ a U <= 4 b & (!c) ]")
cslParser = new storm::parser::CslParser("P = ? [ a U [3,4] b & (!c) ]")
);
ASSERT_NE(cslParser->getFormula(), nullptr);
ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U<=4 (b & !c)]");
ASSERT_EQ(cslParser->getFormula()->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]");
delete cslParser->getFormula();
delete cslParser;
@ -116,13 +116,15 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
TEST(CslParserTest, parseComplexFormulaTest) {
storm::parser::CslParser* cslParser = nullptr;
ASSERT_NO_THROW(
cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])")
cslParser = new storm::parser::CslParser("S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ])")
);
ASSERT_NE(cslParser->getFormula(), nullptr);
ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", cslParser->getFormula()->toString());
//NOTE: This test case is dependent on the string output of the double value infinity.
// In g++ and clang++ on Linux, it is "inf". If some compiler (or library) uses a different output, please
// notify me and I will restructure this test case.
ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F[7.000000,inf] (a & b)]]))", cslParser->getFormula()->toString());
delete cslParser->getFormula();
delete cslParser;

Loading…
Cancel
Save