From 6cea1969530d2a53f3a971bdceb6f9faa4302e63 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 24 Nov 2020 16:05:13 +0100 Subject: [PATCH] rpatl smg formulas now accept operatorFormulas --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 4984cc929..b6dde5a95 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -141,8 +141,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);