treating bounded JANI variables with single bound

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<storm::expressions::Variable> 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);

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<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));

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);

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<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             Variable::substitute(substitution);
+            if (this->hasLowerBound()) {
                 this->setLowerBound(this->getLowerBound().substitute(substitution));
+            }
+            if (this->hasUpperBound()) {
                 this->setUpperBound(this->getUpperBound().substitute(substitution));
             }
+        }
         
         std::shared_ptr<BoundedIntegerVariable> makeBoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, boost::optional<storm::expressions::Expression> initValue, bool transient, boost::optional<storm::expressions::Expression> lowerBound, boost::optional<storm::expressions::Expression> 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<BoundedIntegerVariable>(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get());
+                return std::make_shared<BoundedIntegerVariable>(name, variable, initValue.get(), transient, lowerBound ? lowerBound.get() : storm::expressions::Expression(), upperBound ? upperBound.get() : storm::expressions::Expression());
             } else {
                 assert(!transient);
-                return std::make_shared<BoundedIntegerVariable>(name, variable, lowerBound.get(), upperBound.get());
+                return std::make_shared<BoundedIntegerVariable>(name, variable, lowerBound ? lowerBound.get() : storm::expressions::Expression(), upperBound ? upperBound.get() : storm::expressions::Expression());
             }
         }
     }

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.
              */