diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 4c897b5a1..78e9c20a3 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -120,36 +120,58 @@ namespace storm { if (actionCount > 0) { parseActions(parsedStructure.at("actions"), model); } + + Scope scope(name); + + // Parse constants size_t constantsCount = parsedStructure.count("constants"); ConstantsMap constants; + scope.constants = &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")) { - std::shared_ptr constant = parseConstant(constStructure, constants, "global"); + std::shared_ptr constant = parseConstant(constStructure, scope.refine("constants[" + std::to_string(constants.size()) + "]")); constants.emplace(constant->getName(), &model.addConstant(*constant)); } } + + // Parse variables 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."); VariablesMap globalVars; + scope.globalVars = &globalVars; if (variablesCount == 1) { bool requireInitialValues = parsedStructure.count("restrict-initial") == 0; for (auto const& varStructure : parsedStructure.at("variables")) { - std::shared_ptr variable = parseVariable(varStructure, requireInitialValues, "global", globalVars, constants); + std::shared_ptr variable = parseVariable(varStructure, requireInitialValues, scope.refine("variables[" + std::to_string(globalVars.size()))); globalVars.emplace(variable->getName(), &model.addVariable(*variable)); } } + + uint64_t funDeclCount = parsedStructure.count("functions"); + STORM_LOG_THROW(funDeclCount < 2, storm::exceptions::InvalidJaniException, "Model '" << name << "' has more than one list of functions"); + FunctionsMap globalFuns; + scope.globalFunctions = &globalFuns; + if (funDeclCount > 0) { + for (auto const& funStructure : parsedStructure.at("functions")) { + storm::jani::FunctionDefinition funDef = parseFunctionDefinition(funStructure, scope.refine("functions[" + std::to_string(globalFuns.size()) + "] of model " + name)); + assert(globalFuns.count(funDef.getName()) == 0); + //TODO globalFuns.emplace(funDef.getName(), &model.addFunction(funDef)); + } + } + + // Parse Automata 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, globalVars, constants)); + model.addAutomaton(parseAutomaton(automataEntry, model, scope.refine("automata[" + std::to_string(model.getNumberOfAutomata()) + "]"))); } 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) { + 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, globalVars, constants); + initialValueRestriction = parseExpression(parsedStructure.at("restrict-initial").at("exp"), scope.refine("Initial value restriction")); } model.setInitialStatesRestriction(initialValueRestriction); STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); @@ -161,7 +183,7 @@ namespace storm { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { try { - auto prop = this->parseProperty(propertyEntry, globalVars, constants); + auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]")); properties.emplace(prop.getName(), prop); } catch (storm::exceptions::NotSupportedException const& ex) { STORM_LOG_WARN("Cannot handle property: " << ex.what()); @@ -175,22 +197,22 @@ namespace storm { } - std::vector> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context) { - STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << context); - return { parseFormula(propertyStructure.at("exp"), formulaContext, globalVars, constants, "Operand of operator " + opstring) }; + std::vector> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << scope.description); + return { parseFormula(propertyStructure.at("exp"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } - std::vector> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context) { - STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << context); - STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << context); - return { parseFormula(propertyStructure.at("left"), formulaContext, globalVars, constants, "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), formulaContext, globalVars, constants, "Operand of operator " + opstring) }; + std::vector> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) { + STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << scope.description); + STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << scope.description); + return { parseFormula(propertyStructure.at("left"), formulaContext, scope.refine("Operand of operator " + opstring)), parseFormula(propertyStructure.at("right"), formulaContext, scope.refine("Operand of operator " + opstring)) }; } - storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure, ConstantsMap const& constants) { + storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure, Scope const& scope) { storm::jani::PropertyInterval pi; if (piStructure.count("lower") > 0) { - pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval", {}, constants); + pi.lowerBound = parseExpression(piStructure.at("lower"), scope.refine("Lower bound for property interval")); } if (piStructure.count("lower-exclusive") > 0) { STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); @@ -198,7 +220,7 @@ namespace storm { } if (piStructure.count("upper") > 0) { - pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval", {}, constants); + pi.upperBound = parseExpression(piStructure.at("upper"), scope.refine("Upper bound for property interval")); } if (piStructure.count("upper-exclusive") > 0) { @@ -207,8 +229,6 @@ namespace storm { } STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operator must have a bounded interval, but no bounds found in '" << piStructure << "'"); return pi; - - } storm::logic::RewardAccumulation JaniParser::parseRewardAccumulation(json const& accStructure, std::string const& context) { @@ -230,7 +250,7 @@ namespace storm { return storm::logic::RewardAccumulation(accSteps, accTime, accExit); } - std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext,VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context, boost::optional bound) { + std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, Scope const& scope, boost::optional bound) { if (propertyStructure.is_boolean()) { return std::make_shared(propertyStructure.get()); } @@ -239,7 +259,7 @@ namespace storm { return std::make_shared(propertyStructure.get()); } } - storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", globalVars, constants, {}, true); + storm::expressions::Expression expr = parseExpression(propertyStructure, scope.refine("expression in property"), true); if(expr.isInitialized()) { assert(bound == boost::none); return std::make_shared(expr); @@ -247,7 +267,7 @@ namespace storm { std::string opString = getString(propertyStructure.at("op"), "Operation description"); if(opString == "Pmin" || opString == "Pmax") { - std::vector> args = parseUnaryFormulaArgument(propertyStructure, storm::logic::FormulaContext::Probability, opString, globalVars, constants, ""); + std::vector> args = parseUnaryFormulaArgument(propertyStructure, storm::logic::FormulaContext::Probability, opString, scope); assert(args.size() == 1); storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; @@ -259,8 +279,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); } 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, globalVars, constants); + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), scope.refine("Reward expression")); if (rewExpr.isVariable()) { time = false; } else { @@ -273,14 +293,14 @@ namespace storm { storm::logic::RewardAccumulation rewardAccumulation(false, false, false); if (propertyStructure.count("accumulate") > 0) { - rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), context); + rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), scope.description); } if (propertyStructure.count("step-instant") > 0) { - STORM_LOG_THROW(propertyStructure.count("time-instant") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a time-instant in " + context); - STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a reward-instant in " + context); + STORM_LOG_THROW(propertyStructure.count("time-instant") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a time-instant in " + scope.description); + STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a reward-instant in " + scope.description); - storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context, globalVars, constants); + storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), scope.refine("Step instant")); if(rewardAccumulation.isEmpty()) { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); @@ -297,9 +317,9 @@ namespace storm { } } } else if (propertyStructure.count("time-instant") > 0) { - STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a time-instant and a reward-instant in " + context); + STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a time-instant and a reward-instant in " + scope.description); - storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context, globalVars, constants); + storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), scope.refine("time instant")); if(rewardAccumulation.isEmpty()) { if (rewExpr.isVariable()) { @@ -320,11 +340,11 @@ namespace storm { std::vector bounds; std::vector boundReferences; for (auto const& rewInst : propertyStructure.at("reward-instants")) { - storm::expressions::Expression rewInstExpression = parseExpression(rewInst.at("exp"), "Reward expression in " + context, globalVars, constants); + storm::expressions::Expression rewInstExpression = parseExpression(rewInst.at("exp"), scope.refine("Reward expression")); STORM_LOG_THROW(!rewInstExpression.isVariable(), storm::exceptions::NotSupportedException, "Reward bounded cumulative reward formulas should only argue over reward expressions."); - storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rewInst.at("accumulate"), context); + storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rewInst.at("accumulate"), scope.description); boundReferences.emplace_back(rewInstExpression.getVariables().begin()->getName(), boundRewardAccumulation); - storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), "reward instant in " + context, globalVars, constants); + storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), scope.refine("reward instant")); bounds.emplace_back(false, rewInstantExpr); } if (rewExpr.isVariable()) { @@ -336,8 +356,8 @@ namespace storm { } else { std::shared_ptr subformula; if (propertyStructure.count("reach") > 0) { - auto context = time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward; - subformula = std::make_shared(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context, rewardAccumulation); + auto formulaContext = time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward; + subformula = std::make_shared(parseFormula(propertyStructure.at("reach"), formulaContext, scope.refine("Reach-expression of operator " + opString)), formulaContext, rewardAccumulation); } else { subformula = std::make_shared(rewardAccumulation); } @@ -375,10 +395,10 @@ namespace storm { assert(bound == boost::none); std::vector> args; if (opString == "U") { - args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, globalVars, constants, ""); + args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, scope); } else { assert(opString == "F"); - args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, globalVars, constants, ""); + args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope); args.push_back(args[0]); args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); } @@ -386,7 +406,7 @@ namespace storm { std::vector> lowerBounds, upperBounds; std::vector tbReferences; if (propertyStructure.count("step-bounds") > 0) { - storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds"), constants); + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds"), scope.refine("step-bounded until").clearVariables()); boost::optional lowerBound, upperBound; if (pi.hasLowerBound()) { lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); @@ -401,7 +421,7 @@ namespace storm { tbReferences.emplace_back(storm::logic::TimeBoundType::Steps); } if (propertyStructure.count("time-bounds") > 0) { - storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"), constants); + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"), scope.refine("time-bounded until").clearVariables()); boost::optional lowerBound, upperBound; if (pi.hasLowerBound()) { lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound)); @@ -417,11 +437,11 @@ namespace storm { } if (propertyStructure.count("reward-bounds") > 0 ) { for (auto const& rbStructure : propertyStructure.at("reward-bounds")) { - storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds"), constants); - STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); - storm::expressions::Expression rewExpr = parseExpression(rbStructure.at("exp"), "Reward expression in " + context, globalVars, constants); + storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds"), scope.refine("reward-bounded until").clearVariables()); + STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description); + storm::expressions::Expression rewExpr = parseExpression(rbStructure.at("exp"), scope.refine("Reward expression")); STORM_LOG_THROW(rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions."); - storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rbStructure.at("accumulate"), context); + storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rbStructure.at("accumulate"), scope.description); tbReferences.emplace_back(rewExpr.getVariables().begin()->getName(), boundRewardAccumulation); std::string rewardName = rewExpr.getVariables().begin()->getName(); STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type."); @@ -447,7 +467,7 @@ namespace storm { } } else if (opString == "G") { assert(bound == boost::none); - std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, globalVars, constants, "Subformula of globally operator " + context); + std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope.refine("Subformula of globally operator ")); if (propertyStructure.count("step-bounds") > 0) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently"); } else if (propertyStructure.count("time-bounds") > 0) { @@ -465,19 +485,19 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Release is not supported"); } else if (opString == "∧" || opString == "∨") { assert(bound == boost::none); - std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, globalVars, constants, ""); + std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, scope); assert(args.size() == 2); storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; return std::make_shared(oper, args[0], args[1]); } else if (opString == "⇒") { assert(bound == boost::none); - std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, globalVars, constants, ""); + std::vector> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, scope); assert(args.size() == 2); std::shared_ptr tmp = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); return std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, tmp, args[1]); } else if (opString == "¬") { assert(bound == boost::none); - std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, globalVars, constants, ""); + std::vector> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, scope); assert(args.size() == 1); return std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); @@ -500,7 +520,7 @@ namespace storm { std::string propertyOperatorString = getString(propertyStructure.at(leftRight[i]).at("op"), "property-operator"); std::set const propertyOperatorStrings = {"Pmin", "Pmax","Emin", "Emax", "Smin", "Smax"}; if (propertyOperatorStrings.count(propertyOperatorString) > 0) { - auto boundExpr = parseExpression(propertyStructure.at(leftRight[1-i]), "Threshold for operator " + propertyStructure.at(leftRight[i]).at("op").get(), {}, constants); + auto boundExpr = parseExpression(propertyStructure.at(leftRight[1-i]), scope.refine("Threshold for operator " + propertyStructure.at(leftRight[i]).at("op").get())); if ((opString == "=" || opString == "≠")) { STORM_LOG_THROW(!boundExpr.containsVariables(), storm::exceptions::NotSupportedException, "Comparison operators '=' or '≠' in property specifications are currently not supported."); auto boundValue = boundExpr.evaluateAsRational(); @@ -520,7 +540,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Comparison operators '=' or '≠' in property specifications are currently not supported."); } } - return parseFormula(propertyStructure.at(leftRight[i]), formulaContext, globalVars, constants, "", storm::logic::Bound(ct, boundExpr)); + return parseFormula(propertyStructure.at(leftRight[i]), formulaContext, scope, storm::logic::Bound(ct, boundExpr)); } } } @@ -533,7 +553,7 @@ namespace storm { } } - storm::jani::Property JaniParser::parseProperty(json const& propertyStructure, VariablesMap const& globalVars, ConstantsMap const& constants) { + storm::jani::Property JaniParser::parseProperty(json const& propertyStructure, Scope const& scope) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); // TODO check unique name std::string name = getString(propertyStructure.at("name"), "property-name"); @@ -586,7 +606,7 @@ namespace storm { if (!statesFormula) { try { // Try to parse the states as formula. - statesFormula = parseFormula(expressionStructure.at("states"), storm::logic::FormulaContext::Undefined, globalVars, constants, "Values of property " + name); + statesFormula = parseFormula(expressionStructure.at("states"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); } catch (storm::exceptions::NotSupportedException const& ex) { throw ex; } catch (storm::exceptions::NotImplementedException const& ex) { @@ -595,48 +615,48 @@ namespace storm { } STORM_LOG_THROW(statesFormula, storm::exceptions::NotImplementedException, "Could not derive states formula."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); - auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, globalVars, constants, "Values of property " + name); + auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, scope.refine("Values of property " + name)); return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft, statesFormula), comment); } - std::shared_ptr JaniParser::parseConstant(json const& constantStructure, ConstantsMap 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"); + std::shared_ptr JaniParser::parseConstant(json const& constantStructure, Scope const& scope) { + STORM_LOG_THROW(constantStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scope.description + ") must have a name"); + std::string name = getString(constantStructure.at("name"), "variable-name in " + scope.description + "-scope"); // TODO check existance of name. // TODO store prefix in variable. std::string exprManagerName = name; - STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); + STORM_LOG_THROW(constantStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Constant '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration."); size_t valueCount = constantStructure.count("value"); storm::expressions::Expression initExpr; - STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name + "' (scope: " + scopeDescription + ") must be given at most once."); + STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name + "' (scope: " + scope.description + ") 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 + ")", {}, constants); + initExpr = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name)); assert(initExpr.isInitialized()); } if (constantStructure.at("type").is_object()) { -// STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ") kind must be given"); -// std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name + "(scope: " + scopeDescription + ") "); +// STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scope.description << ") kind must be given"); +// std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name + "(scope: " + scope.description + ") "); // 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_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scope.description << ") lower-bound must be given"); +// storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable "+ name + " (scope: " + scope.description + ")"); // 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_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scope.description << ") upper-bound must be given"); +// storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scope.description + ")"); // 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"); -// std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); +// STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scope.description << ") base must be given"); +// std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scope.description + ") "); // if(basictype == "int") { -// STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); -// STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); +// STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scope.description << ") must be integer-typed"); +// STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scope.description << ") must be integer-typed"); // return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), lowerboundExpr, upperboundExpr); // } else { -// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); +// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scope.description << ") "); // } // } else { -// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") "); +// STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scope.description << ") "); // } } else if(constantStructure.at("type").is_string()) { @@ -661,83 +681,121 @@ namespace storm { } } else { // TODO clocks. - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << constantStructure.at("type").dump() << " for constant '" << name << "' (scope: " << scopeDescription << ")"); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << constantStructure.at("type").dump() << " for constant '" << name << "' (scope: " << scope.description << ")"); } } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << constantStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << constantStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scope.description << ")"); } - void JaniParser::parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars) { + void JaniParser::parseType(ParsedType& result, json const& typeStructure, std::string variableName, Scope const& scope) { if (typeStructure.is_string()) { if (typeStructure == "real") { result.basicType = ParsedType::BasicType::Real; + result.expressionType = expressionManager->getRationalType(); } else if (typeStructure == "bool") { result.basicType = ParsedType::BasicType::Bool; + result.expressionType = expressionManager->getBooleanType(); } else if (typeStructure == "int") { result.basicType = ParsedType::BasicType::Int; + result.expressionType = expressionManager->getIntegerType(); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << variableName << "' (scope: " << scopeDescription << ")"); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << variableName << "' (scope: " << scope.description << ")"); } } else if (typeStructure.is_object()) { - STORM_LOG_THROW(typeStructure.count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << variableName << "(scope: " << scopeDescription << ") kind must be given"); - std::string kind = getString(typeStructure.at("kind"), "kind for complex type as in variable " + variableName + "(scope: " + scopeDescription + ") "); + STORM_LOG_THROW(typeStructure.count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << variableName << "(scope: " << scope.description << ") kind must be given"); + std::string kind = getString(typeStructure.at("kind"), "kind for complex type as in variable " + variableName + "(scope: " + scope.description + ") "); if (kind == "bounded") { - STORM_LOG_THROW(typeStructure.count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scopeDescription << ") lower-bound must be given"); - storm::expressions::Expression lowerboundExpr = parseExpression(typeStructure.at("lower-bound"), "Lower bound for variable " + variableName + " (scope: " + scopeDescription + ")", globalVars, constants, localVars); + STORM_LOG_THROW(typeStructure.count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scope.description << ") lower-bound must be given"); + storm::expressions::Expression lowerboundExpr = parseExpression(typeStructure.at("lower-bound"), scope.refine("Lower bound for variable " + variableName)); assert(lowerboundExpr.isInitialized()); - STORM_LOG_THROW(typeStructure.count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scopeDescription << ") upper-bound must be given"); - storm::expressions::Expression upperboundExpr = parseExpression(typeStructure.at("upper-bound"), "Upper bound for variable "+ variableName + " (scope: " + scopeDescription + ")", globalVars, constants, localVars); + STORM_LOG_THROW(typeStructure.count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scope.description << ") upper-bound must be given"); + storm::expressions::Expression upperboundExpr = parseExpression(typeStructure.at("upper-bound"), scope.refine("Upper bound for variable "+ variableName)); assert(upperboundExpr.isInitialized()); - STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scopeDescription << ") base must be given"); - std::string basictype = getString(typeStructure.at("base"), "base for bounded type as in variable " + variableName + "(scope: " + scopeDescription + ") "); + STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scope.description << ") base must be given"); + std::string basictype = getString(typeStructure.at("base"), "base for bounded type as in variable " + variableName + "(scope: " + scope.description + ") "); if (basictype == "int") { - STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << variableName << "(scope: " << scopeDescription << ") must be integer-typed"); - STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << variableName << "(scope: " << scopeDescription << ") must be integer-typed"); + STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << variableName << "(scope: " << scope.description << ") must be integer-typed"); + STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << variableName << "(scope: " << scope.description << ") must be integer-typed"); if (!lowerboundExpr.containsVariables() && !upperboundExpr.containsVariables()) { - STORM_LOG_THROW(lowerboundExpr.evaluateAsInt() <= upperboundExpr.evaluateAsInt(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable " << variableName << "(scope: " << scopeDescription << ")"); + STORM_LOG_THROW(lowerboundExpr.evaluateAsInt() <= upperboundExpr.evaluateAsInt(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable " << variableName << "(scope: " << scope.description << ")"); } result.basicType = ParsedType::BasicType::Int; + result.expressionType = expressionManager->getIntegerType(); result.bounds = std::make_pair(lowerboundExpr, upperboundExpr); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << variableName << "(scope: " << scopeDescription << ") "); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << variableName << "(scope: " << scope.description << ") "); } } else if (kind == "array") { - STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For array type as in variable " << variableName << "(scope: " << scopeDescription << ") base must be given"); + STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For array type as in variable " << variableName << "(scope: " << scope.description << ") base must be given"); result.arrayBase = std::make_unique(); - parseType(*result.arrayBase, typeStructure.at("base"), variableName, scopeDescription, globalVars, constants, localVars); + parseType(*result.arrayBase, typeStructure.at("base"), variableName, scope); + result.expressionType = expressionManager->getArrayType(result.arrayBase->expressionType); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << variableName << "(scope: " << scopeDescription << ") "); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << variableName << "(scope: " << scope.description << ") "); } } } - std::shared_ptr JaniParser::parseVariable(json const& variableStructure, bool requireInitialValues, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap 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"); + storm::jani::FunctionDefinition JaniParser::parseFunctionDefinition(json const& functionDefinitionStructure, Scope const& scope, std::string const& parameterNamePrefix) { + STORM_LOG_THROW(functionDefinitionStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Function definition (scope: " + scope.description + ") must have a name"); + std::string functionName = getString(functionDefinitionStructure.at("name"), "function-name in " + scope.description); + // TODO check existence of name. + STORM_LOG_THROW(functionDefinitionStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) type-declaration."); + ParsedType type; + parseType(type, functionDefinitionStructure.at("type"), functionName, scope); + + std::unordered_map parameterNameToVariableMap; + std::vector parameters; + if (functionDefinitionStructure.count("parameters")) { + STORM_LOG_THROW(functionDefinitionStructure.count("parameters") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have exactly one list of parameters."); + for (auto const& parameterStructure : functionDefinitionStructure.at("parameters")) { + STORM_LOG_THROW(parameterStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Parameter declaration of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ") must have a name"); + std::string parameterName = getString(functionDefinitionStructure.at("name"), "parameter-name of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ")"); + ParsedType parameterType; + STORM_LOG_THROW(functionDefinitionStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Parameter declaration of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ") must have exactly one type."); + parseType(parameterType, parameterStructure.at("type"), parameterName, scope.refine("parameter declaration of parameter " + std::to_string(parameters.size()) + " of function definition " + functionName)); + STORM_LOG_WARN_COND(!parameterType.bounds.is_initialized(), "Bounds on parameter" + parameterName + " of function definition " + functionName + " will be ignored."); + + std::string exprParameterName = parameterNamePrefix + functionName + VARIABLE_AUTOMATON_DELIMITER + parameterName; + parameters.push_back(expressionManager->declareVariable(exprParameterName, parameterType.expressionType)); + parameterNameToVariableMap.emplace(parameterName, parameters.back()); + } + } + + STORM_LOG_THROW(functionDefinitionStructure.count("body") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have a (single) body."); + storm::expressions::Expression functionBody = parseExpression(functionDefinitionStructure.at("body"), scope.refine("body of function definition " + functionName), false, parameterNameToVariableMap); + STORM_LOG_WARN_COND(functionBody.getType() == type.expressionType, "Type of body of function " + functionName + "' (scope: " + scope.description + ") has type " << functionBody.getType() << " although the function type is given as " << type.expressionType); + + return storm::jani::FunctionDefinition(functionName, type.expressionType, parameters, functionBody); + } + + + std::shared_ptr JaniParser::parseVariable(json const& variableStructure, bool requireInitialValues, Scope const& scope, std::string const& namePrefix) { + STORM_LOG_THROW(variableStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Variable (scope: " + scope.description + ") must have a name"); + std::string name = getString(variableStructure.at("name"), "variable-name in " + scope.description + "-scope"); // TODO check existance of name. // TODO store prefix in variable. - std::string exprManagerName = pref + name; + std::string exprManagerName = namePrefix + name; bool transientVar = defaultVariableTransient; // Default value for variables. size_t tvarcount = variableStructure.count("transient"); - STORM_LOG_THROW(tvarcount <= 1, storm::exceptions::InvalidJaniException, "Multiple definitions of transient not allowed in variable '" + name + "' (scope: " + scopeDescription + ") "); + STORM_LOG_THROW(tvarcount <= 1, storm::exceptions::InvalidJaniException, "Multiple definitions of transient not allowed in variable '" + name + "' (scope: " + scope.description + ") "); if(tvarcount == 1) { - transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name + "' (scope: " + scopeDescription + ") "); + transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name + "' (scope: " + scope.description + ") "); } - STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); + STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration."); ParsedType type; - parseType(type, variableStructure.at("type"), name, scopeDescription, globalVars, constants, localVars); + parseType(type, variableStructure.at("type"), name, scope); size_t initvalcount = variableStructure.count("initial-value"); if(transientVar) { - STORM_LOG_THROW(initvalcount == 1, storm::exceptions::InvalidJaniException, "Initial value must be given once for transient variable '" + name + "' (scope: " + scopeDescription + ") "+ name + "' (scope: " + scopeDescription + ") "); + STORM_LOG_THROW(initvalcount == 1, storm::exceptions::InvalidJaniException, "Initial value must be given once for transient variable '" + name + "' (scope: " + scope.description + ") "+ name + "' (scope: " + scope.description + ") "); } else { - STORM_LOG_THROW(initvalcount <= 1, storm::exceptions::InvalidJaniException, "Initial value can be given at most one for variable " + name + "' (scope: " + scopeDescription + ")"); + STORM_LOG_THROW(initvalcount <= 1, storm::exceptions::InvalidJaniException, "Initial value can be given at most one for variable " + name + "' (scope: " + scope.description + ")"); } boost::optional initVal; if (initvalcount == 1 && !variableStructure.at("initial-value").is_null()) { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); + initVal = parseExpression(variableStructure.at("initial-value"), scope.refine("Initial value for variable " + name)); } else { assert(!transientVar); } @@ -750,7 +808,7 @@ namespace storm { initVal = expressionManager->rational(defaultRationalInitialValue); } if (initVal) { - STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational"); + STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scope.description + ") should be a rational"); return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); } else { return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName)); @@ -765,7 +823,7 @@ namespace storm { } } if (initVal) { - STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer"); + STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scope.description + ") should be an integer"); if (type.bounds) { return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, type.bounds->first, type.bounds->second); } else { @@ -784,7 +842,7 @@ namespace storm { initVal = expressionManager->boolean(defaultBooleanInitialValue); } if (initVal) { - STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); + STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scope.description + ") should be a Boolean"); if (transientVar) { labels.insert(name); } @@ -794,7 +852,7 @@ namespace storm { } } } else if (type.arrayBase) { - STORM_LOG_THROW(type.arrayBase->basicType, storm::exceptions::InvalidJaniException, "Array base type for variable " + name + "(scope " + scopeDescription + ") should be a BasicType or a BoundedType."); + STORM_LOG_THROW(type.arrayBase->basicType, storm::exceptions::InvalidJaniException, "Array base type for variable " + name + "(scope " + scope.description + ") should be a BasicType or a BoundedType."); storm::jani::ArrayVariable::ElementType elementType; storm::expressions::Type exprVariableType; switch (type.arrayBase->basicType.get()) { @@ -818,7 +876,7 @@ namespace storm { } std::shared_ptr result; if (initVal) { - STORM_LOG_THROW(initVal->getType().isArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scopeDescription + ") should be an Array"); + STORM_LOG_THROW(initVal->getType().isArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scope.description + ") should be an Array"); result = std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType, initVal.get(), transientVar); } else { result = std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType); @@ -829,7 +887,7 @@ namespace storm { return result; } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")"); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scope.description << ")"); } /** @@ -839,14 +897,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, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars,returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, Scope const& scope, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), scope.refine("Argument of operator " + opstring), returnNoneInitializedOnUnknownOperator, auxiliaryVariables); return {left}; } - std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); - storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, Scope const& scope, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), scope.refine("Left argument of operator " + opstring), returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), scope.refine("Right argument of operator " + opstring), returnNoneInitializedOnUnknownOperator, auxiliaryVariables); return {left, right}; } /** @@ -877,65 +935,65 @@ namespace storm { STORM_LOG_THROW(expr.getType().isArrayType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be of type 'array' in " << errorInfo << "."); } - storm::jani::LValue JaniParser::parseLValue(json const& lValueStructure, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars) { + storm::jani::LValue JaniParser::parseLValue(json const& lValueStructure, Scope const& scope) { if (lValueStructure.is_string()) { - std::string ident = getString(lValueStructure, scopeDescription); - auto localVar = localVars.find(ident); - if (localVar != localVars.end()) { - return storm::jani::LValue(*localVar->second); - } - auto globalVar = globalVars.find(ident); - if (globalVar != globalVars.end()) { - return storm::jani::LValue(*globalVar->second); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); + std::string ident = getString(lValueStructure, scope.description); + if (scope.localVars != nullptr) { + auto localVar = scope.localVars->find(ident); + if (localVar != scope.localVars->end()) { + return storm::jani::LValue(*localVar->second); + } } + STORM_LOG_THROW(scope.globalVars != nullptr, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scope.description); + auto globalVar = scope.globalVars->find(ident); + STORM_LOG_THROW(globalVar != scope.globalVars->end(), storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scope.description); + return storm::jani::LValue(*globalVar->second); } else if (lValueStructure.count("op") == 1) { - std::string opstring = getString(lValueStructure.at("op"), scopeDescription); - STORM_LOG_THROW(opstring == "aa", storm::exceptions::InvalidJaniException, "Unknown operation '" << opstring << "' occurs in " << scopeDescription); - STORM_LOG_THROW(lValueStructure.count("exp"), storm::exceptions::InvalidJaniException, "Missing 'exp' in array access at " << scopeDescription); - storm::jani::LValue exp = parseLValue(lValueStructure.at("exp"), "LValue description of array expression in " + scopeDescription, globalVars, constants, localVars); - STORM_LOG_THROW(lValueStructure.count("index"), storm::exceptions::InvalidJaniException, "Missing 'index' in array access at " << scopeDescription); - storm::expressions::Expression index = parseExpression(lValueStructure.at("index"), "Index expression of array access at " + scopeDescription, globalVars, constants, localVars); + std::string opstring = getString(lValueStructure.at("op"), scope.description); + STORM_LOG_THROW(opstring == "aa", storm::exceptions::InvalidJaniException, "Unknown operation '" << opstring << "' occurs in " << scope.description); + STORM_LOG_THROW(lValueStructure.count("exp"), storm::exceptions::InvalidJaniException, "Missing 'exp' in array access at " << scope.description); + storm::jani::LValue exp = parseLValue(lValueStructure.at("exp"), scope.refine("LValue description of array expression")); + STORM_LOG_THROW(lValueStructure.count("index"), storm::exceptions::InvalidJaniException, "Missing 'index' in array access at " << scope.description); + storm::expressions::Expression index = parseExpression(lValueStructure.at("index"), scope.refine("Index expression of array access")); return storm::jani::LValue(exp, index); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown LValue '" << lValueStructure.dump() << "' occurs in " << scopeDescription); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown LValue '" << lValueStructure.dump() << "' occurs in " << scope.description); // Silly warning suppression. - return storm::jani::LValue(*localVars.end()->second); + return storm::jani::LValue(*scope.globalVars->end()->second); } } - storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars, std::unordered_map const& auxiliaryVariables) { + storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, Scope const& scope, std::unordered_map const& auxiliaryVariables) { { auto it = auxiliaryVariables.find(ident); if (it != auxiliaryVariables.end()) { return it->second; } } - { - auto it = localVars.find(ident); - if (it != localVars.end()) { + if (scope.localVars != nullptr) { + auto it = scope.localVars->find(ident); + if (it != scope.localVars->end()) { return it->second->getExpressionVariable(); } } - { - auto it = globalVars.find(ident); - if (it != globalVars.end()) { + if (scope.globalVars != nullptr) { + auto it = scope.globalVars->find(ident); + if (it != scope.globalVars->end()) { return it->second->getExpressionVariable(); } } - { - auto it = constants.find(ident); - if (it != constants.end()) { + if (scope.constants != nullptr) { + auto it = scope.constants->find(ident); + if (it != scope.constants->end()) { return it->second->getExpressionVariable(); } } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scope.description); // Silly warning suppression. return storm::expressions::Variable(); } - storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, Scope const& scope, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { if (expressionStructure.is_boolean()) { if (expressionStructure.get()) { return expressionManager->boolean(true); @@ -950,229 +1008,229 @@ namespace storm { return expressionManager->rational(expressionStructure.get()); } else if (expressionStructure.is_string()) { std::string ident = expressionStructure.get(); - return storm::expressions::Expression(getVariableOrConstantExpression(ident, scopeDescription, globalVars, constants, localVars, auxiliaryVariables)); + return storm::expressions::Expression(getVariableOrConstantExpression(ident, scope, auxiliaryVariables)); } 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 << "."); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Distributions are not supported by storm expressions, cannot import " << expressionStructure.dump() << " in " << scope.description << "."); } if (expressionStructure.count("op") == 1) { - std::string opstring = getString(expressionStructure.at("op"), scopeDescription); + std::string opstring = getString(expressionStructure.at("op"), scope.description); std::vector arguments = {}; if(opstring == "ite") { 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, "Then operator required"); - arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables)); - arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables)); - arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables)); - ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription); + arguments.push_back(parseExpression(expressionStructure.at("if"), scope.refine("if-formula"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables)); + arguments.push_back(parseExpression(expressionStructure.at("then"), scope.refine("then-formula"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables)); + arguments.push_back(parseExpression(expressionStructure.at("else"), scope.refine("else-formula"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables)); + ensureNumberOfArguments(3, arguments.size(), opstring, scope.description); assert(arguments.size() == 3); - ensureBooleanType(arguments[0], opstring, 0, scopeDescription); + ensureBooleanType(arguments[0], opstring, 0, scope.description); return storm::expressions::ite(arguments[0], arguments[1], arguments[2]); } else if (opstring == "∨") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } - ensureBooleanType(arguments[0], opstring, 0, scopeDescription); - ensureBooleanType(arguments[1], opstring, 1, scopeDescription); + ensureBooleanType(arguments[0], opstring, 0, scope.description); + ensureBooleanType(arguments[1], opstring, 1, scope.description); return arguments[0] || arguments[1]; } else if (opstring == "∧") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } - ensureBooleanType(arguments[0], opstring, 0, scopeDescription); - ensureBooleanType(arguments[1], opstring, 1, scopeDescription); + ensureBooleanType(arguments[0], opstring, 0, scope.description); + ensureBooleanType(arguments[1], opstring, 1, scope.description); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } - ensureBooleanType(arguments[0], opstring, 0, scopeDescription); - ensureBooleanType(arguments[1], opstring, 1, scopeDescription); + ensureBooleanType(arguments[0], opstring, 0, scope.description); + ensureBooleanType(arguments[1], opstring, 1, scope.description); return (!arguments[0]) || arguments[1]; } else if (opstring == "¬") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); if(!arguments[0].isInitialized()) { return storm::expressions::Expression(); } - ensureBooleanType(arguments[0], opstring, 0, scopeDescription); + ensureBooleanType(arguments[0], opstring, 0, scope.description); return !arguments[0]; } else if (opstring == "=") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } if(arguments[0].hasBooleanType()) { - ensureBooleanType(arguments[1], opstring, 1, scopeDescription); + ensureBooleanType(arguments[1], opstring, 1, scope.description); return storm::expressions::iff(arguments[0], arguments[1]); } else { - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] == arguments[1]; } } else if (opstring == "≠") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } if(arguments[0].hasBooleanType()) { - ensureBooleanType(arguments[1], opstring, 1, scopeDescription); + ensureBooleanType(arguments[1], opstring, 1, scope.description); return storm::expressions::xclusiveor(arguments[0], arguments[1]); } else { - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] != arguments[1]; } } else if (opstring == "<") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] < arguments[1]; } else if (opstring == "≤") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] <= arguments[1]; } else if (opstring == ">") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] > arguments[1]; } else if (opstring == "≥") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); } - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] >= arguments[1]; } else if (opstring == "+") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] + arguments[1]; } else if (opstring == "-") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] - arguments[1]; } else if (opstring == "-") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription,globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); return -arguments[0]; } else if (opstring == "*") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] * arguments[1]; } else if (opstring == "/") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] / arguments[1]; } else if (opstring == "%") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0] % arguments[1]; } else if (opstring == "max") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return storm::expressions::maximum(arguments[0],arguments[1]); } else if (opstring == "min") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return storm::expressions::minimum(arguments[0],arguments[1]); } else if (opstring == "floor") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); return storm::expressions::floor(arguments[0]); } else if (opstring == "ceil") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); return storm::expressions::ceil(arguments[0]); } else if (opstring == "abs") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); return storm::expressions::abs(arguments[0]); } else if (opstring == "sgn") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); return storm::expressions::sign(arguments[0]); } else if (opstring == "trc") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); return storm::expressions::truncate(arguments[0]); } else if (opstring == "pow") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); return arguments[0]^arguments[1]; } else if (opstring == "exp") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); // TODO implement STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "exp operation is not yet implemented"); } else if (opstring == "log") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scope, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); - ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - ensureNumericalType(arguments[1], opstring, 1, scopeDescription); + ensureNumericalType(arguments[0], opstring, 0, scope.description); + ensureNumericalType(arguments[1], opstring, 1, scope.description); // TODO implement STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "log operation is not yet implemented"); } else if (opstring == "aa") { - STORM_LOG_THROW(expressionStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one exp (at " + scopeDescription + ")."); - storm::expressions::Expression exp = parseExpression(expressionStructure.at("exp"), "exp in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); - STORM_LOG_THROW(expressionStructure.count("index") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one index (at " + scopeDescription + ")."); - storm::expressions::Expression index = parseExpression(expressionStructure.at("index"), "index in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); - ensureArrayType(exp, opstring, 0, scopeDescription); - ensureIntegerType(index, opstring, 1, scopeDescription); + STORM_LOG_THROW(expressionStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one exp (at " + scope.description + ")."); + storm::expressions::Expression exp = parseExpression(expressionStructure.at("exp"), scope.refine("'exp' of array access operator"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + STORM_LOG_THROW(expressionStructure.count("index") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one index (at " + scope.description + ")."); + storm::expressions::Expression index = parseExpression(expressionStructure.at("index"), scope.refine("index of array access operator"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + ensureArrayType(exp, opstring, 0, scope.description); + ensureIntegerType(index, opstring, 1, scope.description); return std::make_shared(exp.getManager(), exp.getType().getElementType(), exp.getBaseExpressionPointer(), index.getBaseExpressionPointer())->toExpression(); } else if (opstring == "av") { - STORM_LOG_THROW(expressionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Array value operator requires exactly one 'elements' (at " + scopeDescription + ")."); + STORM_LOG_THROW(expressionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Array value operator requires exactly one 'elements' (at " + scope.description + ")."); std::vector> elements; storm::expressions::Type commonType; bool first = true; for (auto const& element : expressionStructure.at("elements")) { - elements.push_back(parseExpression(element, "element " + std::to_string(elements.size()) + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables).getBaseExpressionPointer()); + elements.push_back(parseExpression(element, scope.refine("element " + std::to_string(elements.size()) + " of array value expression"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables).getBaseExpressionPointer()); if (first) { commonType = elements.back()->getType(); first = false; @@ -1180,37 +1238,56 @@ namespace storm { if (commonType.isIntegerType() && elements.back()->getType().isRationalType()) { commonType = elements.back()->getType(); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Incompatible element types " << commonType << " and " << elements.back()->getType() << " of array value expression at " << scopeDescription); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Incompatible element types " << commonType << " and " << elements.back()->getType() << " of array value expression at " << scope.description); } } } return std::make_shared(*expressionManager, expressionManager->getArrayType(commonType), elements)->toExpression(); } else if (opstring == "ac") { - STORM_LOG_THROW(expressionStructure.count("length") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one length (at " + scopeDescription + ")."); - storm::expressions::Expression length = parseExpression(expressionStructure.at("length"), "index in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); - ensureIntegerType(length, opstring, 1, scopeDescription); - STORM_LOG_THROW(expressionStructure.count("var") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one var (at " + scopeDescription + ")."); - std::string indexVarName = getString(expressionStructure.at("var"), "Field 'var' of Array access operator (at " + scopeDescription + ")."); - STORM_LOG_THROW(auxiliaryVariables.find(indexVarName) == auxiliaryVariables.end(), storm::exceptions::InvalidJaniException, "Index variable " << indexVarName << " is already defined as an auxiliary variable (at " + scopeDescription + ")."); + STORM_LOG_THROW(expressionStructure.count("length") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one length (at " + scope.description + ")."); + storm::expressions::Expression length = parseExpression(expressionStructure.at("length"), scope.refine("index of array constructor expression"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables); + ensureIntegerType(length, opstring, 1, scope.description); + STORM_LOG_THROW(expressionStructure.count("var") == 1, storm::exceptions::InvalidJaniException, "Array access operator requires exactly one var (at " + scope.description + ")."); + std::string indexVarName = getString(expressionStructure.at("var"), "Field 'var' of Array access operator (at " + scope.description + ")."); + STORM_LOG_THROW(auxiliaryVariables.find(indexVarName) == auxiliaryVariables.end(), storm::exceptions::InvalidJaniException, "Index variable " << indexVarName << " is already defined as an auxiliary variable (at " + scope.description + ")."); auto newAuxVars = auxiliaryVariables; storm::expressions::Variable indexVar = expressionManager->declareFreshIntegerVariable(false, "ac_" + indexVarName); newAuxVars.emplace(indexVarName, indexVar); - STORM_LOG_THROW(expressionStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Array constructor operator requires exactly one exp (at " + scopeDescription + ")."); - storm::expressions::Expression exp = parseExpression(expressionStructure.at("exp"), "exp of array constructor in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, newAuxVars); + STORM_LOG_THROW(expressionStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Array constructor operator requires exactly one exp (at " + scope.description + ")."); + storm::expressions::Expression exp = parseExpression(expressionStructure.at("exp"), scope.refine("exp of array constructor"), returnNoneInitializedOnUnknownOperator, newAuxVars); return std::make_shared(*expressionManager, expressionManager->getArrayType(exp.getType()), length.getBaseExpressionPointer(), indexVar, exp.getBaseExpressionPointer())->toExpression(); - } else if (unsupportedOpstrings.count(opstring) > 0){ + } else if (opstring == "call") { + STORM_LOG_THROW(expressionStructure.count("function") == 1, storm::exceptions::InvalidJaniException, "Function call operator requires exactly one function (at " + scope.description + ")."); + std::string functionName = getString(expressionStructure.at("function"), "in function call operator (at " + scope.description + ")."); + storm::jani::FunctionDefinition const* functionDefinition; + if (scope.localFunctions != nullptr && scope.localFunctions->count(functionName) > 0) { + functionDefinition = scope.localFunctions->at(functionName); + } else if (scope.globalFunctions != nullptr && scope.globalFunctions->count(functionName) > 0){ + functionDefinition = scope.globalFunctions->at(functionName); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Function call operator calls unknown function '" + functionName + "' (at " + scope.description + ")."); + } + STORM_LOG_THROW(expressionStructure.count("args") == 1, storm::exceptions::InvalidJaniException, "Function call operator requires exactly one args (at " + scope.description + ")."); + std::vector> args; + if (expressionStructure.count("args") > 0) { + STORM_LOG_THROW(expressionStructure.count("args") == 1, storm::exceptions::InvalidJaniException, "Function call operator requires exactly one args (at " + scope.description + ")."); + for (auto const& arg : expressionStructure.at("args")) { + args.push_back(parseExpression(arg, scope.refine("argument " + std::to_string(args.size()) + " of function call expression"), returnNoneInitializedOnUnknownOperator, auxiliaryVariables).getBaseExpressionPointer()); + } + } + return std::make_shared(*expressionManager, functionDefinition->getType(), functionName, args)->toExpression(); + } else if (unsupportedOpstrings.count(opstring) > 0) { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Opstring " + opstring + " is not supported by storm"); - } else { if(returnNoneInitializedOnUnknownOperator) { return storm::expressions::Expression(); } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scopeDescription << "."); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scope.description << "."); } } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported operator declaration found for complex expressions as " << expressionStructure.dump() << " in " << scopeDescription << "."); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported operator declaration found for complex expressions as " << expressionStructure.dump() << " in " << scope.description << "."); } - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported expression found at " << expressionStructure.dump() << " in " << scopeDescription << "."); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported expression found at " << expressionStructure.dump() << " in " << scope.description << "."); // Silly warning suppression. return storm::expressions::Expression(); @@ -1227,23 +1304,37 @@ namespace storm { } } - storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure, storm::jani::Model const& parentModel, VariablesMap const& globalVars, ConstantsMap const& constants ) { + storm::jani::Automaton JaniParser::parseAutomaton(json const &automatonStructure, storm::jani::Model const& parentModel, Scope const& globalScope) { 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"); + Scope scope = globalScope.refine(name); 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"); VariablesMap localVars; - if(varDeclCount > 0) { + scope.localVars = &localVars; + if (varDeclCount > 0) { bool requireInitialValues = automatonStructure.count("restrict-initial") == 0; for(auto const& varStructure : automatonStructure.at("variables")) { - std::shared_ptr var = parseVariable(varStructure, requireInitialValues, name, globalVars, constants, localVars, true); + std::shared_ptr var = parseVariable(varStructure, requireInitialValues, scope.refine("variables[" + std::to_string(localVars.size()) + "] of automaton " + name), name + VARIABLE_AUTOMATON_DELIMITER); assert(localVars.count(var->getName()) == 0); localVars.emplace(var->getName(), &automaton.addVariable(*var)); } } + uint64_t funDeclCount = automatonStructure.count("functions"); + STORM_LOG_THROW(funDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of functions"); + FunctionsMap localFuns; + scope.localFunctions = &localFuns; + if (funDeclCount > 0) { + for (auto const& funStructure : automatonStructure.at("functions")) { + storm::jani::FunctionDefinition funDef = parseFunctionDefinition(funStructure, scope.refine("functions[" + std::to_string(localFuns.size()) + "] of automaton " + name), name + VARIABLE_AUTOMATON_DELIMITER); + assert(localFuns.count(funDef.getName()) == 0); + //TODO localVars.emplace(funDef.getName(), &automaton.addFunction(funDef)); + } + } + 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")) { @@ -1257,9 +1348,9 @@ namespace storm { for(auto const& transientValueEntry : locEntry.at("transient-values")) { STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to"); STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value"); - storm::jani::LValue lValue = parseLValue(transientValueEntry.at("ref"), "LHS of assignment in location " + locName + " (automaton '" + name + "')", globalVars, constants, localVars); + storm::jani::LValue lValue = parseLValue(transientValueEntry.at("ref"), scope.refine("LHS of assignment in location " + locName)); STORM_LOG_THROW(lValue.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " << lValue << " in location " + locName + " (automaton: '" + name + "')"); - storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of lValue in location " + locName + " (automaton: '" + name + "')", globalVars, constants, localVars); + storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), scope.refine("Assignment of lValue in location " + locName)); transientAssignments.emplace_back(lValue, rhs); } } @@ -1274,12 +1365,11 @@ 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, globalVars, constants, localVars); + initialValueRestriction = parseExpression(automatonStructure.at("restrict-initial").at("exp"), scope.refine("Initial value restriction")); } automaton.setInitialStatesRestriction(initialValueRestriction); - STORM_LOG_THROW(automatonStructure.count("edges") > 0, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' must have a list of edges"); for(auto const& edgeEntry : automatonStructure.at("edges")) { // source location @@ -1299,7 +1389,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 + "'", globalVars, constants, localVars); + rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), scope.refine("rate expression in edge from '" + sourceLoc)); STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type"); } // guard @@ -1307,7 +1397,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 + "'", globalVars, constants, localVars); + guardExpr = parseExpression(edgeEntry.at("guard").at("exp"), scope.refine("guard expression in edge from '" + sourceLoc)); STORM_LOG_THROW(guardExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Guard " << guardExpr << " does not have Boolean type."); } assert(guardExpr.isInitialized()); @@ -1329,7 +1419,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 + "'", globalVars, constants, localVars); + probExpr = parseExpression(destEntry.at("probability").at("exp"), scope.refine("probability expression in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'")); } assert(probExpr.isInitialized()); STORM_LOG_THROW(probExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Probability expression " << probExpr << " does not have a numerical type." ); @@ -1341,10 +1431,10 @@ namespace storm { for (auto const& assignmentEntry : destEntry.at("assignments")) { // ref STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field"); - storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); + storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), scope.refine("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 + "'", globalVars, constants, localVars); + storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), scope.refine("assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'")); // TODO check types // index int64_t assignmentIndex = 0; // default. diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index e6cf5f069..7716126a2 100644 --- a/src/storm-parsers/parser/JaniParser.h +++ b/src/storm-parsers/parser/JaniParser.h @@ -1,5 +1,6 @@ #pragma once #include "storm/storage/jani/Constant.h" +#include "storm/storage/jani/FunctionDefinition.h" #include "storm/storage/jani/LValue.h" #include "storm/logic/Formula.h" #include "storm/logic/Bound.h" @@ -32,8 +33,6 @@ namespace storm { /* * The JANI format parser. * Parses Models and Properties - * - * TODO some parts are copy-heavy, a bit of cleaning is good as soon as the format is stable. */ class JaniParser { @@ -41,48 +40,75 @@ namespace storm { typedef std::vector PropertyVector; typedef std::unordered_map VariablesMap; typedef std::unordered_map ConstantsMap; + typedef std::unordered_map FunctionsMap; JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); static std::pair> parse(std::string const& path); - protected: void readFile(std::string const& path); + + struct Scope { + Scope(std::string description = "global", ConstantsMap const* constants = nullptr, VariablesMap const* globalVars = nullptr, FunctionsMap const* globalFunctions = nullptr, VariablesMap const* localVars = nullptr, FunctionsMap const* localFunctions = nullptr) : description(description) , constants(constants), globalVars(globalVars), globalFunctions(globalFunctions), localVars(localVars), localFunctions(localFunctions) {}; + + Scope(Scope const& other) = default; + std::string description; + ConstantsMap const* constants; + VariablesMap const* globalVars; + FunctionsMap const* globalFunctions; + VariablesMap const* localVars; + FunctionsMap const* localFunctions; + Scope refine(std::string const& prependedDescription = "") const { + Scope res(*this); + if (prependedDescription != "") { + res.description = "'" + prependedDescription + "' at " + res.description; + } + return res; + } + + Scope& clearVariables() { + this->globalVars = nullptr; + this->localVars = nullptr; + return *this; + } + }; + std::pair> parseModel(bool parseProperties = true); - storm::jani::Property parseProperty(json const& propertyStructure, VariablesMap const& globalVars, ConstantsMap const& constants); - storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, VariablesMap const& globalVars, ConstantsMap const& constants); + storm::jani::Property parseProperty(json const& propertyStructure, Scope const& scope); + storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, Scope const& scope); struct ParsedType { enum class BasicType {Bool, Int, Real}; boost::optional basicType; boost::optional> bounds; std::unique_ptr arrayBase; + storm::expressions::Type expressionType; }; - void parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars); - storm::jani::LValue parseLValue(json const& lValueStructure, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars = {}); - std::shared_ptr parseVariable(json const& variableStructure, bool requireInitialValues, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars = {}, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); + void parseType(ParsedType& result, json const& typeStructure, std::string variableName, Scope const& scope); + storm::jani::LValue parseLValue(json const& lValueStructure, Scope const& scope); + std::shared_ptr parseVariable(json const& variableStructure, bool requireInitialValues, Scope const& scope, std::string const& namePrefix = ""); + storm::expressions::Expression parseExpression(json const& expressionStructure, Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); private: - std::shared_ptr parseConstant(json const& constantStructure, ConstantsMap const& constants, std::string const& scopeDescription = "global"); + std::shared_ptr parseConstant(json const& constantStructure, Scope const& scope); + storm::jani::FunctionDefinition parseFunctionDefinition(json const& functionDefinitionStructure, Scope const& scope, std::string const& parameterNamePrefix = ""); /** * 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, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context, boost::optional bound = boost::none); - std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars= {}, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); - std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); + std::shared_ptr parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, Scope const& scope, boost::optional bound = boost::none); + std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); + std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, Scope const& scope, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); - std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context); - std::vector> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, VariablesMap const& globalVars, ConstantsMap const& constants, std::string const& context); - storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, ConstantsMap const& constants); + std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope); + std::vector> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope); + storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, Scope const& scope); storm::logic::RewardAccumulation parseRewardAccumulation(json const& accStructure, std::string const& context); - std::shared_ptr parseComposition(json const& compositionStructure); - storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, VariablesMap const& globalVars, ConstantsMap const& constants, VariablesMap const& localVars = {}, std::unordered_map const& auxiliaryVariables = {}); + storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, Scope const& scope, std::unordered_map const& auxiliaryVariables = {}); diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 14a1e7b2f..c1b375b2b 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -85,6 +85,20 @@ namespace storm { return variables.hasTransientVariable(); } + FunctionDefinition const& Automaton::addFunctionDefinition(FunctionDefinition const& functionDefinition) { + auto insertionRes = functionDefinitions.emplace(functionDefinition.getName(), functionDefinition); + STORM_LOG_THROW(insertionRes.second, storm::exceptions::InvalidArgumentException, " a function with the name " << functionDefinition.getName() << " already exists in this automaton (" << this->getName() << ")"); + return insertionRes.first->second; + } + + std::unordered_map const& Automaton::getFunctionDefinitions() const { + return functionDefinitions; + } + + std::unordered_map Automaton::getFunctionDefinitions() { + return functionDefinitions; + } + bool Automaton::hasLocation(std::string const& name) const { return locationToIndex.find(name) != locationToIndex.end(); } @@ -385,6 +399,9 @@ namespace storm { for (auto& variable : this->getVariables().getBoundedIntegerVariables()) { variable.substitute(substitution); } + for (auto& variable : this->getVariables().getArrayVariables()) { + variable.substitute(substitution); + } for (auto& location : this->getLocations()) { location.substitute(substitution); diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index c6422fb1a..ed67d2efc 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -9,7 +9,7 @@ #include "storm/storage/jani/VariableSet.h" #include "storm/storage/jani/TemplateEdgeContainer.h" #include "storm/storage/jani/EdgeContainer.h" - +#include "storm/storage/jani/FunctionDefinition.h" namespace storm { namespace jani { @@ -99,6 +99,21 @@ namespace storm { */ bool hasTransientVariable() const; + /*! + * Adds the given function definition + */ + FunctionDefinition const& addFunctionDefinition(FunctionDefinition const& functionDefinition); + + /*! + * Retrieves all function definitions of this automaton + */ + std::unordered_map const& getFunctionDefinitions() const; + + /*! + * Retrieves all function definitions of this automaton + */ + std::unordered_map getFunctionDefinitions(); + /*! * Retrieves whether the automaton has a location with the given name. */ @@ -356,6 +371,9 @@ namespace storm { /// The set of variables of this automaton. VariableSet variables; + /// A mapping from names to function definitions + std::unordered_map functionDefinitions; + /// The locations of the automaton. std::vector locations; diff --git a/src/storm/storage/jani/FunctionDefinition.cpp b/src/storm/storage/jani/FunctionDefinition.cpp new file mode 100644 index 000000000..2bac96f91 --- /dev/null +++ b/src/storm/storage/jani/FunctionDefinition.cpp @@ -0,0 +1,30 @@ +#include "storm/storage/jani/FunctionDefinition.h" + +namespace storm { + namespace jani { + + FunctionDefinition::FunctionDefinition(std::string const& name, storm::expressions::Type const& type, std::vector const& parameters, storm::expressions::Expression const& functionBody) : name(name), type(type), parameters(parameters), functionBody(functionBody) { + // Intentionally left empty. + } + + std::string const& FunctionDefinition::getName() const { + return name; + } + + storm::expressions::Type const& FunctionDefinition::getType() const { + return type; + } + + std::vector const& FunctionDefinition::getParameters() const { + return parameters; + } + + storm::expressions::Expression const& FunctionDefinition::getFunctionBody() const { + return functionBody; + } + + void FunctionDefinition::setFunctionBody(storm::expressions::Expression const& body) { + functionBody = body; + } + } +} diff --git a/src/storm/storage/jani/FunctionDefinition.h b/src/storm/storage/jani/FunctionDefinition.h new file mode 100644 index 000000000..51eabf937 --- /dev/null +++ b/src/storm/storage/jani/FunctionDefinition.h @@ -0,0 +1,61 @@ +#pragma once + +#include +#include + +#include + +#include "storm/storage/expressions/Variable.h" +#include "storm/storage/expressions/Expression.h" + +namespace storm { + namespace jani { + + class FunctionDefinition { + public: + /*! + * Creates a functionDefinition. + */ + FunctionDefinition(std::string const& name, storm::expressions::Type const& type, std::vector const& parameters, storm::expressions::Expression const& functionBody); + + /*! + * Retrieves the name of the function. + */ + std::string const& getName() const; + + /*! + * Retrieves the type of the function. + */ + storm::expressions::Type const& getType() const; + + /*! + * Retrieves the parameters of the function + */ + std::vector const& getParameters() const; + + /*! + * Retrieves the expression that defines the function + */ + storm::expressions::Expression const& getFunctionBody() const; + + /*! + * sets the expression that defines the function + */ + void setFunctionBody(storm::expressions::Expression const& body); + + private: + // The name of the function. + std::string name; + + // The type of the function + storm::expressions::Type type; + + // The parameters + std::vector parameters; + + // The body of the function + storm::expressions::Expression functionBody; + }; + + } +} diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 3da43c78b..4bfb71e03 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -36,9 +36,9 @@ namespace storm { namespace jani { - modernjson::json buildExpression(storm::expressions::Expression const& exp, std::vector const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet()) { + modernjson::json buildExpression(storm::expressions::Expression const& exp, std::vector const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet(), std::unordered_set const& auxiliaryVariables = {}) { STORM_LOG_TRACE("Exporting " << exp); - return ExpressionToJson::translate(exp, constants, globalVariables, localVariables); + return ExpressionToJson::translate(exp, constants, globalVariables, localVariables, auxiliaryVariables); } class CompositionJsonExporter : public CompositionVisitor { @@ -616,13 +616,13 @@ namespace storm { } } - modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { + modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set const& auxiliaryVariables) { // Simplify the expression first and reduce the nesting auto simplifiedExpr = expr.simplify().reduceNesting(); - ExpressionToJson visitor(constants, globalVariables, localVariables); + ExpressionToJson visitor(constants, globalVariables, localVariables, auxiliaryVariables); return boost::any_cast(simplifiedExpr.accept(visitor, boost::none)); } @@ -657,7 +657,9 @@ namespace storm { return opDecl; } boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const&) { - if (globalVariables.hasVariable(expression.getVariable())) { + if (auxiliaryVariables.count(expression.getVariableName())) { + return modernjson::json(expression.getVariableName()); + } else if (globalVariables.hasVariable(expression.getVariable())) { return modernjson::json(globalVariables.getVariable(expression.getVariable()).getName()); } else if (localVariables.hasVariable(expression.getVariable())) { return modernjson::json(localVariables.getVariable(expression.getVariable()).getName()); @@ -701,7 +703,7 @@ namespace storm { for (uint64_t i = 0; i < size; ++i) { elements.push_back(boost::any_cast(expression.at(i)->accept(*this, data))); } - opDecl["elements"] = elements; + opDecl["elements"] = std::move(elements); return opDecl; } @@ -710,7 +712,11 @@ namespace storm { opDecl["op"] = "ac"; opDecl["var"] = expression.getIndexVar().getName(); opDecl["length"] = boost::any_cast(expression.size()->accept(*this, data)); + bool inserted = auxiliaryVariables.insert(expression.getIndexVar().getName()).second; opDecl["exp"] = boost::any_cast(expression.getElementExpression()->accept(*this, data)); + if (inserted) { + auxiliaryVariables.erase(expression.getIndexVar().getName()); + } return opDecl; } @@ -722,6 +728,18 @@ namespace storm { return opDecl; } + boost::any ExpressionToJson::visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) { + modernjson::json opDecl; + opDecl["op"] = "call"; + opDecl["function"] = expression.getIdentifier(); + std::vector arguments; + for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) { + arguments.push_back(boost::any_cast(expression.getArgument(i)->accept(*this, data))); + } + opDecl["args"] = std::move(arguments); + return opDecl; + } + void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector const& formulas, std::string const& filepath, bool checkValid, bool compact) { std::ofstream stream; storm::utility::openFile(filepath, stream); @@ -832,16 +850,54 @@ namespace storm { } break; } - typeDesc["base"] = "int"; } varEntry["type"] = typeDesc; - if(variable.hasInitExpression()) { + if (variable.hasInitExpression()) { varEntry["initial-value"] = buildExpression(variable.getInitExpression(), constants, globalVariables, localVariables); } variableDeclarations.push_back(varEntry); } return modernjson::json(variableDeclarations); - + } + + modernjson::json buildTypeDescription(storm::expressions::Type const& type) { + modernjson::json typeDescr; + if (type.isIntegerType()) { + typeDescr = "int"; + } else if (type.isRationalType()) { + typeDescr = "real"; + } else if (type.isBooleanType()) { + typeDescr = "bool"; + } else if (type.isArrayType()) { + typeDescr["kind"] = "array"; + typeDescr["base"] = buildTypeDescription(type.getElementType()); + } else { + assert(false); + } + return typeDescr; + } + + modernjson::json buildFunctionsArray(std::unordered_map const& functionDefinitions, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables = VariableSet()) { + std::vector functionDeclarations; + for (auto const& nameFunDef : functionDefinitions) { + storm::jani::FunctionDefinition const& funDef = nameFunDef.second; + modernjson::json funDefJson; + funDefJson["name"] = nameFunDef.first; + funDefJson["type"] = buildTypeDescription(funDef.getType()); + std::vector parameterDeclarations; + std::unordered_set parameterNames; + for (auto const& p : funDef.getParameters()) { + modernjson::json parDefJson; + parDefJson["name"] = p.getName(); + parameterNames.insert(p.getName()); + parDefJson["type"] = buildTypeDescription(p.getType()); + parameterDeclarations.push_back(parDefJson); + } + funDefJson["parameters"] = parameterDeclarations; + funDefJson["body"] = buildExpression(funDef.getFunctionBody(), constants, globalVariables, localVariables, parameterNames); + functionDeclarations.push_back(funDefJson); + } + return modernjson::json(functionDeclarations); } modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { @@ -868,7 +924,7 @@ namespace storm { assignmentEntry["comment"] = assignment.getVariable().getName() + " <- " + assignment.getAssignedExpression().toString(); } } - return modernjson::json(assignmentDeclarations); + return modernjson::json(std::move(assignmentDeclarations)); } modernjson::json buildLocationsArray(std::vector const& locations, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { @@ -882,7 +938,7 @@ namespace storm { } locationDeclarations.push_back(locEntry); } - return modernjson::json(locationDeclarations); + return modernjson::json(std::move(locationDeclarations)); } modernjson::json buildInitialLocations(storm::jani::Automaton const& automaton) { @@ -916,7 +972,7 @@ namespace storm { } destDeclarations.push_back(destEntry); } - return modernjson::json(destDeclarations); + return modernjson::json(std::move(destDeclarations)); } modernjson::json buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { @@ -950,7 +1006,7 @@ namespace storm { edgeDeclarations.push_back(edgeEntry); } - return modernjson::json(edgeDeclarations); + return modernjson::json(std::move(edgeDeclarations)); } modernjson::json buildAutomataArray(std::vector const& automata, std::map const& actionNames, std::vector const& constants, VariableSet const& globalVariables, bool commentExpressions) { @@ -967,7 +1023,7 @@ namespace storm { autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap(), constants, globalVariables, automaton.getVariables(), commentExpressions); automataDeclarations.push_back(autoEntry); } - return modernjson::json(automataDeclarations); + return modernjson::json(std::move(automataDeclarations)); } void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) { diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index ce95a2c0f..1e6eefb50 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -19,7 +19,7 @@ namespace storm { class ExpressionToJson : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor { public: - static modernjson::json translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables); + static modernjson::json translate(storm::expressions::Expression const& expr, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set const& auxiliaryVariables); virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data); virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data); @@ -34,13 +34,15 @@ namespace storm { virtual boost::any visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data); virtual boost::any visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data); virtual boost::any visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data); + virtual boost::any visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data); private: - ExpressionToJson(std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) : constants(constants), globalVariables(globalVariables), localVariables(localVariables) {} + ExpressionToJson(std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, std::unordered_set const& auxiliaryVariables) : constants(constants), globalVariables(globalVariables), localVariables(localVariables), auxiliaryVariables(auxiliaryVariables) {} std::vector const& constants; VariableSet const& globalVariables; VariableSet const& localVariables; + std::unordered_set auxiliaryVariables; }; class FormulaToJaniJson : public storm::logic::FormulaVisitor { diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index d84762fc7..e983cccab 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -82,6 +82,7 @@ namespace storm { this->automatonToIndex = other.automatonToIndex; this->composition = other.composition; this->initialStatesRestriction = other.initialStatesRestriction; + this->globalFunctions = other.globalFunctions; // Now that we have copied all the data, we need to fix all assignments as they contain references to the old model. std::map> remapping; @@ -725,6 +726,20 @@ namespace storm { return false; } + FunctionDefinition const& Model::addFunctionDefinition(FunctionDefinition const& functionDefinition) { + auto insertionRes = globalFunctions.emplace(functionDefinition.getName(), functionDefinition); + STORM_LOG_THROW(insertionRes.second, storm::exceptions::InvalidOperationException, " a function with the name " << functionDefinition.getName() << " already exists in this model."); + return insertionRes.first->second; + } + + std::unordered_map const& Model::getGlobalFunctionDefinitions() const { + return globalFunctions; + } + + std::unordered_map Model::getGlobalFunctionDefinitions() { + return globalFunctions; + } + storm::expressions::ExpressionManager& Model::getExpressionManager() const { return *expressionManager; } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 274d17490..2f0bbaa72 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -12,6 +12,7 @@ #include "storm/storage/jani/Constant.h" #include "storm/storage/jani/Composition.h" #include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/FunctionDefinition.h" #include "storm/storage/jani/Location.h" #include "storm/storage/jani/TemplateEdge.h" #include "storm/storage/jani/ModelFeatures.h" @@ -248,6 +249,21 @@ namespace storm { */ bool hasNonGlobalTransientVariable() const; + /*! + * Adds the given function definition + */ + FunctionDefinition const& addFunctionDefinition(FunctionDefinition const& functionDefinition); + + /*! + * Retrieves all global function definitions + */ + std::unordered_map const& getGlobalFunctionDefinitions() const; + + /*! + * Retrieves all global function definitions + */ + std::unordered_map getGlobalFunctionDefinitions(); + /*! * Retrieves the manager responsible for the expressions in the JANI model. */ @@ -564,6 +580,9 @@ namespace storm { /// The global variables of the model. VariableSet globalVariables; + /// A mapping from names to function definitions + std::unordered_map globalFunctions; + /// The list of automata. std::vector automata; diff --git a/src/storm/storage/jani/ModelFeatures.cpp b/src/storm/storage/jani/ModelFeatures.cpp index ada96c565..205b7cfc3 100644 --- a/src/storm/storage/jani/ModelFeatures.cpp +++ b/src/storm/storage/jani/ModelFeatures.cpp @@ -11,6 +11,8 @@ namespace storm { return "arrays"; case ModelFeature::DerivedOperators: return "derived-operators"; + case ModelFeature::Functions: + return "functions"; case ModelFeature::StateExitRewards: return "state-exit-rewards"; } @@ -40,6 +42,10 @@ namespace storm { return features.count(ModelFeature::DerivedOperators) > 0; } + bool ModelFeatures::hasFunctions() const { + return features.count(ModelFeature::Functions) > 0; + } + bool ModelFeatures::hasStateExitRewards() const { return features.count(ModelFeature::StateExitRewards) > 0; } diff --git a/src/storm/storage/jani/ModelFeatures.h b/src/storm/storage/jani/ModelFeatures.h index 363ee236c..32b4d3db3 100644 --- a/src/storm/storage/jani/ModelFeatures.h +++ b/src/storm/storage/jani/ModelFeatures.h @@ -6,7 +6,7 @@ namespace storm { namespace jani { - enum class ModelFeature {Arrays, DerivedOperators, StateExitRewards}; + enum class ModelFeature {Arrays, DerivedOperators, Functions, StateExitRewards}; std::string toString(ModelFeature const& modelFeature); @@ -16,6 +16,7 @@ namespace storm { std::string toString() const; bool hasArrays() const; + bool hasFunctions() const; bool hasDerivedOperators() const; bool hasStateExitRewards() const; diff --git a/src/storm/storage/jani/expressions/FunctionCallExpression.cpp b/src/storm/storage/jani/expressions/FunctionCallExpression.cpp new file mode 100644 index 000000000..4ab6d64b4 --- /dev/null +++ b/src/storm/storage/jani/expressions/FunctionCallExpression.cpp @@ -0,0 +1,75 @@ +#include "storm/storage/jani/expressions/FunctionCallExpression.h" + +#include "storm/storage/jani/expressions/JaniExpressionVisitor.h" +#include "storm/storage/expressions/ExpressionManager.h" + +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/UnexpectedException.h" + +namespace storm { + namespace expressions { + + FunctionCallExpression::FunctionCallExpression(ExpressionManager const& manager, Type const& type, std::string const& functionIdentifier, std::vector> const& arguments) : BaseExpression(manager, type), identifier(functionIdentifier), arguments(arguments) { + // Intentionally left empty + } + + void FunctionCallExpression::gatherVariables(std::set& variables) const { + for (auto const& a : arguments) { + a->gatherVariables(variables); + } + } + + bool FunctionCallExpression::containsVariables() const { + for (auto const& a : arguments) { + if (a->containsVariables()) { + return true; + } + } + return false; + } + + std::shared_ptr FunctionCallExpression::simplify() const { + std::vector> simplifiedArguments; + simplifiedArguments.reserve(arguments.size()); + for (auto const& a : arguments) { + simplifiedArguments.push_back(a->simplify()); + } + return std::shared_ptr(new FunctionCallExpression(getManager(), getType(), identifier, simplifiedArguments)); + } + + boost::any FunctionCallExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { + auto janiVisitor = dynamic_cast(&visitor); + STORM_LOG_THROW(janiVisitor != nullptr, storm::exceptions::UnexpectedException, "Visitor of jani expression should be of type JaniVisitor."); + return janiVisitor->visit(*this, data); + } + + void FunctionCallExpression::printToStream(std::ostream& stream) const { + stream << identifier; + if (getNumberOfArguments() > 0) { + stream << "("; + bool first = true; + for (auto const& a : arguments) { + stream << *a; + if (!first) { + stream << ", "; + } + first = false; + } + stream << ")"; + } + } + + std::string const& FunctionCallExpression::getFunctionIdentifier() const { + return identifier; + } + + uint64_t FunctionCallExpression::getNumberOfArguments() const { + return arguments.size(); + } + + std::shared_ptr FunctionCallExpression::getArgument(uint64_t i) const { + STORM_LOG_THROW(i < arguments.size(), storm::exceptions::InvalidArgumentException, "Tried to access the argument with index " << i << " of a function call with " << arguments.size() << " arguments."); + return arguments[i]; + } + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/expressions/FunctionCallExpression.h b/src/storm/storage/jani/expressions/FunctionCallExpression.h new file mode 100644 index 000000000..75949247a --- /dev/null +++ b/src/storm/storage/jani/expressions/FunctionCallExpression.h @@ -0,0 +1,42 @@ +#pragma once + +#include "storm/storage/expressions/BaseExpression.h" + +namespace storm { + namespace expressions { + /*! + * Represents an array with a given list of elements. + */ + class FunctionCallExpression : public BaseExpression { + public: + + FunctionCallExpression(ExpressionManager const& manager, Type const& type, std::string const& functionIdentifier, std::vector> const& arguments); + + + // Instantiate constructors and assignments with their default implementations. + FunctionCallExpression(FunctionCallExpression const& other) = default; + FunctionCallExpression& operator=(FunctionCallExpression const& other) = delete; + FunctionCallExpression(FunctionCallExpression&&) = default; + FunctionCallExpression& operator=(FunctionCallExpression&&) = delete; + + virtual ~FunctionCallExpression() = default; + + virtual void gatherVariables(std::set& variables) const override; + virtual bool containsVariables() const override; + virtual std::shared_ptr simplify() const override; + virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; + + std::string const& getFunctionIdentifier() const; + uint64_t getNumberOfArguments() const; + std::shared_ptr getArgument(uint64_t i) const; + + + protected: + virtual void printToStream(std::ostream& stream) const override; + + private: + std::string identifier; + std::vector> arguments; + }; + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp index cfd421c59..6b17ba50c 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp +++ b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp @@ -60,6 +60,15 @@ namespace storm { } } + template + boost::any JaniExpressionSubstitutionVisitor::visit(FunctionCallExpression const& expression, boost::any const& data) { + std::vector> newArguments; + newArguments.reserve(expression.getNumberOfArguments()); + for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) { + newArguments.push_back(boost::any_cast>(expression.getArgument(i)->accept(*this, data))); + } + return std::const_pointer_cast(std::shared_ptr(new FunctionCallExpression(expression.getManager(), expression.getType(), expression.getIdentifier(), newArguments))); + } // Explicitly instantiate the class with map and unordered_map. template class JaniExpressionSubstitutionVisitor>; diff --git a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h index ab196acee..07867be28 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h +++ b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h @@ -25,6 +25,7 @@ namespace storm { virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) override; virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) override; virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override; + virtual boost::any visit(FunctionCallExpression const& expression, boost::any const& data) override; }; } } \ No newline at end of file diff --git a/src/storm/storage/jani/expressions/JaniExpressionVisitor.h b/src/storm/storage/jani/expressions/JaniExpressionVisitor.h index 61808bb0d..99a45f2c5 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionVisitor.h +++ b/src/storm/storage/jani/expressions/JaniExpressionVisitor.h @@ -11,6 +11,7 @@ namespace storm { virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) = 0; virtual boost::any visit(ConstructorArrayExpression const& expression, boost::any const& data) = 0; virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) = 0; + virtual boost::any visit(FunctionCallExpression const& expression, boost::any const& data) = 0; }; } } diff --git a/src/storm/storage/jani/expressions/JaniExpressions.h b/src/storm/storage/jani/expressions/JaniExpressions.h index a48ec5119..209d6edd7 100644 --- a/src/storm/storage/jani/expressions/JaniExpressions.h +++ b/src/storm/storage/jani/expressions/JaniExpressions.h @@ -2,3 +2,4 @@ #include "storm/storage/jani/expressions/ArrayAccessExpression.h" #include "storm/storage/jani/expressions/ConstructorArrayExpression.h" #include "storm/storage/jani/expressions/ValueArrayExpression.h" +#include "storm/storage/jani/expressions/FunctionCallExpression.h" diff --git a/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp b/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp index f9c80a36a..8e5d11a92 100644 --- a/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp +++ b/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp @@ -71,6 +71,15 @@ namespace storm { virtual boost::any visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) override { return true; } + + virtual boost::any visit(storm::expressions::FunctionCallExpression const& expression, boost::any const& data) override { + for (uint64_t i = 0; i < expression.getNumberOfArguments(); ++i) { + if (boost::any_cast(expression.getArgument(i)->accept(*this, data))) { + return true; + } + } + return false; + } }; class ArrayExpressionFinderTraverser : public ConstJaniTraverser {