From 4cdd70949c1ebd969d60f585d48b8adfe1ef1013 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 23 Jun 2021 06:27:54 +0200 Subject: [PATCH] FormulaParser: HOA formulas shall only consider state-subformulas --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 6a522051a..18adfc932 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -126,7 +126,7 @@ namespace storm { globallyFormula.name("globally formula"); hoaPathFormula = qi::lit("HOA:") > qi::lit("{") > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)] - >> *(qi::lit(",") > quotedString > qi::lit("->") > formula(FormulaKind::Path, qi::_r1) )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)] + >> *(qi::lit(",") > quotedString > qi::lit("->") > formula(FormulaKind::State, qi::_r1) )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)] > qi::lit("}"); multiBoundedPathFormulaOperand = pathFormula(qi::_r1)[qi::_pass = phoenix::bind(&FormulaParserGrammar::isValidMultiBoundedPathFormulaOperand, phoenix::ref(*this), qi::_1)][qi::_val = qi::_1]; multiBoundedPathFormulaOperand.name("multi bounded path formula operand");