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<std::string, std::shared_ptr<storm::jani::Constant>> 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<storm::jani::Constant> 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<std::string, std::shared_ptr<storm::jani::Variable>> globalVars;
if (variablesCount == 1) {
for (auto const& varStructure : parsedStructure.at("variables")) {
- model.addVariable(*parseVariable(varStructure, "global"));
+ std::shared_ptr<storm::jani::Variable> 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<storm::logic::AtomicLabelFormula>(propertyStructure.get<std::string>());
}
}
- 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<storm::logic::AtomicExpressionFormula>(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<std::string>());
+ auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get<std::string>(),{},{});
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<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(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<std::string>());
+ auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get<std::string>(),{},{});
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<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble())));
@@ -488,7 +494,7 @@ namespace storm {
return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment);
}
- std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) {
+ std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> 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<storm::jani::Variable> JaniParser::parseVariable(json const &variableStructure, std::string const& scopeDescription, bool prefWithScope) {
+ std::shared_ptr<storm::jani::Variable> JaniParser::parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> 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<storm::jani::RealVariable>(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<storm::jani::UnboundedIntegerVariable>(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<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
- storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, localVars,returnNoneInitializedOnUnknownOperator);
+ std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> 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<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> 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<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> 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<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) {
+ storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> 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<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
+ storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
if(expressionStructure.is_boolean()) {
if(expressionStructure.get<bool>()) {
return expressionManager->boolean(true);
@@ -730,7 +739,7 @@ namespace storm {
return expressionManager->rational(expressionStructure.get<double>());
} else if(expressionStructure.is_string()) {
std::string ident = expressionStructure.get<std::string>();
- 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<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> 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<std::string, std::shared_ptr<storm::jani::Variable>> localVars;
+ if(varDeclCount > 0) {
+ for(auto const& varStructure : automatonStructure.at("variables")) {
+ std::shared_ptr<storm::jani::Variable> 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<std::string, uint64_t> 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<std::string, std::shared_ptr<storm::jani::Variable>> localVars;
- if(varDeclCount > 0) {
- for(auto const& varStructure : automatonStructure.at("variables")) {
- std::shared_ptr<storm::jani::Variable> 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<storm::jani::Model, std::map<std::string, storm::jani::Property>> 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<storm::jani::Variable> 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<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
+ storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants);
+ std::shared_ptr<storm::jani::Variable> parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool prefWithScope = false);
+ storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
private:
- std::shared_ptr<storm::jani::Constant> parseConstant(json const& constantStructure, std::string const& scopeDescription = "global");
+ std::shared_ptr<storm::jani::Constant> parseConstant(json const& constantStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> 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<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none);
- std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
- std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
+ std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars= {}, bool returnNoneOnUnknownOpString = false);
+ std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context);
std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::jani::Composition> parseComposition(json const& compositionStructure);
- storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
+ storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
/**