From 57fd0fa2dd400a3fa0c65bb2bf5f04ebe37fb99b Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 12 Feb 2017 14:14:11 +0100 Subject: [PATCH] Fixed variable parsing in JANI, now stricter and handles a larger set of files (also detects issues in our export...). --- src/storm/parser/JaniParser.cpp | 169 +++++++++++++++++--------------- src/storm/parser/JaniParser.h | 14 +-- 2 files changed, 98 insertions(+), 85 deletions(-) diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 99f1993d4..6d9519a7a 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -101,30 +101,36 @@ namespace storm { STORM_LOG_THROW(parsedStructure.count("actions") < 2, storm::exceptions::InvalidJaniException, "Action-declarations can be given at most once."); parseActions(parsedStructure.at("actions"), model); size_t constantsCount = parsedStructure.count("constants"); + std::unordered_map> constants; STORM_LOG_THROW(constantsCount < 2, storm::exceptions::InvalidJaniException, "Constant-declarations can be given at most once."); if (constantsCount == 1) { for (auto const &constStructure : parsedStructure.at("constants")) { - model.addConstant(*parseConstant(constStructure, "global")); + std::shared_ptr constant = parseConstant(constStructure, constants, "global"); + constants.emplace(constant->getName(), constant); + model.addConstant(*constant); } } size_t variablesCount = parsedStructure.count("variables"); STORM_LOG_THROW(variablesCount < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables."); + std::unordered_map> globalVars; if (variablesCount == 1) { for (auto const& varStructure : parsedStructure.at("variables")) { - model.addVariable(*parseVariable(varStructure, "global")); + std::shared_ptr variable = parseVariable(varStructure, "global", globalVars, constants); + globalVars.emplace(variable->getName(), variable); + model.addVariable(*variable); } } STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given"); STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array"); // Automatons can only be parsed after constants and variables. for (auto const& automataEntry : parsedStructure.at("automata")) { - model.addAutomaton(parseAutomaton(automataEntry, model)); + model.addAutomaton(parseAutomaton(automataEntry, model, globalVars, constants)); } STORM_LOG_THROW(parsedStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Model has multiple initial value restrictions"); storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true); if(parsedStructure.count("restrict-initial") > 0) { STORM_LOG_THROW(parsedStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Model needs an expression inside the initial restricion"); - initialValueRestriction = parseExpression(parsedStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name); + initialValueRestriction = parseExpression(parsedStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name, globalVars, constants); } model.setInitialStatesRestriction(initialValueRestriction); STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); @@ -165,7 +171,7 @@ namespace storm { storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure) { storm::jani::PropertyInterval pi; if (piStructure.count("lower") > 0) { - pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval"); + pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval", {}, {}); // TODO substitute constants. STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds"); @@ -177,7 +183,7 @@ namespace storm { } if (piStructure.count("upper") > 0) { - pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval"); + pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval", {}, {}); // TODO substitute constants. STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds"); @@ -202,7 +208,7 @@ namespace storm { return std::make_shared(propertyStructure.get()); } } - storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); + storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, {}, {}, true); if(expr.isInitialized()) { assert(bound == boost::none); return std::make_shared(expr); @@ -223,7 +229,7 @@ namespace storm { } else if (opString == "Emin" || opString == "Emax") { bool time=false; STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); - storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context, {}, {}); if (rewExpr.isVariable()) { time = false; } else { @@ -257,7 +263,7 @@ namespace storm { if (propertyStructure.count("step-instant") > 0) { - storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context); + storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context, {}, {}); STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant step-instants"); int64_t stepInstant = stepInstantExpr.evaluateAsInt(); STORM_LOG_THROW(stepInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative step-instants are allowed"); @@ -277,7 +283,7 @@ namespace storm { } } } else if (propertyStructure.count("time-instant") > 0) { - storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context); + storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context, {}, {}); STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant time-instants"); double timeInstant = timeInstantExpr.evaluateAsDouble(); STORM_LOG_THROW(timeInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative time-instants are allowed"); @@ -417,12 +423,12 @@ namespace storm { ct = storm::logic::ComparisonType::Greater; } if (propertyStructure.at("left").count("op") > 0 && (propertyStructure.at("left").at("op") == "Pmin" || propertyStructure.at("left").at("op") == "Pmax" || propertyStructure.at("left").at("op") == "Emin" || propertyStructure.at("left").at("op") == "Emax" || propertyStructure.at("left").at("op") == "Smin" || propertyStructure.at("left").at("op") == "Smax")) { - auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get()); + auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get(),{},{}); STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); // TODO evaluate this expression directly as rational number return parseFormula(propertyStructure.at("left"), formulaContext, "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) { - auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get()); + auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get(),{},{}); STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); // TODO evaluate this expression directly as rational number return parseFormula(propertyStructure.at("right"),formulaContext, "", storm::logic::Bound(ct, storm::utility::convertNumber(expr.evaluateAsDouble()))); @@ -488,7 +494,7 @@ namespace storm { return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment); } - std::shared_ptr JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) { + std::shared_ptr JaniParser::parseConstant(json const& constantStructure, std::unordered_map> const& constants, std::string const& scopeDescription) { STORM_LOG_THROW(constantStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scopeDescription + ") must have a name"); std::string name = getString(constantStructure.at("name"), "variable-name in " + scopeDescription + "-scope"); // TODO check existance of name. @@ -500,7 +506,7 @@ namespace storm { STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name + "' (scope: " + scopeDescription + ") must be given at most once."); if (valueCount == 1) { // Read initial value before; that makes creation later on a bit easier, and has as an additional benefit that we do not need to check whether the variable occurs also on the assignment. - initExpr = parseExpression(constantStructure.at("value"), "Value of constant " + name + " (scope: " + scopeDescription + ")"); + initExpr = parseExpression(constantStructure.at("value"), "Value of constant " + name + " (scope: " + scopeDescription + ")", {}, constants); assert(initExpr.isInitialized()); } @@ -557,7 +563,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << constantStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); } - std::shared_ptr JaniParser::parseVariable(json const &variableStructure, std::string const& scopeDescription, bool prefWithScope) { + std::shared_ptr JaniParser::parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool prefWithScope) { STORM_LOG_THROW(variableStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scopeDescription + ") must have a name"); std::string pref = prefWithScope ? scopeDescription + VARIABLE_AUTOMATON_DELIMITER : ""; std::string name = getString(variableStructure.at("name"), "variable-name in " + scopeDescription + "-scope"); @@ -584,7 +590,7 @@ namespace storm { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->rational(defaultRationalInitialValue); } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); + initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); STORM_LOG_THROW(initVal.get().hasRationalType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a rational"); } return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); @@ -597,7 +603,7 @@ namespace storm { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->boolean(defaultBooleanInitialValue); } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); + initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); } if(transientVar) { @@ -612,7 +618,7 @@ namespace storm { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->integer(defaultIntegerInitialValue); } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); + initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer"); } return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar); @@ -632,10 +638,10 @@ namespace storm { if(kind == "bounded") { // First do the bounds, that makes the code a bit more streamlined STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given"); - storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")"); + storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")", globalVars, constants, localVars); assert(lowerboundExpr.isInitialized()); STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given"); - storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")"); + storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")", globalVars, constants, localVars); assert(upperboundExpr.isInitialized()); STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given"); if(initvalcount == 1) { @@ -643,7 +649,7 @@ namespace storm { initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr); // TODO as soon as we support half-open intervals, we have to change this. } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); + initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); } } std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); @@ -672,14 +678,14 @@ namespace storm { STORM_LOG_THROW(expected == actual, storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects " << expected << " arguments, but got " << actual << " in " << errorInfo << "."); } - std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, localVars,returnNoneInitializedOnUnknownOperator); + std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars,returnNoneInitializedOnUnknownOperator); return {left}; } - std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); - storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); return {left, right}; } /** @@ -706,16 +712,19 @@ namespace storm { } } - storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const &ident,std::string const& scopeDescription, std::unordered_map> const& localVars) { + storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars) { if(localVars.count(ident) == 1) { return localVars.at(ident)->getExpressionVariable(); + } else if(globalVars.count(ident) == 1) { + return globalVars.at(ident)->getExpressionVariable(); + } else if(constants.count(ident) == 1) { + return constants.at(ident)->getExpressionVariable(); } else { - STORM_LOG_THROW(expressionManager->hasVariable(ident), storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); - return expressionManager->getVariable(ident); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); } } - storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { if(expressionStructure.is_boolean()) { if(expressionStructure.get()) { return expressionManager->boolean(true); @@ -730,7 +739,7 @@ namespace storm { return expressionManager->rational(expressionStructure.get()); } else if(expressionStructure.is_string()) { std::string ident = expressionStructure.get(); - return storm::expressions::Expression(getVariableOrConstantExpression(ident, scopeDescription, localVars)); + return storm::expressions::Expression(getVariableOrConstantExpression(ident, scopeDescription, globalVars, constants, localVars)); } else if(expressionStructure.is_object()) { if(expressionStructure.count("distribution") == 1) { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Distributions are not supported by storm expressions, cannot import " << expressionStructure.dump() << " in " << scopeDescription << "."); @@ -742,15 +751,15 @@ namespace storm { STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required"); STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required"); STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "If operator required"); - arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator)); - arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator)); - arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator)); + arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator)); + arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator)); + arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator)); ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription); assert(arguments.size() == 3); ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ite(arguments[0], arguments[1], arguments[2]); } else if (opstring == "∨") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -759,7 +768,7 @@ namespace storm { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] || arguments[1]; } else if (opstring == "∧") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -768,7 +777,7 @@ namespace storm { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -777,7 +786,7 @@ namespace storm { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return (!arguments[0]) || arguments[1]; } else if (opstring == "¬") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); if(!arguments[0].isInitialized()) { return storm::expressions::Expression(); @@ -785,7 +794,7 @@ namespace storm { ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return !arguments[0]; } else if (opstring == "=") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(arguments[0].hasBooleanType()) { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); @@ -795,7 +804,7 @@ namespace storm { return arguments[0] == arguments[1]; } } else if (opstring == "≠") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(arguments[0].hasBooleanType()) { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); @@ -805,7 +814,7 @@ namespace storm { return arguments[0] != arguments[1]; } } else if (opstring == "<") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -814,7 +823,7 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] < arguments[1]; } else if (opstring == "≤") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -823,7 +832,7 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] <= arguments[1]; } else if (opstring == ">") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -832,7 +841,7 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] > arguments[1]; } else if (opstring == "≥") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -841,94 +850,94 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] >= arguments[1]; } else if (opstring == "+") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] + arguments[1]; } else if (opstring == "-") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] - arguments[1]; } else if (opstring == "-") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription,globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return -arguments[0]; } else if (opstring == "*") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] * arguments[1]; } else if (opstring == "/") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] / arguments[1]; } else if (opstring == "%") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); // TODO implement STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "modulo operation is not yet implemented"); } else if (opstring == "max") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return storm::expressions::maximum(arguments[0],arguments[1]); } else if (opstring == "min") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return storm::expressions::minimum(arguments[0],arguments[1]); } else if (opstring == "floor") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::floor(arguments[0]); } else if (opstring == "ceil") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ceil(arguments[0]); } else if (opstring == "abs") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::abs(arguments[0]); } else if (opstring == "sgn") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::sign(arguments[0]); } else if (opstring == "trc") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::abs(arguments[0]); } else if (opstring == "pow") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); // TODO implement STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "pow operation is not yet implemented"); } else if (opstring == "exp") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); // TODO implement STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "exp operation is not yet implemented"); } else if (opstring == "log") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); @@ -965,10 +974,24 @@ namespace storm { } } - storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure, storm::jani::Model const& parentModel) { + storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure, storm::jani::Model const& parentModel, std::unordered_map> const& globalVars, std::unordered_map> const& constants ) { STORM_LOG_THROW(automatonStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Each automaton must have a name"); std::string name = getString(automatonStructure.at("name"), " the name field for automaton"); storm::jani::Automaton automaton(name, expressionManager->declareIntegerVariable("_loc_" + name)); + + uint64_t varDeclCount = automatonStructure.count("variables"); + STORM_LOG_THROW(varDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of variables"); + std::unordered_map> localVars; + if(varDeclCount > 0) { + for(auto const& varStructure : automatonStructure.at("variables")) { + std::shared_ptr var = parseVariable(varStructure, name, globalVars, constants, localVars, true); + assert(localVars.count(var->getName()) == 0); + automaton.addVariable(*var); + localVars.emplace(var->getName(), var); + } + } + + STORM_LOG_THROW(automatonStructure.count("locations") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' does not have locations."); std::unordered_map locIds; for(auto const& locEntry : automatonStructure.at("locations")) { @@ -984,7 +1007,7 @@ namespace storm { STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value"); storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')"); STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); - storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); + storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')", globalVars, constants, localVars); transientAssignments.emplace_back(lhs, rhs); } } @@ -999,20 +1022,10 @@ namespace storm { storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true); if(automatonStructure.count("restrict-initial") > 0) { STORM_LOG_THROW(automatonStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' needs an expression inside the initial restricion"); - initialValueRestriction = parseExpression(automatonStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name); + initialValueRestriction = parseExpression(automatonStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name, globalVars, constants, localVars); } automaton.setInitialStatesRestriction(initialValueRestriction); - uint64_t varDeclCount = automatonStructure.count("variables"); - STORM_LOG_THROW(varDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of variables"); - std::unordered_map> localVars; - if(varDeclCount > 0) { - for(auto const& varStructure : automatonStructure.at("variables")) { - std::shared_ptr var = parseVariable(varStructure, name, true); - assert(localVars.count(var->getName()) == 0); - automaton.addVariable(*var); - localVars.emplace(var->getName(), var); - } - } + STORM_LOG_THROW(automatonStructure.count("edges") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' must have a list of edges"); @@ -1034,7 +1047,7 @@ namespace storm { storm::expressions::Expression rateExpr; if(edgeEntry.count("rate") > 0) { STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a defing expression."); - rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), "rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'"); + rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), "rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type"); } // guard @@ -1042,7 +1055,7 @@ namespace storm { storm::expressions::Expression guardExpr = expressionManager->boolean(true); if(edgeEntry.count("guard") == 1) { STORM_LOG_THROW(edgeEntry.at("guard").count("exp") == 1, storm::exceptions::InvalidJaniException, "Guard in edge from '" + sourceLoc + "' in automaton '" + name + "' must have one expression"); - guardExpr = parseExpression(edgeEntry.at("guard").at("exp"), "guard expression in edge from '" + sourceLoc + "' in automaton '" + name + "'", localVars); + guardExpr = parseExpression(edgeEntry.at("guard").at("exp"), "guard expression in edge from '" + sourceLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); STORM_LOG_THROW(guardExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Guard " << guardExpr << " does not have Boolean type."); } assert(guardExpr.isInitialized()); @@ -1064,7 +1077,7 @@ namespace storm { probExpr = expressionManager->rational(1.0); } else { STORM_LOG_THROW(destEntry.at("probability").count("exp") == 1, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have a probability expression."); - probExpr = parseExpression(destEntry.at("probability").at("exp"), "probability expression in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars); + probExpr = parseExpression(destEntry.at("probability").at("exp"), "probability expression in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); } assert(probExpr.isInitialized()); STORM_LOG_THROW(probExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Probability expression " << probExpr << " does not have a numerical type." ); @@ -1080,7 +1093,7 @@ namespace storm { storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); // value STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); - storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars); + storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); // TODO check types // index uint64_t assignmentIndex = 0; // default. diff --git a/src/storm/parser/JaniParser.h b/src/storm/parser/JaniParser.h index 627a056dd..db207546c 100644 --- a/src/storm/parser/JaniParser.h +++ b/src/storm/parser/JaniParser.h @@ -47,20 +47,20 @@ namespace storm { void readFile(std::string const& path); std::pair> parseModel(bool parseProperties = true); storm::jani::Property parseProperty(json const& propertyStructure); - storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel); - std::shared_ptr parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>(), bool returnNoneOnUnknownOpString = false); + storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, std::unordered_map> const& globalVars, std::unordered_map> const& constants); + std::shared_ptr parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool prefWithScope = false); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); private: - std::shared_ptr parseConstant(json const& constantStructure, std::string const& scopeDescription = "global"); + std::shared_ptr parseConstant(json const& constantStructure, std::unordered_map> const& constants, std::string const& scopeDescription = "global"); /** * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); std::shared_ptr parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional> bound = boost::none); - std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); - std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars= {}, bool returnNoneOnUnknownOpString = false); + std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); std::vector> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); @@ -68,7 +68,7 @@ namespace storm { std::shared_ptr parseComposition(json const& compositionStructure); - storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); + storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}); /**