diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 0d415d388..6d2df8e36 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -10,6 +10,7 @@ #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/CompositionInformationVisitor.h" +#include "storm/storage/jani/expressions/JaniExpressions.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/InvalidJaniException.h" @@ -23,6 +24,7 @@ #include #include #include +#include #include "storm/utility/macros.h" #include "storm/utility/file.h" @@ -109,8 +111,9 @@ namespace storm { STORM_LOG_THROW(variablesCount < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables."); std::unordered_map> globalVars; if (variablesCount == 1) { + bool requireInitialValues = parsedStructure.count("restrict-initial") == 0; for (auto const& varStructure : parsedStructure.at("variables")) { - std::shared_ptr variable = parseVariable(varStructure, "global", globalVars, constants); + std::shared_ptr variable = parseVariable(varStructure, requireInitialValues, "global", globalVars, constants); globalVars.emplace(variable->getName(), variable); model.addVariable(*variable); } @@ -626,8 +629,52 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << constantStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); } - - std::shared_ptr JaniParser::parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars, bool prefWithScope) { + + 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) { + if (typeStructure.is_string()) { + if (typeStructure == "real") { + result.basicType = ParsedType::BasicType::Real; + } else if (typeStructure == "bool") { + result.basicType = ParsedType::BasicType::Bool; + } 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 << ")"); + } + } 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 + ") "); + 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); + 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); + 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 + ") "); + 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"); + 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 << ")"); + } + result.basicType = ParsedType::BasicType::Int; + result.bounds = std::make_pair(lowerboundExpr, upperboundExpr); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << variableName << "(scope: " << scopeDescription << ") "); + } + } 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); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") "); + } + } + } + + std::shared_ptr JaniParser::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) { 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"); @@ -640,101 +687,103 @@ namespace storm { if(tvarcount == 1) { transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name + "' (scope: " + scopeDescription + ") "); } + STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); + ParsedType type; + parseType(type, variableStructure.at("type"), name, scopeDescription, globalVars, constants, localVars); + 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 + ") "); } 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(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); boost::optional initVal; - if(variableStructure.at("type").is_string()) { - if(variableStructure.at("type") == "real") { - if(initvalcount == 1) { - if(variableStructure.at("initial-value").is_null()) { + 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); + } else { + assert(!transientVar); + } + + bool setInitValFromDefault = !initVal.is_initialized() && requireInitialValues; + if (type.basicType) { + switch (type.basicType.get()) { + case ParsedType::BasicType::Real: + if (setInitValFromDefault) { initVal = expressionManager->rational(defaultRationalInitialValue); - } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); - STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational"); } - return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); - - } - assert(!transientVar); - return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName)); - } else if(variableStructure.at("type") == "bool") { - if(initvalcount == 1) { - if(variableStructure.at("initial-value").is_null()) { - initVal = expressionManager->boolean(defaultBooleanInitialValue); + 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"); + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); - STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName)); } - if(transientVar) { - labels.insert(name); + case ParsedType::BasicType::Int: + if (setInitValFromDefault) { + if (type.bounds) { + initVal = storm::expressions::ite(type.bounds->first < 0 && type.bounds->second > 0, expressionManager->integer(defaultIntegerInitialValue), type.bounds->first); + // TODO as soon as we support half-open intervals, we have to change this. + } else { + initVal = expressionManager->integer(defaultIntegerInitialValue); + } } - return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); - } - assert(!transientVar); - return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName)); - } else if(variableStructure.at("type") == "int") { - if(initvalcount == 1) { - if(variableStructure.at("initial-value").is_null()) { - initVal = expressionManager->integer(defaultIntegerInitialValue); - } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); + if (initVal) { STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer"); - } - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar); - } - assert(!transientVar); // Checked earlier. - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName)); - } else if(variableStructure.at("type") == "clock") { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'clock' for variable '" << name << "' (scope: " << scopeDescription << ")"); - } else if(variableStructure.at("type") == "continuous") { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'continuous' for variable ''" << name << "' (scope: " << scopeDescription << ")"); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")"); - } - } else if(variableStructure.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 + ") "); - 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 + ")", globalVars, constants, localVars); - assert(lowerboundExpr.isInitialized()); - STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given"); - storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")", globalVars, constants, localVars); - assert(upperboundExpr.isInitialized()); - STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given"); - if(initvalcount == 1) { - if(variableStructure.at("initial-value").is_null()) { - initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr); - // TODO as soon as we support half-open intervals, we have to change this. + if (type.bounds) { + return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, type.bounds->first, type.bounds->second); + } else { + return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar); + } } else { - initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars); + if (type.bounds) { + return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), initVal.get(), transientVar); + } else { + return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), boost::none, false, type.bounds->first, type.bounds->second); + } } - } - std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name + "(scope: " + scopeDescription + ") "); - if(basictype == "int") { - if(initVal) { - STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer"); + break; + case ParsedType::BasicType::Bool: + if (setInitValFromDefault) { + initVal = expressionManager->boolean(defaultBooleanInitialValue); } - 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"); - 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 " << name << "(scope: " << scopeDescription << ")"); + if (initVal) { + STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); + if (transientVar) { + labels.insert(name); + } + return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); + } else { + return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName)); } - return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); - } + } + } 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; + switch (type.arrayBase->basicType.get()) { + case ParsedType::BasicType::Real: + elementType = storm::jani::ArrayVariable::ElementType::Real; + exprVariableType = &expressionManager->getArrayType(expressionManager->getRationalType()); + break; + case ParsedType::BasicType::Bool: + elementType = storm::jani::ArrayVariable::ElementType::Bool; + exprVariableType = &expressionManager->getArrayType(expressionManager->getBooleanType()); + break; + case ParsedType::BasicType::Int: + elementType = storm::jani::ArrayVariable::ElementType::Int; + exprVariableType = &expressionManager->getArrayType(expressionManager->getIntegerType()); + break; + } + if (setInitValFromDefault) { + initVal = storm::expressions::ValueArrayExpression(expressionManager, *exprVariableType, {}); + } + 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); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") "); + return std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType->getElementType()), elementType); } } - + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")"); } @@ -1050,8 +1099,9 @@ namespace storm { STORM_LOG_THROW(varDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of variables"); std::unordered_map> localVars; if(varDeclCount > 0) { + bool requireInitialValues = automatonStructure.count("restrict-initial") == 0; for(auto const& varStructure : automatonStructure.at("variables")) { - std::shared_ptr var = parseVariable(varStructure, name, globalVars, constants, localVars, true); + std::shared_ptr var = parseVariable(varStructure, requireInitialValues, name, globalVars, constants, localVars, true); assert(localVars.count(var->getName()) == 0); automaton.addVariable(*var); localVars.emplace(var->getName(), var); diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index 1ac4a514f..a6141c37c 100644 --- a/src/storm-parsers/parser/JaniParser.h +++ b/src/storm-parsers/parser/JaniParser.h @@ -48,7 +48,15 @@ namespace storm { std::pair> parseModel(bool parseProperties = true); storm::jani::Property parseProperty(json const& propertyStructure, std::unordered_map> const& globalVars, std::unordered_map> const& constants); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel, std::unordered_map> const& globalVars, std::unordered_map> const& constants); - std::shared_ptr parseVariable(json const& variableStructure, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}, bool prefWithScope = false); + struct ParsedType { + enum class BasicType {Bool, Int, Real}; + + boost::optional basicType; + boost::optional> bounds; + boost::optional 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); + 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); private: diff --git a/src/storm/storage/jani/ArrayVariable.cpp b/src/storm/storage/jani/ArrayVariable.cpp new file mode 100644 index 000000000..95e146d91 --- /dev/null +++ b/src/storm/storage/jani/ArrayVariable.cpp @@ -0,0 +1,57 @@ +#include "storm/storage/jani/ArrayVariable.h" + +namespace storm { + namespace jani { + + ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { + // Intentionally left empty. + } + + ArrayVariable::ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue) : Variable(name, variable, initValue, transient) { + // Intentionally left empty. + } + + void ArrayVariable::setElementTypeBounds(storm::expressions::Expression lowerBound, storm::expressions::Expression upperBound) { + elementTypeBounds = std::make_pair(lowerBound, upperBound); + } + + bool ArrayVariable::hasElementTypeBounds() const { + return elementTypeBounds.is_initialized(); + } + + std::pair const& ArrayVariable::getElementTypeBounds() const { + return elementTypeBounds.get(); + } + + void ArrayVariable::setMaxSize(uint64_t size) { + maxSize = size; + } + + bool ArrayVariable::hasMaxSize() const { + return maxSize.is_initialized(); + } + + uint64_t ArrayVariable::getMaxSize() const { + return maxSize.get(); + } + + ElementType ArrayVariable::getElementType() const { + return elementType; + } + + std::unique_ptr ArrayVariable::clone() const { + return std::make_unique(*this); + } + + bool ArrayVariable::isArrayVariable() const { + return true; + } + + void ArrayVariable::substitute(std::map const& substitution) { + Variable::substitute(substitution); + if (hasElementTypeBounds()) { + setElementTypeBounds(elementTypeBounds->first.substitute(substitution), elementTypeBounds->second.substitute(substitution)); + } + } + } +} diff --git a/src/storm/storage/jani/ArrayVariable.h b/src/storm/storage/jani/ArrayVariable.h new file mode 100644 index 000000000..f8aca2397 --- /dev/null +++ b/src/storm/storage/jani/ArrayVariable.h @@ -0,0 +1,52 @@ +#pragma once + +#include "storm/storage/jani/Variable.h" + +namespace storm { + namespace jani { + + class ArrayVariable : public Variable { + public: + + enum class ElementType {Bool, Int, Real}; + + /*! + * Creates an Array variable + */ + ArrayVariable(std::string const& name, storm::expressions::Variable const& variable, ElementType 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); + + /*! + * Sets/Gets bounds to the values stored in this array + */ + void setElementTypeBounds(storm::expressions::Expression lowerBound, storm::expressions::Expression upperBound); + bool hasElementTypeBounds() const; + std::pair const& getElementTypeBounds() const; + + /*! + * Sets/Gets the maximum size of the array + */ + void setMaxSize(uint64_t size); + bool hasMaxSize() const; + uint64_t getMaxSize() const; + + ElementType getElementType() const; + + virtual std::unique_ptr clone() const override; + virtual bool isArrayVariable() const override; + virtual void substitute(std::map const& substitution) override; + + + private: + ElementType elementType; + boost::optional> elementTypeBounds; + boost::optional maxSize; + }; + + + } +} diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 040f73eba..bd6e59c0c 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -924,10 +924,11 @@ namespace storm { } bool Model::hasArrayVariables() const { - return true; + return getExpressionManager().getNumberOfArrayVariables() != 0; } Model Model::convertArrays() const { + std::cout << "TODO"; return *this; } diff --git a/src/storm/storage/jani/Variable.cpp b/src/storm/storage/jani/Variable.cpp index 00f867ac2..d6a67996c 100644 --- a/src/storm/storage/jani/Variable.cpp +++ b/src/storm/storage/jani/Variable.cpp @@ -4,6 +4,7 @@ #include "storm/storage/jani/BoundedIntegerVariable.h" #include "storm/storage/jani/UnboundedIntegerVariable.h" #include "storm/storage/jani/RealVariable.h" +#include "storm/storage/jani/ArrayVariable.h" namespace storm { namespace jani { @@ -48,6 +49,10 @@ namespace storm { return false; } + bool Variable::isArrayVariable() const { + return false; + } + bool Variable::isTransient() const { return transient; } @@ -96,6 +101,14 @@ namespace storm { return static_cast(*this); } + ArrayVariable& Variable::asArrayVariable() { + return static_cast(*this); + } + + ArrayVariable const& Variable::asArrayVariable() const { + return static_cast(*this); + } + void Variable::substitute(std::map const& substitution) { if (this->hasInitExpression()) { this->setInitExpression(this->getInitExpression().substitute(substitution)); diff --git a/src/storm/storage/jani/Variable.h b/src/storm/storage/jani/Variable.h index 010b37449..8d5884a12 100644 --- a/src/storm/storage/jani/Variable.h +++ b/src/storm/storage/jani/Variable.h @@ -14,6 +14,7 @@ namespace storm { class BoundedIntegerVariable; class UnboundedIntegerVariable; class RealVariable; + class ArrayVariable; class Variable { public: @@ -72,6 +73,7 @@ namespace storm { virtual bool isBoundedIntegerVariable() const; virtual bool isUnboundedIntegerVariable() const; virtual bool isRealVariable() const; + virtual bool isArrayVariable() const; virtual bool isTransient() const; @@ -84,6 +86,8 @@ namespace storm { UnboundedIntegerVariable const& asUnboundedIntegerVariable() const; RealVariable& asRealVariable(); RealVariable const& asRealVariable() const; + RealVariable& asArrayVariable(); + RealVariable const& asArrayVariable() const; /*! * Substitutes all variables in all expressions according to the given substitution.