added support for unbounded integer variables in explicit jani builder such that it is treated as a bounded variable (with a given number of bits) and an exception is thrown in case of an underflow or overflow

src/storm/builder/BuilderOptions.cpp

@@ -37,7 +37,7 @@ namespace storm {
             return boost::get<storm::expressions::Expression>(labelOrExpression);
         }
         
-        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), scaleAndLiftTransitionRewards(true), explorationChecks(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) {
+        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), scaleAndLiftTransitionRewards(true), explorationChecks(false), addOverlappingGuardsLabel(false), addOutOfBoundsState(false), reservedBitsForUnboundedVariables(32), showProgress(false), showProgressDelay(0) {
             // Intentionally left empty.
         }
         
@@ -59,6 +59,7 @@ namespace storm {
             auto const& buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             explorationChecks = buildSettings.isExplorationChecksSet();
+            reservedBitsForUnboundedVariables = buildSettings.getBitsForUnboundedVariables();
             showProgress = generalSettings.isVerboseSet();
             showProgressDelay = generalSettings.getShowProgressDelay();
         }
@@ -172,6 +173,10 @@ namespace storm {
         bool BuilderOptions::isAddOutOfBoundsStateSet() const {
             return addOutOfBoundsState;
         }
+        
+        uint64_t BuilderOptions::getReservedBitsForUnboundedVariables() const {
+            return reservedBitsForUnboundedVariables;
+        }
 
         bool BuilderOptions::isAddOverlappingGuardLabelSet() const {
             return addOverlappingGuardsLabel;
@@ -257,6 +262,11 @@ namespace storm {
             addOutOfBoundsState = newValue;
             return *this;
         }
+        
+        BuilderOptions& BuilderOptions::setReservedBitsForUnboundedVariables(uint64_t newValue) {
+            reservedBitsForUnboundedVariables = newValue;
+            return *this;
+        }
 
         BuilderOptions& BuilderOptions::setAddOverlappingGuardsLabel(bool newValue) {
             addOverlappingGuardsLabel = newValue;

src/storm/builder/BuilderOptions.h

@@ -109,6 +109,7 @@ namespace storm {
             bool isShowProgressSet() const;
             bool isScaleAndLiftTransitionRewardsSet() const;
             bool isAddOutOfBoundsStateSet() const;
+            uint64_t getReservedBitsForUnboundedVariables() const;
             bool isAddOverlappingGuardLabelSet() const;
             uint64_t getShowProgressDelay() const;
 
@@ -179,6 +180,11 @@ namespace storm {
              */
             BuilderOptions& setAddOverlappingGuardsLabel(bool newValue = true);
 
+            /**
+             * Sets the number of bits that will be reserved for unbounded integer variables.
+             */
+            BuilderOptions& setReservedBitsForUnboundedVariables(uint64_t value);
+            
             /**
              * Substitutes all expressions occurring in these options.
              */
@@ -226,6 +232,9 @@ namespace storm {
             /// A flag indicating that the an additional state for out of bounds should be created.
             bool addOutOfBoundsState;
 
+            /// Indicates the number of bits that are reserved for the storage of unbounded integer variables.
+            uint64_t reservedBitsForUnboundedVariables;
+            
             /// A flag that stores whether the progress of exploration is to be printed.
             bool showProgress;
 

src/storm/generator/JaniNextStateGenerator.cpp

@@ -73,7 +73,7 @@ namespace storm {
 
             // Now we are ready to initialize the variable information.
             this->checkValid();
-            this->variableInformation = VariableInformation(this->model, this->parallelAutomata, options.isAddOutOfBoundsStateSet());
+            this->variableInformation = VariableInformation(this->model, this->parallelAutomata, options.getReservedBitsForUnboundedVariables(), options.isAddOutOfBoundsStateSet());
             this->variableInformation.registerArrayVariableReplacements(arrayEliminatorData);
             
             // Create a proper evalator.
@@ -344,7 +344,7 @@ namespace storm {
                     if (assignedValue < integerIt->lowerBound || assignedValue > integerIt->upperBound) {
                         return this->outOfBoundsState;
                     }
-                } else if (this->options.isExplorationChecksSet()) {
+                } else if (integerIt->forceOutOfBoundsCheck || this->options.isExplorationChecksSet()) {
                     STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
                     STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
                 }

src/storm/generator/PrismNextStateGenerator.cpp

@@ -386,7 +386,7 @@ namespace storm {
                     if (assignedValue < integerIt->lowerBound || assignedValue > integerIt->upperBound) {
                         return this->outOfBoundsState;
                     }
-                } else if (this->options.isExplorationChecksSet()) {
+                } else if (integerIt->forceOutOfBoundsCheck || this->options.isExplorationChecksSet()) {
                     STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
                     STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
                 }

src/storm/generator/VariableInformation.cpp

@@ -22,7 +22,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth), global(global) {
+        IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global, bool forceOutOfBoundsCheck) : variable(variable), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth), global(global), forceOutOfBoundsCheck(forceOutOfBoundsCheck) {
             // Intentionally left empty.
         }
         
@@ -68,7 +68,7 @@ namespace storm {
             sortVariables();
         }
         
-        VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, bool outOfBoundsState) : totalBitOffset(0) {
+        VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState) : totalBitOffset(0) {
             // Check that the model does not contain non-transient unbounded integer or non-transient real variables.
             STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains global non-transient real variables.");
             STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables.");
@@ -82,7 +82,7 @@ namespace storm {
             } else {
                 outOfBoundsBit = boost::none;
             }
-
+            
             for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
                 if (!variable.isTransient()) {
                     booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true);
@@ -91,14 +91,33 @@ 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();
+                    int64_t lowerBound;
+                    int64_t upperBound;
+                    if (variable.hasLowerBound()) {
+                        lowerBound = variable.getLowerBound().evaluateAsInt();
+                        if (variable.hasUpperBound()) {
+                            upperBound = variable.getUpperBound().evaluateAsInt();
+                        } else {
+                            upperBound = lowerBound + ((1u << reservedBitsForUnboundedVariables) - 1);
+                        }
+                    } else {
+                        STORM_LOG_THROW(variable.hasUpperBound(), storm::exceptions::WrongFormatException, "Bounded integer variable has neither a lower nor an upper bound.");
+                        upperBound = variable.getUpperBound().evaluateAsInt();
+                        lowerBound = upperBound - ((1u << reservedBitsForUnboundedVariables) - 1);
+                    }
                     uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
-                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
+                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true, !variable.hasLowerBound() || !variable.hasUpperBound());
                     totalBitOffset += bitwidth;
                 }
             }
+            for (auto const& variable : model.getGlobalVariables().getUnboundedIntegerVariables()) {
+                if (!variable.isTransient()) {
+                    int64_t lowerBound = - (1u << (reservedBitsForUnboundedVariables - 1));
+                    int64_t upperBound = (1u << (reservedBitsForUnboundedVariables - 1)) - 1;
+                    integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, reservedBitsForUnboundedVariables, true, true);
+                    totalBitOffset += reservedBitsForUnboundedVariables;
+                }
+            }
             
             for (auto const& automatonRef : parallelAutomata) {
                 createVariablesForAutomaton(automatonRef.get());

src/storm/generator/VariableInformation.h

@@ -37,7 +37,7 @@ namespace storm {
         
         // A structure storing information about the integer variables of the model.
         struct IntegerVariableInformation {
-            IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global = false);
+            IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth, bool global = false, bool forceOutOfBoundsCheck = false);
             
             // The integer variable.
             storm::expressions::Variable variable;
@@ -56,6 +56,9 @@ namespace storm {
             
             // A flag indicating whether the variable is a global one.
             bool global;
+            
+            // A flag indicating whether an out of bounds check is enforced for this variable.
+            bool forceOutOfBoundsCheck;
         };
         
         // A structure storing information about the location variables of the model.
@@ -78,7 +81,7 @@ namespace storm {
         // A structure storing information about the used variables of the program.
         struct VariableInformation {
             VariableInformation(storm::prism::Program const& program, bool outOfBoundsState = false);
-            VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, bool outOfBoundsState = false);
+            VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState);
             
             VariableInformation() = default;
             uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;

src/storm/settings/modules/BuildSettings.cpp

@@ -30,6 +30,7 @@ namespace storm {
             const std::string buildChoiceLabelOptionName = "buildchoicelab";
             const std::string buildStateValuationsOptionName = "buildstateval";
             const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate";
+            const std::string bitsForUnboundedVariablesOptionName = "int-bits";
             BuildSettings::BuildSettings() : ModuleSettings(moduleName) {
 
                 std::vector<std::string> explorationOrders = {"dfs", "bfs"};
@@ -44,10 +45,10 @@ namespace storm {
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, buildOutOfBoundsStateOptionName, false, "If set, a state for out-of-bounds valuations is added").build());
-
+                this->addOption(storm::settings::OptionBuilder(moduleName, bitsForUnboundedVariablesOptionName, false, "Sets the number of bits that is used for unbounded integer variables.")
+                                        .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build());
             }
 
-
             bool BuildSettings::isJitSet() const {
                 return this->getOption(jitOptionName).getHasOptionBeenSet();
             }
@@ -80,7 +81,6 @@ namespace storm {
                 return this->getOption(buildOutOfBoundsStateOptionName).getHasOptionBeenSet();
             }
 
-
             storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const {
                 std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();
                 if (explorationOrderAsString == "dfs") {
@@ -90,10 +90,15 @@ namespace storm {
                 }
                 STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'.");
             }
-
+            
             bool BuildSettings::isExplorationChecksSet() const {
                 return this->getOption(explorationChecksOptionName).getHasOptionBeenSet();
             }
+
+            uint64_t BuildSettings::getBitsForUnboundedVariables() const {
+                return this->getOption(bitsForUnboundedVariablesOptionName).getArgumentByName("number").getValueAsUnsignedInteger();
+            }
+
         }
 
 

src/storm/settings/modules/BuildSettings.h

@@ -80,6 +80,12 @@ namespace storm {
                  * @return
                  */
                 bool isBuildOutOfBoundsStateSet() const;
+                
+                /*!
+                 * Retrieves the number of bits that should be used to represent unbounded integer variables
+                 * @return
+                 */
+                uint64_t getBitsForUnboundedVariables() const;
 
 
                 // The name of the module.