From dac431b263fe882dd4498f58215da42960b3672b Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 31 Aug 2018 17:28:36 +0200 Subject: [PATCH] parsing of jani-arrays --- src/storm-parsers/parser/JaniParser.cpp | 230 ++++++++++++------ src/storm-parsers/parser/JaniParser.h | 15 +- src/storm/storage/expressions/Expression.cpp | 3 - .../storage/expressions/SubstitutionVisitor.h | 2 +- src/storm/storage/jani/ArrayVariable.cpp | 6 +- src/storm/storage/jani/ArrayVariable.h | 4 +- src/storm/storage/jani/Assignment.cpp | 45 ++-- src/storm/storage/jani/Assignment.h | 41 +++- src/storm/storage/jani/LValue.cpp | 96 ++++++++ src/storm/storage/jani/LValue.h | 41 ++++ src/storm/storage/jani/OrderedAssignments.cpp | 4 +- src/storm/storage/jani/Variable.h | 4 +- .../expressions/ArrayAccessExpression.cpp | 17 +- .../jani/expressions/ArrayAccessExpression.h | 3 +- .../jani/expressions/ArrayExpression.h | 1 - .../ConstructorArrayExpression.cpp | 22 +- .../expressions/ConstructorArrayExpression.h | 5 +- .../JaniExpressionSubstitutionVisitor.cpp | 6 +- .../JaniExpressionSubstitutionVisitor.h | 8 +- .../jani/expressions/JaniExpressionVisitor.h | 3 - .../jani/expressions/ValueArrayExpression.cpp | 7 +- .../jani/expressions/ValueArrayExpression.h | 4 +- .../storage/jani/traverser/ArrayEliminator.h | 56 +++++ .../storage/jani/traverser/JaniTraverser.cpp | 8 +- .../storage/jani/traverser/JaniTraverser.h | 1 + src/storm/storage/prism/ToJaniConverter.cpp | 10 +- 26 files changed, 479 insertions(+), 163 deletions(-) create mode 100644 src/storm/storage/jani/LValue.cpp create mode 100644 src/storm/storage/jani/LValue.h create mode 100644 src/storm/storage/jani/traverser/ArrayEliminator.h diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index fc61bed31..97e7a80ad 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -644,7 +644,7 @@ namespace storm { } else if (typeStructure == "int") { result.basicType = ParsedType::BasicType::Int; } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")"); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << variableName << "' (scope: " << scopeDescription << ")"); } } 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"); @@ -671,10 +671,10 @@ namespace storm { } } 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"); - result.arrayBase = ParsedType(); - parseType(result.arrayBase.get(), typeStructure.at("base"), variableName, scopeDescription, globalVars, constants, localVars); + result.arrayBase = std::make_unique(); + parseType(*result.arrayBase, typeStructure.at("base"), variableName, scopeDescription, globalVars, constants, localVars); } 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 " << variableName << "(scope: " << scopeDescription << ") "); } } } @@ -763,29 +763,31 @@ 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::jani::ArrayVariable::ElementType elementType; - storm::expressions::Type* exprVariableType; + storm::expressions::Type exprVariableType; switch (type.arrayBase->basicType.get()) { case ParsedType::BasicType::Real: elementType = storm::jani::ArrayVariable::ElementType::Real; - exprVariableType = &expressionManager->getArrayType(expressionManager->getRationalType()); + exprVariableType = expressionManager->getArrayType(expressionManager->getRationalType()); break; case ParsedType::BasicType::Bool: elementType = storm::jani::ArrayVariable::ElementType::Bool; - exprVariableType = &expressionManager->getArrayType(expressionManager->getBooleanType()); + exprVariableType = expressionManager->getArrayType(expressionManager->getBooleanType()); break; case ParsedType::BasicType::Int: elementType = storm::jani::ArrayVariable::ElementType::Int; - exprVariableType = &expressionManager->getArrayType(expressionManager->getIntegerType()); + exprVariableType = expressionManager->getArrayType(expressionManager->getIntegerType()); break; + default: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported type"); } if (setInitValFromDefault) { - initVal = storm::expressions::ValueArrayExpression(expressionManager, *exprVariableType, {}); + initVal = storm::expressions::ValueArrayExpression(*expressionManager, exprVariableType, {}).toExpression(); } if (initVal) { - STORM_LOG_THROW(initVal.get().hasArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scopeDescription + ") should be an Array"); - return std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType->getElementType()), elementType, initVal.get(), transientVar); + STORM_LOG_THROW(initVal->getType().isArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scopeDescription + ") should be an Array"); + return std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType, initVal.get(), transientVar); } else { - return std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType->getElementType()), elementType); + return std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType); } } @@ -799,14 +801,14 @@ namespace storm { STORM_LOG_THROW(expected == actual, storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects " << expected << " arguments, but got " << actual << " in " << errorInfo << "."); } - std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars,returnNoneInitializedOnUnknownOperator); + std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars,returnNoneInitializedOnUnknownOperator, auxiliaryVariables); return {left}; } - std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); - storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator, 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); return {left, right}; } /** @@ -823,29 +825,79 @@ namespace storm { STORM_LOG_THROW(expr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << "."); } - storm::jani::Variable const& getLValue(std::string const& ident, storm::jani::VariableSet const& globalVars, storm::jani::VariableSet const& localVars, std::string const& scopeDescription) { - if(localVars.hasVariable(ident)) { - return localVars.getVariable(ident); - } else if(globalVars.hasVariable(ident)) { - return globalVars.getVariable(ident); + /** + * Helper for parse expression. + */ + void ensureIntegerType(storm::expressions::Expression const& expr, std::string const& opstring, unsigned argNr, std::string const& errorInfo) { + STORM_LOG_THROW(expr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects argument " + std::to_string(argNr) + " to be numerical in " << errorInfo << "."); + } + + /** + * Helper for parse expression. + */ + void ensureArrayType(storm::expressions::Expression const& expr, std::string const& opstring, unsigned argNr, std::string const& errorInfo) { + 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, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars) { + 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); + } + } 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); + return storm::jani::LValue(exp, index); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown LValue '" << lValueStructure.dump() << "' occurs in " << scopeDescription); + // Silly warning suppression. + return storm::jani::LValue(*localVars.end()->second); } } - storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars) { - if(localVars.count(ident) == 1) { - return localVars.at(ident)->getExpressionVariable(); - } else if(globalVars.count(ident) == 1) { - return globalVars.at(ident)->getExpressionVariable(); - } else if(constants.count(ident) == 1) { - return constants.at(ident)->getExpressionVariable(); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); + storm::expressions::Variable JaniParser::getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, 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()) { + return it->second->getExpressionVariable(); + } + } + { + auto it = globalVars.find(ident); + if (it != globalVars.end()) { + return it->second->getExpressionVariable(); + } + } + { + auto it = constants.find(ident); + if (it != constants.end()) { + return it->second->getExpressionVariable(); + } } + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown identifier '" << ident << "' occurs in " << scopeDescription); + // Silly warning suppression. + return storm::expressions::Variable(); } - storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator, std::unordered_map const& auxiliaryVariables) { if(expressionStructure.is_boolean()) { if(expressionStructure.get()) { return expressionManager->boolean(true); @@ -872,15 +924,15 @@ namespace storm { STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required"); STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required"); STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "Then operator required"); - arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator)); - arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator)); - arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator)); + 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); assert(arguments.size() == 3); ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ite(arguments[0], arguments[1], arguments[2]); } else if (opstring == "∨") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -889,7 +941,7 @@ namespace storm { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] || arguments[1]; } else if (opstring == "∧") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -898,7 +950,7 @@ namespace storm { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -907,7 +959,7 @@ namespace storm { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return (!arguments[0]) || arguments[1]; } else if (opstring == "¬") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); if(!arguments[0].isInitialized()) { return storm::expressions::Expression(); @@ -915,7 +967,7 @@ namespace storm { ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return !arguments[0]; } else if (opstring == "=") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(arguments[0].hasBooleanType()) { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); @@ -925,7 +977,7 @@ namespace storm { return arguments[0] == arguments[1]; } } else if (opstring == "≠") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(arguments[0].hasBooleanType()) { ensureBooleanType(arguments[1], opstring, 1, scopeDescription); @@ -935,7 +987,7 @@ namespace storm { return arguments[0] != arguments[1]; } } else if (opstring == "<") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -944,7 +996,7 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] < arguments[1]; } else if (opstring == "≤") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -953,7 +1005,7 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] <= arguments[1]; } else if (opstring == ">") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -962,7 +1014,7 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] > arguments[1]; } else if (opstring == "≥") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { return storm::expressions::Expression(); @@ -971,97 +1023,137 @@ namespace storm { ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] >= arguments[1]; } else if (opstring == "+") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] + arguments[1]; } else if (opstring == "-") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] - arguments[1]; } else if (opstring == "-") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription,globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription,globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return -arguments[0]; } else if (opstring == "*") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] * arguments[1]; } else if (opstring == "/") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] / arguments[1]; } else if (opstring == "%") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] % arguments[1]; } else if (opstring == "max") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return storm::expressions::maximum(arguments[0],arguments[1]); } else if (opstring == "min") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return storm::expressions::minimum(arguments[0],arguments[1]); } else if (opstring == "floor") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::floor(arguments[0]); } else if (opstring == "ceil") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ceil(arguments[0]); } else if (opstring == "abs") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::abs(arguments[0]); } else if (opstring == "sgn") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::sign(arguments[0]); } else if (opstring == "trc") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::truncate(arguments[0]); } else if (opstring == "pow") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0]^arguments[1]; } else if (opstring == "exp") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); // TODO implement STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "exp operation is not yet implemented"); } else if (opstring == "log") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator, auxiliaryVariables); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); // TODO implement STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "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); + 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 + ")."); + 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()); + if (first) { + commonType = elements.back()->getType(); + first = false; + } else if (!(commonType == elements.back()->getType())) { + 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); + } + } + } + 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 + ")."); + auto newAuxVars = auxiliaryVariables; + storm::expressions::Variable indexVar = expressionManager->declareIntegerVariable(indexVarName); + newAuxVars.emplace(indexVarName, indexVar); + 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, newAuxVars); + return std::make_shared(*expressionManager, expressionManager->getArrayType(exp.getType()), length.getBaseExpressionPointer(), indexVar, exp.getBaseExpressionPointer())->toExpression(); } else if (unsupportedOpstrings.count(opstring) > 0){ STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Opstring " + opstring + " is not supported by storm"); @@ -1080,8 +1172,6 @@ namespace storm { } - - void JaniParser::parseActions(json const& actionStructure, storm::jani::Model& parentModel) { std::set actionNames; for(auto const& actionEntry : actionStructure) { @@ -1125,10 +1215,10 @@ 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::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')"); - STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')"); - storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')", globalVars, constants, localVars); - transientAssignments.emplace_back(lhs, rhs); + storm::jani::LValue lValue = parseLValue(transientValueEntry.at("ref"), "LHS of assignment in location " + locName + " (automaton '" + name + "')", globalVars, constants, localVars); + 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); + transientAssignments.emplace_back(lValue, rhs); } } uint64_t id = automaton.addLocation(storm::jani::Location(locName, transientAssignments)); @@ -1210,7 +1300,7 @@ namespace storm { // 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"); std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); - storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); + storm::jani::LValue lValue = parseLValue(refstring, "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", globalVars, constants, localVars); // 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); @@ -1220,7 +1310,7 @@ namespace storm { if(assignmentEntry.count("index") > 0) { assignmentIndex = getUnsignedInt(assignmentEntry.at("index"), "assignment index in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); } - assignments.emplace_back(lhs, assignmentExpr, assignmentIndex); + assignments.emplace_back(lValue, assignmentExpr, assignmentIndex); } } destinationLocationsAndProbabilities.emplace_back(locIds.at(targetLoc), probExpr); diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index d14b20259..ed5d9fe32 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/LValue.h" #include "storm/logic/Formula.h" #include "storm/logic/Bound.h" #include "storm/logic/RewardAccumulation.h" @@ -51,14 +52,14 @@ namespace storm { storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, std::unordered_map> const& globalVars, std::unordered_map> const& constants); struct ParsedType { enum class BasicType {Bool, Int, Real}; - boost::optional basicType; boost::optional> bounds; - boost::optional arrayBase; + std::unique_ptr arrayBase; }; - void JaniParser::parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars); + void parseType(ParsedType& result, json const& typeStructure, std::string variableName, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars); + storm::jani::LValue parseLValue(json const& lValueStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}); std::shared_ptr parseVariable(json const& variableStructure, bool requireInitialValues, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); private: std::shared_ptr parseConstant(json const& constantStructure, std::unordered_map> const& constants, std::string const& scopeDescription = "global"); @@ -68,8 +69,8 @@ namespace storm { */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); std::shared_ptr parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::unordered_map> const& globalVars, std::unordered_map> 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, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars= {}, bool returnNoneOnUnknownOpString = false); - std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars= {}, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); + std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false, std::unordered_map const& auxiliaryVariables = {}); std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::string const& context); @@ -79,7 +80,7 @@ namespace storm { std::shared_ptr parseComposition(json const& compositionStructure); - storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}); + storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, std::unordered_map const& auxiliaryVariables = {}); diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index 1d31f4c6f..957acf978 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -451,8 +451,5 @@ namespace storm { return result; } - - - } } diff --git a/src/storm/storage/expressions/SubstitutionVisitor.h b/src/storm/storage/expressions/SubstitutionVisitor.h index c0885c0fe..99f0c2c18 100644 --- a/src/storm/storage/expressions/SubstitutionVisitor.h +++ b/src/storm/storage/expressions/SubstitutionVisitor.h @@ -39,7 +39,7 @@ namespace storm { virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override; virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override; - private: + protected: // A mapping of variables to expressions with which they shall be replaced. MapType const& variableToExpressionMapping; }; diff --git a/src/storm/storage/jani/ArrayVariable.cpp b/src/storm/storage/jani/ArrayVariable.cpp index 95e146d91..9ae41fff7 100644 --- a/src/storm/storage/jani/ArrayVariable.cpp +++ b/src/storm/storage/jani/ArrayVariable.cpp @@ -3,11 +3,11 @@ namespace storm { namespace jani { - ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { + ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType) : Variable(name, variable), elementType(elementType) { // Intentionally left empty. } - ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue) : Variable(name, variable, initValue, transient) { + ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType, storm::expressions::Expression const& initValue, bool transient) : Variable(name, variable, initValue, transient), elementType(elementType) { // Intentionally left empty. } @@ -35,7 +35,7 @@ namespace storm { return maxSize.get(); } - ElementType ArrayVariable::getElementType() const { + typename ArrayVariable::ElementType ArrayVariable::getElementType() const { return elementType; } diff --git a/src/storm/storage/jani/ArrayVariable.h b/src/storm/storage/jani/ArrayVariable.h index f8aca2397..4c68b1ca9 100644 --- a/src/storm/storage/jani/ArrayVariable.h +++ b/src/storm/storage/jani/ArrayVariable.h @@ -13,12 +13,12 @@ namespace storm { /*! * Creates an Array variable */ - ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType elementType); + ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType); /*! * Creates an Array variable with initial value */ - ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType elementType, storm::expressions::Expression const& initialValue, bool transient); + ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType const& elementType, storm::expressions::Expression const& initValue, bool transient); /*! * Sets/Gets bounds to the values stored in this array diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp index 747679385..6830abb6f 100644 --- a/src/storm/storage/jani/Assignment.cpp +++ b/src/storm/storage/jani/Assignment.cpp @@ -1,5 +1,7 @@ #include "storm/storage/jani/Assignment.h" +#include "storm/storage/jani/LValue.h" + #include "storm/storage/expressions/LinearityCheckVisitor.h" #include "storm/utility/macros.h" @@ -8,20 +10,32 @@ namespace storm { namespace jani { - Assignment::Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t level) : variable(variable), expression(expression), level(level) { - + Assignment::Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, uint64_t level) : lValue(lValue), expression(expression), level(level) { + // Intentionally left empty } bool Assignment::operator==(Assignment const& other) const { return this->isTransient() == other.isTransient() && this->getExpressionVariable() == other.getExpressionVariable() && this->getAssignedExpression().isSyntacticallyEqual(other.getAssignedExpression()) && this->getLevel() == other.getLevel(); } + bool Assignment::lValueIsVariable() const { + return lValue.isVariable(); + } + + bool Assignment::lValueIsArrayAccess() const { + return lValue.isArrayAccess(); + } + + storm::jani::LValue const& Assignment::getLValue() const { + return lValue; + } + storm::jani::Variable const& Assignment::getVariable() const { - return variable.get(); + return lValue.getVariable(); } storm::expressions::Variable const& Assignment::getExpressionVariable() const { - return variable.get().getExpressionVariable(); + return getVariable().getExpressionVariable(); } storm::expressions::Expression const& Assignment::getAssignedExpression() const { @@ -33,11 +47,14 @@ namespace storm { } bool Assignment::isTransient() const { - return this->variable.get().isTransient(); + return lValue.isTransient(); } void Assignment::substitute(std::map const& substitution) { this->setAssignedExpression(this->getAssignedExpression().substitute(substitution).simplify()); + if (lValue.isArrayAccess()) { + lValue = LValue(LValue(lValue.getArray()), lValue.getArrayIndex().substitute(substitution).simplify()); + } } int64_t Assignment::getLevel() const { @@ -54,24 +71,24 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { - stream << assignment.getVariable().getName() << " := " << assignment.getAssignedExpression(); + stream << assignment.getLValue() << " := " << assignment.getAssignedExpression(); return stream; } - bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, Assignment const& right) const { - return left.getLevel() < right.getLevel() || (left.getLevel() == right.getLevel() && left.getExpressionVariable() < right.getExpressionVariable()); + bool AssignmentPartialOrderByLevelAndLValue::operator()(Assignment const& left, Assignment const& right) const { + return left.getLevel() < right.getLevel() || (left.getLevel() == right.getLevel() && left.getLValue() < right.getLValue()); } - bool AssignmentPartialOrderByLevelAndVariable::operator()(Assignment const& left, std::shared_ptr const& right) const { - return left.getLevel() < right->getLevel() || (left.getLevel() == right->getLevel() && left.getExpressionVariable() < right->getExpressionVariable()); + bool AssignmentPartialOrderByLevelAndLValue::operator()(Assignment const& left, std::shared_ptr const& right) const { + return left.getLevel() < right->getLevel() || (left.getLevel() == right->getLevel() && left.getLValue() < right->getLValue()); } - bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr const& left, std::shared_ptr const& right) const { - return left->getLevel() < right->getLevel() || (left->getLevel() == right->getLevel() && left->getExpressionVariable() < right->getExpressionVariable()); + bool AssignmentPartialOrderByLevelAndLValue::operator()(std::shared_ptr const& left, std::shared_ptr const& right) const { + return left->getLevel() < right->getLevel() || (left->getLevel() == right->getLevel() && left->getLValue() < right->getLValue()); } - bool AssignmentPartialOrderByLevelAndVariable::operator()(std::shared_ptr const& left, Assignment const& right) const { - return left->getLevel() < right.getLevel() || (left->getLevel() == right.getLevel() && left->getExpressionVariable() < right.getExpressionVariable()); + bool AssignmentPartialOrderByLevelAndLValue::operator()(std::shared_ptr const& left, Assignment const& right) const { + return left->getLevel() < right.getLevel() || (left->getLevel() == right.getLevel() && left->getLValue() < right.getLValue()); } } } diff --git a/src/storm/storage/jani/Assignment.h b/src/storm/storage/jani/Assignment.h index 3ab3b5581..5179215e7 100644 --- a/src/storm/storage/jani/Assignment.h +++ b/src/storm/storage/jani/Assignment.h @@ -2,7 +2,7 @@ #include -#include "storm/storage/jani/Variable.h" +#include "storm/storage/jani/LValue.h" #include "storm/storage/expressions/Expression.h" namespace storm { @@ -11,20 +11,39 @@ namespace storm { class Assignment { public: /*! - * Creates an assignment of the given expression to the given variable. + * Creates an assignment of the given expression to the given LValue. */ - Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t index = 0); + Assignment(storm::jani::LValue const& lValue, storm::expressions::Expression const& expression, uint64_t index = 0); Assignment(Assignment const&) = default; bool operator==(Assignment const& other) const; + /*! - * Retrieves the expression variable that is written in this assignment. + * Returns true if the lValue is a variable + */ + bool lValueIsVariable() const; + + /*! + * Returns true if the lValue is an array access + */ + bool lValueIsArrayAccess() const; + + /*! + * Retrieves the lValue that is written in this assignment. + * @return + */ + storm::jani::LValue const& getLValue() const; + + /*! + * Retrieves the Variable that is written in this assignment. + * This assumes that the lValue is a variable. */ storm::jani::Variable const& getVariable() const; - + /*! * Retrieves the expression variable that is written in this assignment. + * This assumes that the lValue is a variable. */ storm::expressions::Variable const& getExpressionVariable() const; @@ -34,7 +53,7 @@ namespace storm { storm::expressions::Expression const& getAssignedExpression() const; /*! - * Sets a new expression that is assigned to the target variable. + * Sets a new expression that is assigned to the target LValue. */ void setAssignedExpression(storm::expressions::Expression const& expression); @@ -66,10 +85,10 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment); private: - // The variable being assigned. - std::reference_wrapper variable; + // The lValue being assigned. + LValue lValue; - // The expression that is being assigned to the variable. + // The expression that is being assigned to the lValue. storm::expressions::Expression expression; // The level of the assignment. @@ -77,10 +96,10 @@ namespace storm { }; /*! - * This functor enables ordering the assignments first by the assignment level and then by variable. + * This functor enables ordering the assignments first by the assignment level and then by lValue. * Note that this is a partial order. */ - struct AssignmentPartialOrderByLevelAndVariable { + struct AssignmentPartialOrderByLevelAndLValue { bool operator()(Assignment const& left, Assignment const& right) const; bool operator()(Assignment const& left, std::shared_ptr const& right) const; bool operator()(std::shared_ptr const& left, std::shared_ptr const& right) const; diff --git a/src/storm/storage/jani/LValue.cpp b/src/storm/storage/jani/LValue.cpp new file mode 100644 index 000000000..f8ba7eef4 --- /dev/null +++ b/src/storm/storage/jani/LValue.cpp @@ -0,0 +1,96 @@ +#include "storm/storage/jani/LValue.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace jani { + + LValue::LValue(storm::jani::Variable const& variable) : variable(&variable) { + // Intentionally left empty + } + + LValue::LValue(LValue const& array, storm::expressions::Expression const& index) : arrayIndex(index) { + STORM_LOG_THROW(array.isVariable(), storm::exceptions::NotSupportedException, "Nested arrays as LValues are currently not implemented."); + variable = &array.getVariable(); + } + + bool LValue::isVariable() const { + return !arrayIndex.isInitialized(); + } + + storm::jani::Variable const& LValue::getVariable() const { + STORM_LOG_ASSERT(isVariable(), "Tried to get the variable of an LValue, that actually is not a variable."); + return *variable; + } + + bool LValue::isArrayAccess() const { + return arrayIndex.isInitialized(); + } + + storm::jani::ArrayVariable const& LValue::getArray() const { + STORM_LOG_ASSERT(isArrayAccess(), "Tried to get the array variable of an LValue that is not an array access."); + STORM_LOG_ASSERT(variable->isArrayVariable(), "Tried to get the array variable of an array access LValue, but the variable is not of type array."); + return variable->asArrayVariable(); + } + + storm::expressions::Expression const& LValue::getArrayIndex() const { + STORM_LOG_ASSERT(isArrayAccess(), "Tried to get the array index of an LValue, that is not an array access."); + return arrayIndex; + } + + bool LValue::isTransient() const { + return variable->isTransient(); + } + + LValue LValue::changeAssignmentVariables(std::map> const& remapping) const { + if (isVariable()) { + return LValue(remapping.at(variable)); + } else { + STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue."); + return LValue(LValue(remapping.at(variable)), arrayIndex); + } + } + + + bool LValue::operator<(LValue const& other) const { + if (isVariable()) { + return !other.isVariable() || variable->getExpressionVariable() < other.getVariable().getExpressionVariable(); + } else { + STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue."); + if (other.isVariable()) { + return false; + } + STORM_LOG_ASSERT(other.isArrayAccess(), "Unhandled LValue."); + if (variable->getExpressionVariable() < other.getVariable().getExpressionVariable()) { + return true; + } else if (other.getVariable().getExpressionVariable() < variable->getExpressionVariable()) { + return false; + } else { + return std::less()(arrayIndex, other.getArrayIndex()); + } + } + } + + bool LValue::operator==(LValue const& other) const { + if (isVariable()) { + return other.isVariable() && getVariable().getExpressionVariable() == other.getVariable().getExpressionVariable(); + } else { + STORM_LOG_ASSERT(isArrayAccess(), "Unhandled LValue."); + return other.isArrayAccess() && getVariable().getExpressionVariable() == other.getVariable().getExpressionVariable() && getArrayIndex().isSyntacticallyEqual(other.getArrayIndex()); + } + } + + std::ostream& operator<<(std::ostream& stream, LValue const& lValue) { + if (lValue.isVariable()) { + stream << lValue.getVariable().getName(); + } else { + STORM_LOG_ASSERT(lValue.isArrayAccess(), "Unhandled LValue."); + stream << lValue.getArray().getName() << "[" << lValue.getArrayIndex() << "]"; + } + return stream; + } + + + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/LValue.h b/src/storm/storage/jani/LValue.h new file mode 100644 index 000000000..0e8126bcd --- /dev/null +++ b/src/storm/storage/jani/LValue.h @@ -0,0 +1,41 @@ +#pragma once + +#include "storm/storage/jani/ArrayVariable.h" +#include "storm/storage/expressions/Expressions.h" + +namespace storm { + namespace jani { + + class LValue { + public: + explicit LValue(storm::jani::Variable const& variable); + LValue(LValue const& array, storm::expressions::Expression const& index); + + LValue(LValue const&) = default; + bool operator==(LValue const& other) const; + + bool isVariable() const; + storm::jani::Variable const& getVariable() const; + + bool isArrayAccess() const; + storm::jani::ArrayVariable const& getArray() const; + storm::expressions::Expression const& getArrayIndex() const; + + bool isTransient() const; + bool operator< (LValue const& other) const; + + LValue changeAssignmentVariables(std::map> const& remapping) const; + + friend std::ostream& operator<<(std::ostream& stream, LValue const& lvalue); + + private: + + // The variable being assigned. + storm::jani::Variable const* variable; + + + // In case of an array access LValue, this is the accessed index of the array. + storm::expressions::Expression arrayIndex; + }; + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 9c622fe2b..bce6a0fc8 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -221,13 +221,13 @@ namespace storm { void OrderedAssignments::changeAssignmentVariables(std::map> const& remapping) { std::vector newAssignments; for (auto& assignment : allAssignments) { - newAssignments.emplace_back(remapping.at(&assignment->getVariable()), assignment->getAssignedExpression(), assignment->getLevel()); + newAssignments.emplace_back(assignment->getLValue().changeAssignmentVariables(remapping), assignment->getAssignedExpression(), assignment->getLevel()); } *this = OrderedAssignments(newAssignments); } std::vector>::const_iterator OrderedAssignments::lowerBound(Assignment const& assignment, std::vector> const& assignments) { - return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable()); + return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndLValue()); } uint64_t OrderedAssignments::isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start) const { diff --git a/src/storm/storage/jani/Variable.h b/src/storm/storage/jani/Variable.h index 8d5884a12..ab4bf80c1 100644 --- a/src/storm/storage/jani/Variable.h +++ b/src/storm/storage/jani/Variable.h @@ -86,8 +86,8 @@ namespace storm { UnboundedIntegerVariable const& asUnboundedIntegerVariable() const; RealVariable& asRealVariable(); RealVariable const& asRealVariable() const; - RealVariable& asArrayVariable(); - RealVariable const& asArrayVariable() const; + ArrayVariable& asArrayVariable(); + ArrayVariable const& asArrayVariable() const; /*! * Substitutes all variables in all expressions according to the given substitution. diff --git a/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp b/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp index d143fc10c..1f3980fc9 100644 --- a/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp +++ b/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp @@ -1,5 +1,8 @@ #include "storm/storage/jani/expressions/ArrayAccessExpression.h" +#include "storm/storage/jani/expressions/JaniExpressionVisitor.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/UnexpectedException.h" namespace storm { namespace expressions { @@ -11,7 +14,7 @@ namespace storm { } std::shared_ptr ArrayAccessExpression::simplify() const { - return std::shared_ptr(new ArrayAccessExpression(manager, type, getFirstOperand()->simplify(), getSecondOperand()->simplify())); + return std::shared_ptr(new ArrayAccessExpression(getManager(), getType(), getFirstOperand()->simplify(), getSecondOperand()->simplify())); } boost::any ArrayAccessExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { @@ -21,16 +24,12 @@ namespace storm { } void ArrayAccessExpression::printToStream(std::ostream& stream) const { - if (firstOperand->isVariable()) { - getFirstOperand()->printToStream(stream); + if (getFirstOperand()->isVariable()) { + stream << *getFirstOperand(); } else { - stream << "("; - getFirstOperand()->printToStream(stream); - stream << ")"; + stream << "(" << *getFirstOperand() << ")"; } - stream << "["; - getSecondOperand()->printToStream(stream); - stream << "]"; + stream << "[" << getSecondOperand() << "]"; } } } \ No newline at end of file diff --git a/src/storm/storage/jani/expressions/ArrayAccessExpression.h b/src/storm/storage/jani/expressions/ArrayAccessExpression.h index 0068b1b47..a545e123e 100644 --- a/src/storm/storage/jani/expressions/ArrayAccessExpression.h +++ b/src/storm/storage/jani/expressions/ArrayAccessExpression.h @@ -1,7 +1,6 @@ #pragma once -#include "storm/storage/expressions/BaseExpression.h" -#include "storm/storage/jani/expressions/ExpressionManager.h" +#include "storm/storage/expressions/BinaryExpression.h" namespace storm { namespace expressions { diff --git a/src/storm/storage/jani/expressions/ArrayExpression.h b/src/storm/storage/jani/expressions/ArrayExpression.h index 63b1bae8e..3dbcf480d 100644 --- a/src/storm/storage/jani/expressions/ArrayExpression.h +++ b/src/storm/storage/jani/expressions/ArrayExpression.h @@ -1,7 +1,6 @@ #pragma once #include "storm/storage/expressions/BaseExpression.h" -#include "storm/storage/jani/expressions/ExpressionManager.h" namespace storm { namespace expressions { diff --git a/src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp b/src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp index d643c527e..2eb778800 100644 --- a/src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp +++ b/src/storm/storage/jani/expressions/ConstructorArrayExpression.cpp @@ -1,6 +1,7 @@ #include "storm/storage/jani/expressions/ConstructorArrayExpression.h" #include "storm/storage/jani/expressions/JaniExpressionVisitor.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -8,14 +9,14 @@ namespace storm { namespace expressions { - ConstructorArrayExpression::ConstructorArrayExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& size, storm::expressions::Variable indexVar, std::shared_ptr const& elementExpression) : ArrayExpression(manager, type), size(size), indexVar(indexVar), elementExpression(elementExpression) { + ConstructorArrayExpression::ConstructorArrayExpression(ExpressionManager const& manager, Type const& type, std::shared_ptr const& size, storm::expressions::Variable indexVar, std::shared_ptr const& elementExpression) : ArrayExpression(manager, type), sizeExpression(size), indexVar(indexVar), elementExpression(elementExpression) { // Intentionally left empty } void ConstructorArrayExpression::gatherVariables(std::set& variables) const { // The indexVar should not be gathered (unless it is already contained). bool indexVarContained = variables.find(indexVar) != variables.end(); - size->gatherVariables(variables); + sizeExpression->gatherVariables(variables); elementExpression->gatherVariables(variables); if (!indexVarContained) { variables.erase(indexVar); @@ -23,7 +24,7 @@ namespace storm { } bool ConstructorArrayExpression::containsVariables() const { - if (size->containsVariables()) { + if (sizeExpression->containsVariables()) { return true; } // The index variable should not count @@ -34,7 +35,7 @@ namespace storm { } std::shared_ptr ConstructorArrayExpression::simplify() const { - return std::shared_ptr(new ConstructorArrayExpression(manager, type, size->simplify(), indexVar, elementExpression->simplify())); + return std::shared_ptr(new ConstructorArrayExpression(getManager(), getType(), sizeExpression->simplify(), indexVar, elementExpression->simplify())); } boost::any ConstructorArrayExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { @@ -44,20 +45,17 @@ namespace storm { } void ConstructorArrayExpression::printToStream(std::ostream& stream) const { - stream << "array[ "; - elementExpression->printToStream(stream); - stream << " | " << indexVar << "<"; - size->printToStream(stream); - stream << " ]"; + stream << "array[ " << *elementExpression << " | " << indexVar.getExpression() << " < " << *sizeExpression << " ]"; } std::shared_ptr ConstructorArrayExpression::size() const { - return size; + return sizeExpression; } std::shared_ptr ConstructorArrayExpression::at(uint64_t i) const { - STORM_LOG_THROW(i < elements.size(), storm::exceptions::InvalidArgumentException, "Tried to access the element with index " << i << " of an array of size " << elements.size() << "."); - return elements[i]; + std::map substitution; + substitution.emplace(indexVar, this->getManager().integer(i)); + return elementExpression->toExpression().substitute(substitution).getBaseExpressionPointer(); } std::shared_ptr const& ConstructorArrayExpression::getElementExpression() const { diff --git a/src/storm/storage/jani/expressions/ConstructorArrayExpression.h b/src/storm/storage/jani/expressions/ConstructorArrayExpression.h index 07d52b570..7c5d93c9e 100644 --- a/src/storm/storage/jani/expressions/ConstructorArrayExpression.h +++ b/src/storm/storage/jani/expressions/ConstructorArrayExpression.h @@ -1,6 +1,7 @@ #pragma once #include "storm/storage/jani/expressions/ArrayExpression.h" +#include "storm/storage/expressions/Variable.h" namespace storm { namespace expressions { @@ -22,7 +23,7 @@ namespace storm { virtual ~ConstructorArrayExpression() = default; virtual void gatherVariables(std::set& variables) const override; - virtual bool containsVariables() const; + virtual bool containsVariables() const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; @@ -38,7 +39,7 @@ namespace storm { virtual void printToStream(std::ostream& stream) const override; private: - std::shared_ptr size; + std::shared_ptr sizeExpression; storm::expressions::Variable indexVar; std::shared_ptr const& elementExpression; }; diff --git a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp index 0a449d3d5..101f53472 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp +++ b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp @@ -6,7 +6,7 @@ namespace storm { namespace expressions { template boost::any JaniExpressionSubstitutionVisitor::visit(ValueArrayExpression const& expression, boost::any const& data) { - uint64_t size = expression.getSize()->evaluateAsInt(); + uint64_t size = expression.size()->evaluateAsInt(); std::vector> newElements; newElements.reserve(size); for (uint64_t i = 0; i < size; ++i) { @@ -17,12 +17,12 @@ namespace storm { template boost::any JaniExpressionSubstitutionVisitor::visit(ConstructorArrayExpression const& expression, boost::any const& data) { - std::shared_ptr newSize = boost::any_cast>(expression.getSize()->accept(*this, data)); + std::shared_ptr newSize = boost::any_cast>(expression.size()->accept(*this, data)); std::shared_ptr elementExpression = boost::any_cast>(expression.getElementExpression()->accept(*this, data)); STORM_LOG_THROW(this->variableToExpressionMapping.find(expression.getIndexVar()) == this->variableToExpressionMapping.end(), storm::exceptions::InvalidArgumentException, "substitution of the index variable of a constructorArrayExpression is not possible."); // If the arguments did not change, we simply push the expression itself. - if (newSize.get() == expression.getSize().get() && elementExpression.get() == expression.getElementExpression().get()) { + if (newSize.get() == expression.size().get() && elementExpression.get() == expression.getElementExpression().get()) { return expression.getSharedPointer(); } else { return std::const_pointer_cast(std::shared_ptr(new ConstructorArrayExpression(expression.getManager(), expression.getType(), newSize, expression.getIndexVar(), elementExpression))); diff --git a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h index 131c2f8ac..ca82d7df1 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h +++ b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h @@ -2,12 +2,12 @@ #include "storm/storage/expressions/SubstitutionVisitor.h" #include "storm/storage/jani/expressions/JaniExpressions.h" - +#include "storm/storage/jani/expressions/JaniExpressionVisitor.h" namespace storm { namespace expressions { template - class JaniExpressionSubstitutionVisitor : public SubstitutionVisitor, public ExpressionManager { + class JaniExpressionSubstitutionVisitor : public SubstitutionVisitor, public JaniExpressionVisitor { public: /*! * Creates a new substitution visitor that uses the given map to replace variables. @@ -21,6 +21,4 @@ namespace storm { virtual boost::any visit(ArrayAccessExpression const& expression, boost::any const& data) override; }; } -} - -#endif /* STORM_STORAGE_EXPRESSIONS_SUBSTITUTIONVISITOR_H_ */ +} \ 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 d9c86e9af..e0e76e95e 100644 --- a/src/storm/storage/jani/expressions/JaniExpressionVisitor.h +++ b/src/storm/storage/jani/expressions/JaniExpressionVisitor.h @@ -6,7 +6,6 @@ namespace storm { namespace expressions { - template class JaniExpressionVisitor{ public: virtual boost::any visit(ValueArrayExpression const& expression, boost::any const& data) = 0; @@ -15,5 +14,3 @@ namespace storm { }; } } - -#endif /* STORM_STORAGE_EXPRESSIONS_SUBSTITUTIONVISITOR_H_ */ diff --git a/src/storm/storage/jani/expressions/ValueArrayExpression.cpp b/src/storm/storage/jani/expressions/ValueArrayExpression.cpp index feaf5a395..23c543c80 100644 --- a/src/storm/storage/jani/expressions/ValueArrayExpression.cpp +++ b/src/storm/storage/jani/expressions/ValueArrayExpression.cpp @@ -1,6 +1,7 @@ #include "storm/storage/jani/expressions/ValueArrayExpression.h" #include "storm/storage/jani/expressions/JaniExpressionVisitor.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/UnexpectedException.h" @@ -33,7 +34,7 @@ namespace storm { for (auto const& e : elements) { simplifiedElements.push_back(e->simplify()); } - return std::shared_ptr(new ValueArrayExpression(manager, type, simplifiedElements)); + return std::shared_ptr(new ValueArrayExpression(getManager(), getType(), simplifiedElements)); } boost::any ValueArrayExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const { @@ -46,7 +47,7 @@ namespace storm { stream << "array[ "; bool first = true; for (auto const& e : elements) { - e->printToStream(stream); + stream << *e; if (!first) { stream << " , "; } @@ -56,7 +57,7 @@ namespace storm { } std::shared_ptr ValueArrayExpression::size() const { - return this->manager.integer(elements.size()).getBaseExpressionPointer(); + return getManager().integer(elements.size()).getBaseExpressionPointer(); } std::shared_ptr ValueArrayExpression::at(uint64_t i) const { diff --git a/src/storm/storage/jani/expressions/ValueArrayExpression.h b/src/storm/storage/jani/expressions/ValueArrayExpression.h index 641330387..770b36db7 100644 --- a/src/storm/storage/jani/expressions/ValueArrayExpression.h +++ b/src/storm/storage/jani/expressions/ValueArrayExpression.h @@ -10,7 +10,7 @@ namespace storm { class ValueArrayExpression : public ArrayExpression { public: - ValueArrayExpression(ExpressionManager const& manager, Type const& type, std::vector> elements); + ValueArrayExpression(ExpressionManager const& manager, Type const& type, std::vector> const& elements); // Instantiate constructors and assignments with their default implementations. @@ -22,7 +22,7 @@ namespace storm { virtual ~ValueArrayExpression() = default; virtual void gatherVariables(std::set& variables) const override; - virtual bool containsVariables() const; + virtual bool containsVariables() const override; virtual std::shared_ptr simplify() const override; virtual boost::any accept(ExpressionVisitor& visitor, boost::any const& data) const override; diff --git a/src/storm/storage/jani/traverser/ArrayEliminator.h b/src/storm/storage/jani/traverser/ArrayEliminator.h new file mode 100644 index 000000000..fcff57b45 --- /dev/null +++ b/src/storm/storage/jani/traverser/ArrayEliminator.h @@ -0,0 +1,56 @@ +#pragma once + + +#include + +#include "storm/storage/jani/traverser/JaniTraverser.h" + +namespace storm { + namespace jani { + class ArrayEliminator { +/* + public: + void eliminate(Model& model); + + private: + + class ArrayVariableReplacer : public JaniTraverser { + public: + + ArrayVariableReplacer() = default; + virtual ~ArrayVariableReplacer() = default; + std::unordered_map> replace(); + + virtual void traverse(Assignment const& assignment, boost::any const& data) const override; + + private: + void std::unordered_map::getMaxSizes(Model& model); + + }; + + + + }; + + : public JaniTraverser { + + public: + + struct ResultType { + bool hasLocationAssignment, hasEdgeAssignment, hasEdgeDestinationAssignment; + }; + + AssignmentsFinder() = default; + + ResultType find(Model const& model, Variable const& variable); + + virtual ~AssignmentsFinder() = default; + + virtual void traverse(Location const& location, boost::any const& data) const override; + virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override; + virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override; + */ + }; + } +} + diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp index 2461792b5..eb60a9358 100644 --- a/src/storm/storage/jani/traverser/JaniTraverser.cpp +++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp @@ -129,10 +129,16 @@ namespace storm { traverse(assignment.getAssignedExpression(), data); } + void JaniTraverser::traverse(LValue const& lValue, boost::any const& data) const { + if (lValue.isArrayAccess()) { + traverse(lValue.getArrayIndex(), data); + } + } + void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const { // intentionally left empty. } - + } } diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h index 905ad0208..9cef29afc 100644 --- a/src/storm/storage/jani/traverser/JaniTraverser.h +++ b/src/storm/storage/jani/traverser/JaniTraverser.h @@ -29,6 +29,7 @@ namespace storm { virtual void traverse(EdgeDestination const& edgeDestination, boost::any const& data) const; virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const; virtual void traverse(Assignment const& assignment, boost::any const& data) const; + virtual void traverse(LValue const& lValue, boost::any const& data) const; virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const; }; } diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 25ecca79a..f8ec3e053 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -118,7 +118,7 @@ namespace storm { } auto newExpressionVariable = manager->declareBooleanVariable(finalLabelName); storm::jani::BooleanVariable const& newTransientVariable = janiModel.addVariable(storm::jani::BooleanVariable(newExpressionVariable.getName(), newExpressionVariable, manager->boolean(false), true)); - transientLocationAssignments.emplace_back(newTransientVariable, label.getStatePredicateExpression()); + transientLocationAssignments.emplace_back(storm::jani::LValue(newTransientVariable), label.getStatePredicateExpression()); // Variables that are accessed in the label predicate expression should be made global. std::set variables = label.getStatePredicateExpression().getVariables(); @@ -156,7 +156,7 @@ namespace storm { transientLocationExpression = rewardTerm; } } - transientLocationAssignments.emplace_back(newTransientVariable, transientLocationExpression); + transientLocationAssignments.emplace_back(storm::jani::LValue(newTransientVariable), transientLocationExpression); // Variables that are accessed in a reward term should be made global. std::set variables = transientLocationExpression.getVariables(); for (auto const& variable : variables) { @@ -178,9 +178,9 @@ namespace storm { for (auto const& entry : actionIndexToExpression) { auto it = transientEdgeAssignments.find(entry.first); if (it != transientEdgeAssignments.end()) { - it->second.push_back(storm::jani::Assignment(newTransientVariable, entry.second)); + it->second.push_back(storm::jani::Assignment(storm::jani::LValue(newTransientVariable), entry.second)); } else { - std::vector assignments = {storm::jani::Assignment(newTransientVariable, entry.second)}; + std::vector assignments = {storm::jani::Assignment(storm::jani::LValue(newTransientVariable), entry.second)}; transientEdgeAssignments.emplace(entry.first, assignments); } // Variables that are accessed in a reward term should be made global. @@ -275,7 +275,7 @@ namespace storm { for (auto const& update : command.getUpdates()) { std::vector assignments; for (auto const& assignment : update.getAssignments()) { - assignments.push_back(storm::jani::Assignment(variableToVariableMap.at(assignment.getVariable()).get(), assignment.getExpression())); + assignments.push_back(storm::jani::Assignment(storm::jani::LValue(variableToVariableMap.at(assignment.getVariable()).get()), assignment.getExpression())); } if (rateExpression) {