Browse Source

WIP (HOA-path) FormulaParser: parse HOAPathFormula

Note: Syntax of HOA path formulas will change!

 Conflicts:
	src/storm-parsers/parser/FormulaParserGrammar.cpp
	src/storm-parsers/parser/FormulaParserGrammar.h
tempestpy_adaptions
Joachim Klein 4 years ago
committed by Stefan Pranger
parent
commit
ad774e5138
  1. 1
      src/storm-parsers/parser/FormulaParserGrammar.cpp

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

@ -75,7 +75,6 @@ namespace storm {
untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
untilFormula.name("until formula"); untilFormula.name("until formula");
conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
hoaPathFormula = qi::lit("HOA:") > qi::lit("{") hoaPathFormula = qi::lit("HOA:") > qi::lit("{")
> quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)] > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)]

Loading…
Cancel
Save