sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Implemented the improvements from the PRCTL parser also in the CSL and 

LTL parsers.
main
Lanchid 13 years ago
parent
a08db1b2cf
commit
00a7c50ad4
5 changed files with 35 additions and 42 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 40
      src/parser/CslParser.cpp
  2. 30
      src/parser/LtlParser.cpp
  3. 1
      src/parser/PrctlParser.cpp
  4. 2
      test/functional/parser/CslParserTest.cpp
  5. 4
      test/functional/parser/LtlParserTest.cpp

40
src/parser/CslParser.cpp
View File

@ -40,7 +40,15 @@ namespace parser {
template<typename Iterator, typename Skipper> template<typename Iterator, typename Skipper>
struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper > { struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper > {
CslGrammar() : CslGrammar::base_type(start) { CslGrammar() : CslGrammar::base_type(start) {
freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
//This block contains helper rules that may be used several times
freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
comparisonType = (
(qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] |
(qi::lit(">"))[qi::_val = storm::property::GREATER] |
(qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] |
(qi::lit("<"))[qi::_val = storm::property::LESS]);
//Comment: Empty line or line starting with "//"
comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr];
//This block defines rules for parsing state formulas //This block defines rules for parsing state formulas
stateFormula %= orFormula; stateFormula %= orFormula;
@ -63,25 +71,13 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::Abstr
phoenix::new_<storm::property::csl::Ap<double>>(qi::_1)]; phoenix::new_<storm::property::csl::Ap<double>>(qi::_1)];
atomicProposition.name("state formula"); atomicProposition.name("state formula");
probabilisticBoundOperator = ( probabilisticBoundOperator = (
(qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::ProbabilisticBoundOperator<double> >(storm::property::GREATER, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::ProbabilisticBoundOperator<double> >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::ProbabilisticBoundOperator<double> >(storm::property::LESS, qi::_1, qi::_2)] |
(qi::lit("P") > qi::lit("<=") > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::ProbabilisticBoundOperator<double> >(storm::property::LESS_EQUAL, qi::_1, qi::_2)]
(qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::ProbabilisticBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]
); );
probabilisticBoundOperator.name("state formula"); probabilisticBoundOperator.name("state formula");
steadyStateBoundOperator = ( steadyStateBoundOperator = (
(qi::lit("S") >> qi::lit(">") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::SteadyStateBoundOperator<double> >(storm::property::GREATER, qi::_1, qi::_2)] |
(qi::lit("S") >> qi::lit(">=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::SteadyStateBoundOperator<double> >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] |
(qi::lit("S") >> qi::lit("<") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::SteadyStateBoundOperator<double> >(storm::property::LESS, qi::_1, qi::_2)] |
(qi::lit("S") > qi::lit("<=") >> qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::SteadyStateBoundOperator<double> >(storm::property::LESS_EQUAL, qi::_1, qi::_2)]
(qi::lit("S") >> comparisonType > qi::double_ > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::csl::SteadyStateBoundOperator<double> >(qi::_1, qi::_2, qi::_3)]
); );
steadyStateBoundOperator.name("state formula"); steadyStateBoundOperator.name("state formula");
@ -126,11 +122,18 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::Abstr
phoenix::new_<storm::property::csl::Until<double>>(phoenix::bind(&storm::property::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)]; phoenix::new_<storm::property::csl::Until<double>>(phoenix::bind(&storm::property::csl::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::property::csl::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
until.name("path formula (for probabilistic operator)"); until.name("path formula (for probabilistic operator)");
start = (noBoundOperator | stateFormula);
formula = (noBoundOperator | stateFormula);
formula.name("CSL formula");
start = (((formula) > (comment | qi::eps))[qi::_val = qi::_1] |
comment
) > qi::eoi;
start.name("CSL formula"); start.name("CSL formula");
} }
qi::rule<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper> start; qi::rule<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper> start;
qi::rule<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper> formula;
qi::rule<Iterator, storm::property::csl::AbstractCslFormula<double>*(), Skipper> comment;
qi::rule<Iterator, storm::property::csl::AbstractStateFormula<double>*(), Skipper> stateFormula; qi::rule<Iterator, storm::property::csl::AbstractStateFormula<double>*(), Skipper> stateFormula;
qi::rule<Iterator, storm::property::csl::AbstractStateFormula<double>*(), Skipper> atomicStateFormula; qi::rule<Iterator, storm::property::csl::AbstractStateFormula<double>*(), Skipper> atomicStateFormula;
@ -155,6 +158,7 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::Abstr
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName; qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
qi::rule<Iterator, storm::property::ComparisonType(), Skipper> comparisonType;
}; };

30
src/parser/LtlParser.cpp
View File

@ -43,6 +43,11 @@ namespace parser {
template<typename Iterator, typename Skipper> template<typename Iterator, typename Skipper>
struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper > { struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper > {
LtlGrammar() : LtlGrammar::base_type(start) { LtlGrammar() : LtlGrammar::base_type(start) {
//This block contains helper rules that may be used several times
freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
//Comment: Empty line or line starting with "//"
comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr];
freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
//This block defines rules for parsing state formulas //This block defines rules for parsing state formulas
@ -68,27 +73,9 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::Abstr
atomicProposition = (freeIdentifierName)[qi::_val = atomicProposition = (freeIdentifierName)[qi::_val =
phoenix::new_<storm::property::ltl::Ap<double>>(qi::_1)]; phoenix::new_<storm::property::ltl::Ap<double>>(qi::_1)];
atomicProposition.name("LTL formula"); atomicProposition.name("LTL formula");
/*probabilisticBoundOperator = (
(qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::ltl::ProbabilisticBoundOperator<double> >(storm::property::GREATER, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::ltl::ProbabilisticBoundOperator<double> >(storm::property::GREATER_EQUAL, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::ltl::ProbabilisticBoundOperator<double> >(storm::property::LESS, qi::_1, qi::_2)] |
(qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::ltl::ProbabilisticBoundOperator<double> >(storm::property::LESS_EQUAL, qi::_1, qi::_2)]
);
probabilisticBoundOperator.name("state formula");*/
//This block defines rules for parsing formulas with noBoundOperators
/*noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator);
noBoundOperator.name("no bound operator");
probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> LtlFormula >> qi::lit("]"))[qi::_val =
phoenix::new_<storm::property::ltl::ProbabilisticNoBoundOperator<double> >(qi::_1)];
probabilisticNoBoundOperator.name("no bound operator");*/
//This block defines rules for parsing probabilistic path formulas //This block defines rules for parsing probabilistic path formulas
pathFormula = (boundedEventually | eventually | globally);//(boundedEventually | eventually | globally | boundedUntil | until);
pathFormula = (boundedEventually | eventually | globally);
pathFormula.name("LTL formula"); pathFormula.name("LTL formula");
boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val = boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val =
phoenix::new_<storm::property::ltl::BoundedEventually<double>>(qi::_2, qi::_1)]; phoenix::new_<storm::property::ltl::BoundedEventually<double>>(qi::_2, qi::_1)];
@ -100,11 +87,14 @@ struct LtlParser::LtlGrammar : qi::grammar<Iterator, storm::property::ltl::Abstr
phoenix::new_<storm::property::ltl::Globally<double> >(qi::_1)]; phoenix::new_<storm::property::ltl::Globally<double> >(qi::_1)];
globally.name("LTL formula"); globally.name("LTL formula");
start = ltlFormula;
start = (((ltlFormula) > (comment | qi::eps))[qi::_val = qi::_1] |
comment
) > qi::eoi;
start.name("LTL formula"); start.name("LTL formula");
} }
qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> start; qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> start;
qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> comment;
qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> ltlFormula; qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> ltlFormula;
qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> atomicLtlFormula; qi::rule<Iterator, storm::property::ltl::AbstractLtlFormula<double>*(), Skipper> atomicLtlFormula;

1
src/parser/PrctlParser.cpp
View File

@ -35,7 +35,6 @@ namespace parser {
template<typename Iterator, typename Skipper> template<typename Iterator, typename Skipper>
struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper > { struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper > {
PrctlGrammar() : PrctlGrammar::base_type(start) { PrctlGrammar() : PrctlGrammar::base_type(start) {
//This block contains helper rules that may be used several times //This block contains helper rules that may be used several times
freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))]; freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
comparisonType = ( comparisonType = (

2
test/functional/parser/CslParserTest.cpp
View File

@ -116,7 +116,7 @@ TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
TEST(CslParserTest, parseComplexFormulaTest) { TEST(CslParserTest, parseComplexFormulaTest) {
storm::parser::CslParser* cslParser = nullptr; storm::parser::CslParser* cslParser = nullptr;
ASSERT_NO_THROW( 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] ]) //and a comment")
); );
ASSERT_NE(cslParser->getFormula(), nullptr); ASSERT_NE(cslParser->getFormula(), nullptr);

4
test/functional/parser/LtlParserTest.cpp
View File

@ -132,7 +132,7 @@ TEST(LtlParserTest, parseComplexUntilTest) {
TEST(LtlParserTest, parseComplexFormulaTest) { TEST(LtlParserTest, parseComplexFormulaTest) {
storm::parser::LtlParser* ltlParser = nullptr; storm::parser::LtlParser* ltlParser = nullptr;
ASSERT_NO_THROW( ASSERT_NO_THROW(
ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b")
ltlParser = new storm::parser::LtlParser("a U F b | G a & F<=3 a U<=7 b //and a comment :P")
); );
ASSERT_NE(ltlParser->getFormula(), nullptr); ASSERT_NE(ltlParser->getFormula(), nullptr);
@ -145,7 +145,7 @@ TEST(LtlParserTest, parseComplexFormulaTest) {
TEST(LtlParserTest, wrongFormulaTest) { TEST(LtlParserTest, wrongFormulaTest) {
storm::parser::LtlParser* ltlParser = nullptr; storm::parser::LtlParser* ltlParser = nullptr;
ASSERT_THROW( ASSERT_THROW(
ltlParser = new storm::parser::LtlParser("(a | b) & +"),
ltlParser = new storm::parser::LtlParser("(a | c) & +"),
storm::exceptions::WrongFormatException storm::exceptions::WrongFormatException
); );
delete ltlParser; delete ltlParser;

Write Preview
Loading…
Cancel
Save