From fa47742a146f0d5d2c6118ae524a9b14ed75c071 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 17 Feb 2021 08:06:39 +0100 Subject: [PATCH] added checks for multiplicative factor parsing --- src/storm-parsers/parser/FormulaParserGrammar.cpp | 5 ++++- src/storm-parsers/parser/FormulaParserGrammar.h | 1 + 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index d5bb59ee2..9182a498c 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -149,8 +149,11 @@ namespace storm { qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]); shieldingType.name("shielding type"); + multiplicativeFactor = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ]; + multiplicativeFactor.name("multiplicative factor between 0 and 1"); + shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | - qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > qi::double_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; + qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > multiplicativeFactor)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; shieldComparison.name("shield comparison type"); stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 3c7551123..00ce6a7f5 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -207,6 +207,7 @@ namespace storm { qi::rule shieldExpression; qi::rule shieldingType; + qi::rule multiplicativeFactor; qi::rule, qi::locals, Skipper> shieldComparison; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).