diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index c79485dc0..f1a8ad4ef 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -83,7 +83,15 @@ struct PrctlParser::PrctlGrammar : qi::grammar> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> pathFormula >> qi::lit("]"))[qi::_val = + probabilisticNoBoundOperator = (probabilisticMinimumNoBoundOperator | probabilisticMaximumNoBoundOperator | probabilisticDeterministicNoBoundOperator); + + probabilisticMinimumNoBoundOperator = (qi::lit("P") >> qi::lit("min") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, true)]; + + probabilisticMaximumNoBoundOperator = (qi::lit("P") >> qi::lit("max") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1, false)]; + + probabilisticDeterministicNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1)]; probabilisticNoBoundOperator.name("no bound operator"); rewardNoBoundOperator = (qi::lit("R") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> rewardPathFormula >> qi::lit("]"))[qi::_val = @@ -141,6 +149,9 @@ struct PrctlParser::PrctlGrammar : qi::grammar*(), Skipper> noBoundOperator; qi::rule*(), Skipper> probabilisticNoBoundOperator; + qi::rule*(), Skipper> probabilisticMinimumNoBoundOperator; + qi::rule*(), Skipper> probabilisticMaximumNoBoundOperator; + qi::rule*(), Skipper> probabilisticDeterministicNoBoundOperator; qi::rule*(), Skipper> rewardNoBoundOperator; qi::rule*(), Skipper> pathFormula;