|
@ -270,8 +270,8 @@ namespace storm { |
|
|
|
|
|
|
|
|
booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; |
|
|
booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; |
|
|
booleanLiteralFormula.name("boolean literal formula"); |
|
|
booleanLiteralFormula.name("boolean literal formula"); |
|
|
|
|
|
|
|
|
operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator; |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator | expectedTimeOperator; |
|
|
operatorFormula.name("operator formulas"); |
|
|
operatorFormula.name("operator formulas"); |
|
|
|
|
|
|
|
|
atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; |
|
|
atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; |
|
@ -334,8 +334,8 @@ namespace storm { |
|
|
start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; |
|
|
start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; |
|
|
start.name("start"); |
|
|
start.name("start"); |
|
|
|
|
|
|
|
|
/*!
|
|
|
|
|
|
* Enable the following lines to print debug output for most the rules. |
|
|
|
|
|
|
|
|
//Enable the following lines to print debug output for most the rules.
|
|
|
|
|
|
/*
|
|
|
debug(start); |
|
|
debug(start); |
|
|
debug(stateFormula); |
|
|
debug(stateFormula); |
|
|
debug(orStateFormula); |
|
|
debug(orStateFormula); |
|
@ -343,6 +343,7 @@ namespace storm { |
|
|
debug(probabilityOperator); |
|
|
debug(probabilityOperator); |
|
|
debug(rewardOperator); |
|
|
debug(rewardOperator); |
|
|
debug(steadyStateOperator); |
|
|
debug(steadyStateOperator); |
|
|
|
|
|
debug(expectedTimeOperator); |
|
|
debug(pathFormulaWithoutUntil); |
|
|
debug(pathFormulaWithoutUntil); |
|
|
debug(pathFormula); |
|
|
debug(pathFormula); |
|
|
debug(conditionalFormula); |
|
|
debug(conditionalFormula); |
|
@ -357,7 +358,7 @@ namespace storm { |
|
|
debug(reachabilityRewardFormula); |
|
|
debug(reachabilityRewardFormula); |
|
|
debug(cumulativeRewardFormula); |
|
|
debug(cumulativeRewardFormula); |
|
|
debug(instantaneousRewardFormula); |
|
|
debug(instantaneousRewardFormula); |
|
|
*/ |
|
|
|
|
|
|
|
|
*/ |
|
|
|
|
|
|
|
|
// Enable error reporting.
|
|
|
// Enable error reporting.
|
|
|
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
@ -366,6 +367,7 @@ namespace storm { |
|
|
qi::on_error<qi::fail>(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
|
|
|
qi::on_error<qi::fail>(expectedTimeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(steadyStateOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(steadyStateOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|
qi::on_error<qi::fail>(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|
|