Browse Source

rpatl smg formulas now accept operatorFormulas

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
40f5fc04a9
  1. 3
      src/storm-parsers/parser/FormulaParserGrammar.cpp

3
src/storm-parsers/parser/FormulaParserGrammar.cpp

@ -149,8 +149,7 @@ namespace storm {
> qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)];
coalitionOperator.name("coalition operator");
// only LRA for now, need to adapt this (beware of cyclic gameFormula pass!)
gameFormula = (coalitionOperator > longRunAverageOperator)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), storm::logic::Coalition({}, {1}), qi::_1)];
gameFormula = (coalitionOperator > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)];
gameFormula.name("game formula");
stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);

Loading…
Cancel
Save