diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 6f245e99e..f3105d6ca 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -847,8 +847,17 @@ namespace storm { 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. + storm::expressions::Expression takeDefaultCondition; + if (type.bounds->first.isInitialized()) { + takeDefaultCondition = type.bounds->first < defaultIntegerInitialValue; + if (type.bounds->second.isInitialized()) { + takeDefaultCondition = takeDefaultCondition && type.bounds->second >= defaultIntegerInitialValue; + } + } else { + STORM_LOG_ASSERT(type.bounds->second.isInitialized(), "Expected to have either a lower or an upper bound"); + takeDefaultCondition = type.bounds->second >= defaultIntegerInitialValue; + } + initVal = storm::expressions::ite(takeDefaultCondition, expressionManager->integer(defaultIntegerInitialValue), type.bounds->first); } else { initVal = expressionManager->integer(defaultIntegerInitialValue); } @@ -910,7 +919,13 @@ namespace storm { result = std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType); } if (type.arrayBase->bounds) { - result->setElementTypeBounds(type.arrayBase->bounds->first, type.arrayBase->bounds->second); + auto const& bounds = type.arrayBase->bounds.get(); + if (bounds.first.isInitialized()) { + result->setLowerElementTypeBound(bounds.first); + } + if (bounds.second.isInitialized()) { + result->setUpperElementTypeBound(bounds.second); + } } return result; } diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp index cd78f95ca..e39a5d7e3 100644 --- a/src/storm/storage/jani/ArrayEliminator.cpp +++ b/src/storm/storage/jani/ArrayEliminator.cpp @@ -569,11 +569,11 @@ namespace storm { } if (arrayVariable.getElementType() == ArrayVariable::ElementType::Int) { storm::expressions::Variable exprVariable = expressionManager.declareIntegerVariable(name); - if (arrayVariable.hasElementTypeBounds()) { + if (arrayVariable.hasElementTypeBound()) { if (initValue.isInitialized()) { - return std::make_shared(name, exprVariable, initValue, arrayVariable.isTransient(), arrayVariable.getElementTypeBounds().first, arrayVariable.getElementTypeBounds().second); + return std::make_shared(name, exprVariable, initValue, arrayVariable.isTransient(), arrayVariable.getLowerElementTypeBound(), arrayVariable.getUpperElementTypeBound()); } else { - return std::make_shared(name, exprVariable, arrayVariable.getElementTypeBounds().first, arrayVariable.getElementTypeBounds().second); + return std::make_shared(name, exprVariable, arrayVariable.getLowerElementTypeBound(), arrayVariable.getUpperElementTypeBound()); } } else { if (initValue.isInitialized()) { diff --git a/src/storm/storage/jani/ArrayVariable.cpp b/src/storm/storage/jani/ArrayVariable.cpp index 9ae41fff7..997ab8d67 100644 --- a/src/storm/storage/jani/ArrayVariable.cpp +++ b/src/storm/storage/jani/ArrayVariable.cpp @@ -1,5 +1,7 @@ #include "storm/storage/jani/ArrayVariable.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" + namespace storm { namespace jani { @@ -11,28 +13,32 @@ namespace storm { // Intentionally left empty. } - void ArrayVariable::setElementTypeBounds(storm::expressions::Expression lowerBound, storm::expressions::Expression upperBound) { - elementTypeBounds = std::make_pair(lowerBound, upperBound); + void ArrayVariable::setLowerElementTypeBound(storm::expressions::Expression const& lowerBound) { + lowerElementTypeBound = lowerBound; } - bool ArrayVariable::hasElementTypeBounds() const { - return elementTypeBounds.is_initialized(); + void ArrayVariable::setUpperElementTypeBound(storm::expressions::Expression const& upperBound) { + upperElementTypeBound = upperBound; + } + + bool ArrayVariable::hasElementTypeBound() const { + return hasLowerElementTypeBound() || hasUpperElementTypeBound(); } - std::pair const& ArrayVariable::getElementTypeBounds() const { - return elementTypeBounds.get(); + bool ArrayVariable::hasLowerElementTypeBound() const { + return lowerElementTypeBound.isInitialized(); } - void ArrayVariable::setMaxSize(uint64_t size) { - maxSize = size; + bool ArrayVariable::hasUpperElementTypeBound() const { + return upperElementTypeBound.isInitialized(); } - bool ArrayVariable::hasMaxSize() const { - return maxSize.is_initialized(); + storm::expressions::Expression const& ArrayVariable::getLowerElementTypeBound() const { + return lowerElementTypeBound; } - uint64_t ArrayVariable::getMaxSize() const { - return maxSize.get(); + storm::expressions::Expression const& ArrayVariable::getUpperElementTypeBound() const { + return upperElementTypeBound; } typename ArrayVariable::ElementType ArrayVariable::getElementType() const { @@ -49,8 +55,11 @@ namespace storm { void ArrayVariable::substitute(std::map const& substitution) { Variable::substitute(substitution); - if (hasElementTypeBounds()) { - setElementTypeBounds(elementTypeBounds->first.substitute(substitution), elementTypeBounds->second.substitute(substitution)); + if (hasLowerElementTypeBound()) { + setLowerElementTypeBound(substituteJaniExpression(getLowerElementTypeBound(), substitution)); + } + if (hasUpperElementTypeBound()) { + setUpperElementTypeBound(substituteJaniExpression(getUpperElementTypeBound(), substitution)); } } } diff --git a/src/storm/storage/jani/ArrayVariable.h b/src/storm/storage/jani/ArrayVariable.h index 4c68b1ca9..9420cd77a 100644 --- a/src/storm/storage/jani/ArrayVariable.h +++ b/src/storm/storage/jani/ArrayVariable.h @@ -21,18 +21,42 @@ namespace storm { 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 + * Sets the lower bound 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; + void setLowerElementTypeBound(storm::expressions::Expression const& lowerBound); + + /*! + * Sets the upper bound to the values stored in this array + */ + void setUpperElementTypeBound(storm::expressions::Expression const& upperBound); + + /*! + * Returns true if there is either an upper bound or a lower bound + */ + bool hasElementTypeBound() const; /*! - * Sets/Gets the maximum size of the array + * Returns true if there is an upper element type bound */ - void setMaxSize(uint64_t size); - bool hasMaxSize() const; - uint64_t getMaxSize() const; + bool hasUpperElementTypeBound() const; + + /*! + * Returns true if there is a lower element type bound + */ + bool hasLowerElementTypeBound() const; + + /*! + * Returns the upper element type bound. The returned expression might not be initialized if there is no such bound. + */ + storm::expressions::Expression const& getUpperElementTypeBound() const; + + /*! + * Returns the lower element type bound. The returned expression might not be initialized if there is no such bound. + */ + storm::expressions::Expression const& getLowerElementTypeBound() const; + + std::pair const& getElementTypeBounds() const; + ElementType getElementType() const; @@ -43,8 +67,7 @@ namespace storm { private: ElementType elementType; - boost::optional> elementTypeBounds; - boost::optional maxSize; + storm::expressions::Expression lowerElementTypeBound, upperElementTypeBound; }; diff --git a/src/storm/storage/jani/FunctionEliminator.cpp b/src/storm/storage/jani/FunctionEliminator.cpp index 4d783c5be..152dfc77f 100644 --- a/src/storm/storage/jani/FunctionEliminator.cpp +++ b/src/storm/storage/jani/FunctionEliminator.cpp @@ -344,8 +344,11 @@ namespace storm { if (variable.hasInitExpression()) { variable.setInitExpression(functionEliminationVisitor->eliminate(variable.getInitExpression())); } - if (variable.hasElementTypeBounds()) { - variable.setElementTypeBounds(functionEliminationVisitor->eliminate(variable.getElementTypeBounds().first), functionEliminationVisitor->eliminate(variable.getElementTypeBounds().second)); + if (variable.hasLowerElementTypeBound()) { + variable.setLowerElementTypeBound(functionEliminationVisitor->eliminate(variable.getLowerElementTypeBound())); + } + if (variable.hasUpperElementTypeBound()) { + variable.setUpperElementTypeBound(functionEliminationVisitor->eliminate(variable.getUpperElementTypeBound())); } } diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 73e019c85..bf83d36f0 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -847,12 +847,16 @@ namespace storm { typeDesc["base"] = "real"; break; case storm::jani::ArrayVariable::ElementType::Int: - if (variable.asArrayVariable().hasElementTypeBounds()) { + if (variable.asArrayVariable().hasElementTypeBound()) { modernjson::json baseTypeDescr; baseTypeDescr["kind"] = "bounded"; baseTypeDescr["base "] = "int"; - baseTypeDescr["lower-bound"] = buildExpression(variable.asArrayVariable().getElementTypeBounds().first, constants, globalVariables, localVariables); - baseTypeDescr["upper-bound"] = buildExpression(variable.asArrayVariable().getElementTypeBounds().second, constants, globalVariables, localVariables); + if (variable.asArrayVariable().hasLowerElementTypeBound()) { + baseTypeDescr["lower-bound"] = buildExpression(variable.asArrayVariable().getLowerElementTypeBound(), constants, globalVariables, localVariables); + } + if (variable.asArrayVariable().hasUpperElementTypeBound()) { + baseTypeDescr["upper-bound"] = buildExpression(variable.asArrayVariable().getUpperElementTypeBound(), constants, globalVariables, localVariables); + } typeDesc["base"] = baseTypeDescr; } else { typeDesc["base"] = "int"; diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index ee8a798e2..f6a47e34c 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -311,12 +311,13 @@ namespace storm { return true; } } - if (arrayVariable.hasElementTypeBounds()) { - auto const& bounds = arrayVariable.getElementTypeBounds(); - if (bounds.first.containsVariable(variables)) { + if (arrayVariable.hasLowerElementTypeBound()) { + if (arrayVariable.getLowerElementTypeBound().containsVariable(variables)) { return true; } - if (bounds.second.containsVariable(variables)) { + } + if (arrayVariable.hasUpperElementTypeBound()) { + if (arrayVariable.getUpperElementTypeBound().containsVariable(variables)) { return true; } } diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp index ae912a3a8..72f979b2d 100644 --- a/src/storm/storage/jani/traverser/JaniTraverser.cpp +++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp @@ -103,9 +103,11 @@ namespace storm { if (variable.hasInitExpression()) { traverse(variable.getInitExpression(), data); } - if (variable.hasElementTypeBounds()) { - traverse(variable.getElementTypeBounds().first, data); - traverse(variable.getElementTypeBounds().second, data); + if (variable.hasLowerElementTypeBound()) { + traverse(variable.getLowerElementTypeBound(), data); + } + if (variable.hasUpperElementTypeBound()) { + traverse(variable.getUpperElementTypeBound(), data); } } @@ -264,9 +266,11 @@ namespace storm { if (variable.hasInitExpression()) { traverse(variable.getInitExpression(), data); } - if (variable.hasElementTypeBounds()) { - traverse(variable.getElementTypeBounds().first, data); - traverse(variable.getElementTypeBounds().second, data); + if (variable.hasLowerElementTypeBound()) { + traverse(variable.getLowerElementTypeBound(), data); + } + if (variable.hasUpperElementTypeBound()) { + traverse(variable.getUpperElementTypeBound(), data); } }