diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 1d2fb60b3..888b534b4 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -619,6 +619,7 @@ namespace storm { // Traverse the path and construct necessary formula parts. auto actionIt = reversedLabels.rbegin(); + uint64_t step = 0; for (; pathIt != reversedPath.rend(); ++pathIt) { // Add new predicate frame. @@ -698,12 +699,36 @@ namespace storm { } } - // Enforce ranges of all assigned variables. -// for (auto const& variablePair : newVariableMaps) { -// for (auto const& ) -// } + // Enforce constraints of all assigned variables. + for (auto const& constraint : abstractionInformation.getConstraints()) { + std::set usedVariables = constraint.getVariables(); + + bool containsAssignedVariables = false; + for (auto usedIt = usedVariables.begin(), assignedIt = assignedVariables.begin();;) { + if (usedIt == usedVariables.end() || assignedIt == assignedVariables.end()) { + break; + } + + if (*usedIt == *assignedIt) { + containsAssignedVariables = true; + break; + } + + if (*usedIt < *assignedIt) { + ++usedIt; + } else { + ++assignedIt; + } + } + + if (containsAssignedVariables) { + auto transformedConstraint = constraint.changeManager(expressionManager).substitute(currentSubstitution); + predicates.back().emplace_back(transformedConstraint); + } + } ++actionIt; + ++step; } return std::make_pair(predicates, stepVariableToCopiedVariableMap); diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 7f7ce0708..948535f79 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -89,6 +89,7 @@ namespace storm { } for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { if (!variable.isTransient()) { + STORM_LOG_THROW(variable.hasLowerBound() && variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variables with infinite range are not supported."); int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index b92b67efb..441089965 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -684,12 +684,15 @@ namespace storm { 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("lower-bound") + variableStructure.at("type").count("upper-bound") > 0, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound or upper-bound must be given"); + storm::expressions::Expression lowerboundExpr; + if (variableStructure.at("type").count("lower-bound") > 0) { + lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")", globalVars, constants, localVars); + } + storm::expressions::Expression upperboundExpr; + if (variableStructure.at("type").count("upper-bound") > 0) { + upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")", globalVars, constants, localVars); + } 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()) { @@ -704,9 +707,9 @@ namespace storm { if(initVal) { STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer"); } - STORM_LOG_THROW(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.isInitialized() || lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); + STORM_LOG_THROW(!upperboundExpr.isInitialized() || upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); + if (lowerboundExpr.isInitialized() && upperboundExpr.isInitialized() && !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 << ")"); } return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr); diff --git a/src/storm/storage/jani/BoundedIntegerVariable.cpp b/src/storm/storage/jani/BoundedIntegerVariable.cpp index 5b851b127..ad15749e8 100644 --- a/src/storm/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storm/storage/jani/BoundedIntegerVariable.cpp @@ -29,6 +29,10 @@ namespace storm { this->lowerBound = expression; } + bool BoundedIntegerVariable::hasLowerBound() const { + return this->lowerBound.isInitialized(); + } + storm::expressions::Expression const& BoundedIntegerVariable::getUpperBound() const { return upperBound; } @@ -37,8 +41,23 @@ namespace storm { this->upperBound = expression; } + bool BoundedIntegerVariable::hasUpperBound() const { + return this->upperBound.isInitialized(); + } + storm::expressions::Expression BoundedIntegerVariable::getRangeExpression() const { - return this->getLowerBound() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBound(); + storm::expressions::Expression range; + if (this->hasLowerBound()) { + range = this->getLowerBound() <= this->getExpressionVariable(); + } + if (this->hasUpperBound()) { + if (range.isInitialized()) { + range = range && this->getExpressionVariable() <= this->getUpperBound(); + } else { + range = this->getExpressionVariable() <= this->getUpperBound(); + } + } + return range; } bool BoundedIntegerVariable::isBoundedIntegerVariable() const { @@ -47,17 +66,20 @@ namespace storm { void BoundedIntegerVariable::substitute(std::map const& substitution) { Variable::substitute(substitution); - this->setLowerBound(this->getLowerBound().substitute(substitution)); - this->setUpperBound(this->getUpperBound().substitute(substitution)); + if (this->hasLowerBound()) { + this->setLowerBound(this->getLowerBound().substitute(substitution)); + } + if (this->hasUpperBound()) { + this->setUpperBound(this->getUpperBound().substitute(substitution)); + } } std::shared_ptr makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional initValue, bool transient, boost::optional lowerBound, boost::optional upperBound) { - STORM_LOG_THROW(lowerBound && upperBound, storm::exceptions::NotImplementedException, "Jani Bounded Integer variables (for now) have to be bounded from both sides"); if (initValue) { - return std::make_shared(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get()); + return std::make_shared(name, variable, initValue.get(), transient, lowerBound ? lowerBound.get() : storm::expressions::Expression(), upperBound ? upperBound.get() : storm::expressions::Expression()); } else { assert(!transient); - return std::make_shared(name, variable, lowerBound.get(), upperBound.get()); + return std::make_shared(name, variable, lowerBound ? lowerBound.get() : storm::expressions::Expression(), upperBound ? upperBound.get() : storm::expressions::Expression()); } } } diff --git a/src/storm/storage/jani/BoundedIntegerVariable.h b/src/storm/storage/jani/BoundedIntegerVariable.h index 1f201ba2e..221d9dceb 100644 --- a/src/storm/storage/jani/BoundedIntegerVariable.h +++ b/src/storm/storage/jani/BoundedIntegerVariable.h @@ -33,6 +33,11 @@ namespace storm { */ void setLowerBound(storm::expressions::Expression const& expression); + /*! + * Retrieves whether the variable has a lower bound. + */ + bool hasLowerBound() const; + /*! * Retrieves the expression defining the upper bound of the variable. */ @@ -43,6 +48,11 @@ namespace storm { */ void setUpperBound(storm::expressions::Expression const& expression); + /*! + * Retrieves whether the variable has an upper bound. + */ + bool hasUpperBound() const; + /*! * Retrieves an expression characterizing the legal range of the bounded integer variable. */