From e3fbb77362ec128e35ee240b971aa18dc4aa11a8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 13 Mar 2019 12:03:06 +0100 Subject: [PATCH] =?UTF-8?q?JaniParser::parseFormula:=20Boolean=20connectio?= =?UTF-8?q?ns=20of=20AtomicExpressionFormulas=20are=20now=20parsed=20as=20?= =?UTF-8?q?a=20single=20AtomicExpressionFormula=20(i.e.=20'a>1=20&=20b>2'?= =?UTF-8?q?=20becomes=20a=20single=20atomic=20proposition=20instead=20of?= =?UTF-8?q?=20having=20two=20propositions=20'a>1'=20and=20'b>2').=20This?= =?UTF-8?q?=20reduces=20the=20number=20of=20labels=20that=20need=20to=20be?= =?UTF-8?q?=20considered=20and=20improves=20partial=20state=20space=20expl?= =?UTF-8?q?oration=20for=20formulas=20such=20as=20'P=3D=3F=20[F=20a>1=20&?= =?UTF-8?q?=20b>2]'.?= --- src/storm-parsers/parser/JaniParser.cpp | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 4065d89c6..876ffc042 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -287,10 +287,21 @@ namespace storm { } } storm::expressions::Expression expr = parseExpression(propertyStructure, scope.refine("expression in property"), true); - if (expr.isInitialized() && propertyStructure.count("op") == 0) { - assert(bound == boost::none); - return std::make_shared(expr); - } else if(propertyStructure.count("op") == 1) { + if (expr.isInitialized()) { + bool exprContainsLabel = false; + auto varsInExpr = expr.getVariables(); + for (auto const& varInExpr : varsInExpr) { + if (labels.count(varInExpr.getName()) > 0) { + exprContainsLabel = true; + break; + } + } + if (!exprContainsLabel) { + assert(bound == boost::none); + return std::make_shared(expr); + } + } + if (propertyStructure.count("op") == 1) { std::string opString = getString(propertyStructure.at("op"), "Operation description"); if(opString == "Pmin" || opString == "Pmax") { @@ -556,9 +567,7 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons for properties are supported."); } else if (expr.isInitialized()) { - assert(bound == boost::none); - STORM_LOG_THROW(expr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Expected a boolean expression at " << scope.description); - return std::make_shared(expr); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Non-trivial Expression '" << expr << "' contains a boolean transient variable. Can not translate to PRCTL-like formula at " << scope.description << "."); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString); }