add option for sparse model builder to add a state encoding out-of-bounds state valuations to enable analysis of buggy models

src/storm-cli-utilities/model-handling.h

@@ -190,6 +190,7 @@ namespace storm {
             options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet());
             options.setBuildAllLabels(buildSettings.isBuildFullModelSet());
             options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet());
+            options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet());
             if (buildSettings.isBuildFullModelSet()) {
                 options.clearTerminalStates();
             }

src/storm/builder/BuilderOptions.cpp

@@ -36,7 +36,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), explorationChecks(false), showProgress(false), showProgressDelay(0) {
+        BuilderOptions::BuilderOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false), buildStateValuations(false), buildChoiceOrigins(false), explorationChecks(false), addOutOfBoundsState(false), showProgress(false), showProgressDelay(0) {
             // Intentionally left empty.
         }
         
@@ -159,7 +159,11 @@ namespace storm {
         bool BuilderOptions::isBuildAllLabelsSet() const {
             return buildAllLabels;
         }
-        
+
+        bool BuilderOptions::isAddOutOfBoundsStateSet() const {
+            return addOutOfBoundsState;
+        }
+
         BuilderOptions& BuilderOptions::setBuildAllRewardModels(bool newValue) {
             buildAllRewardModels = newValue;
             return *this;
@@ -229,5 +233,10 @@ namespace storm {
             return *this;
         }
 
+        BuilderOptions& BuilderOptions::setAddOutOfBoundsState(bool newValue) {
+            addOutOfBoundsState = newValue;
+            return *this;
+        }
+
     }
 }

src/storm/builder/BuilderOptions.h

@@ -107,6 +107,7 @@ namespace storm {
             bool isBuildAllLabelsSet() const;
             bool isExplorationChecksSet() const;
             bool isShowProgressSet() const;
+            bool isAddOutOfBoundsStateSet() const;
             uint64_t getShowProgressDelay() const;
 
             /**
@@ -155,7 +156,15 @@ namespace storm {
              * @return this
              */
             BuilderOptions& setExplorationChecks(bool newValue = true);
-            
+
+            /**
+             * Should a state for out of bounds be constructed
+             * @param newValue The new value (default true)
+             * @return this
+             */
+            BuilderOptions& setAddOutOfBoundsState(bool newValue = true);
+
+
         private:
             /// A flag that indicates whether all reward models are to be built. In this case, the reward model names are
             /// to be ignored.
@@ -188,10 +197,13 @@ namespace storm {
             
             /// A flag that stores whether exploration checks are to be performed.
             bool explorationChecks;
-            
+
+            /// A flag indicating that the an additional state for out of bounds should be created.
+            bool addOutOfBoundsState;
+
             /// A flag that stores whether the progress of exploration is to be printed.
             bool showProgress;
-            
+
             /// The delay for printing progress information.
             uint64_t showProgressDelay;
         };

src/storm/generator/JaniNextStateGenerator.cpp

@@ -52,7 +52,7 @@ namespace storm {
 
             // Now we are ready to initialize the variable information.
             this->checkValid();
-            this->variableInformation = VariableInformation(model, this->parallelAutomata);
+            this->variableInformation = VariableInformation(model, this->parallelAutomata, options.isAddOutOfBoundsStateSet());
             
             // Create a proper evalator.
             this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(model.getManager());
@@ -256,10 +256,15 @@ namespace storm {
                     ++integerIt;
                 }
                 int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression());
-                if (this->options.isExplorationChecksSet()) {
+                if (this->options.isAddOutOfBoundsStateSet()) {
+                    if (assignedValue < integerIt->lowerBound || assignedValue > integerIt->upperBound) {
+                        return this->outOfBoundsState;
+                    }
+                } else if (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() << "'.");
                 }
+
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
                 STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
             }

src/storm/generator/NextStateGenerator.cpp

@@ -1,3 +1,4 @@
+#include <storm/exceptions/WrongFormatException.h>
 #include "storm/generator/NextStateGenerator.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
@@ -99,6 +100,12 @@ namespace storm {
                     result.addLabelToState("deadlock", index);
                 }
             }
+
+            if (stateStorage.stateToId.contains(outOfBoundsState)) {
+                STORM_LOG_THROW(!result.containsLabel("out_of_bounds"),storm::exceptions::WrongFormatException, "Label 'out_of_bounds' is reserved when adding out of bounds states.");
+                result.addLabel("out_of_bounds");
+                result.addLabelToState("out_of_bounds", stateStorage.stateToId.getValue(outOfBoundsState));
+            }
             
             return result;
         }

src/storm/generator/NextStateGenerator.h

@@ -95,6 +95,9 @@ namespace storm {
             
             /// A comparator used to compare constants.
             storm::utility::ConstantsComparator<ValueType> comparator;
+
+            /// A state that encodes the outOfBoundsState
+            CompressedState outOfBoundsState;
         };
     }
 }

src/storm/generator/PrismNextStateGenerator.cpp

@@ -33,7 +33,7 @@ namespace storm {
                         
             // Only after checking validity of the program, we initialize the variable information.
             this->checkValid();
-            this->variableInformation = VariableInformation(program);
+            this->variableInformation = VariableInformation(program, options.isAddOutOfBoundsStateSet());
             
             // Create a proper evalator.
             this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager());
@@ -318,7 +318,11 @@ namespace storm {
                     ++integerIt;
                 }
                 int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getExpression());
-                if (this->options.isExplorationChecksSet()) {
+                if (this->options.isAddOutOfBoundsStateSet()) {
+                    if (assignedValue < integerIt->lowerBound || assignedValue > integerIt->upperBound) {
+                        return this->outOfBoundsState;
+                    }
+                } else if (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

@@ -13,6 +13,7 @@
 #include "storm/exceptions/WrongFormatException.h"
 
 #include <cmath>
+#include <storm/exceptions/InvalidJaniException.h>
 
 namespace storm {
     namespace generator {
@@ -29,7 +30,13 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        VariableInformation::VariableInformation(storm::prism::Program const& program) : totalBitOffset(0) {
+        VariableInformation::VariableInformation(storm::prism::Program const& program, bool outOfBoundsState) : totalBitOffset(0) {
+            if(outOfBoundsState) {
+                deadlockBit = 0;
+                ++totalBitOffset;
+            } else {
+                deadlockBit = boost::none;
+            }
             for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
                 booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), totalBitOffset, true);
                 ++totalBitOffset;
@@ -58,7 +65,7 @@ namespace storm {
             sortVariables();
         }
         
-        VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata) : totalBitOffset(0) {
+        VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata, 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.");
@@ -66,6 +73,12 @@ namespace storm {
                 STORM_LOG_THROW(!automaton.getVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables in automaton '" << automaton.getName() << "'.");
                 STORM_LOG_THROW(!automaton.getVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient real variables in automaton '" << automaton.getName() << "'.");
             }
+            if(outOfBoundsState) {
+                deadlockBit = 0;
+                ++totalBitOffset;
+            } else {
+                deadlockBit = boost::none;
+            }
             
             for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
                 if (!variable.isTransient()) {

src/storm/generator/VariableInformation.h

@@ -3,6 +3,7 @@
 
 #include <vector>
 #include <boost/container/flat_map.hpp>
+#include <boost/optional/optional.hpp>
 
 #include "storm/storage/expressions/Variable.h"
 
@@ -74,8 +75,8 @@ namespace storm {
         
         // A structure storing information about the used variables of the program.
         struct VariableInformation {
-            VariableInformation(storm::prism::Program const& program);
-            VariableInformation(storm::jani::Model const& model, std::vector<std::reference_wrapper<storm::jani::Automaton const>> const& parallelAutomata);
+            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() = default;
             uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const;
@@ -91,8 +92,11 @@ namespace storm {
             
             /// The integer variables.
             std::vector<IntegerVariableInformation> integerVariables;
+
             
         private:
+            boost::optional<uint64_t> deadlockBit;
+
             /*!
              * Sorts the variables to establish a known ordering.
              */

src/storm/settings/modules/BuildSettings.cpp

@@ -29,6 +29,7 @@ namespace storm {
             const std::string fullModelBuildOptionName = "buildfull";
             const std::string buildChoiceLabelOptionName = "buildchoicelab";
             const std::string buildStateValuationsOptionName = "buildstateval";
+            const std::string buildOutOfBoundsStateOptionName = "buildoutofboundsstate";
             BuildSettings::BuildSettings() : ModuleSettings(moduleName) {
 
                 std::vector<std::string> explorationOrders = {"dfs", "bfs"};
@@ -42,6 +43,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
                                         .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());
 
             }
 
@@ -74,6 +76,10 @@ namespace storm {
                 return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet();
             }
 
+            bool BuildSettings::isBuildOutOfBoundsStateSet() const {
+                return this->getOption(buildOutOfBoundsStateOptionName).getHasOptionBeenSet();
+            }
+
 
             storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const {
                 std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString();

src/storm/settings/modules/BuildSettings.h

@@ -75,6 +75,12 @@ namespace storm {
                  */
                 bool isBuildStateValuationsSet() const;
 
+                /*!
+                 * Retrieves whether out of bounds state should be added
+                 * @return
+                 */
+                bool isBuildOutOfBoundsStateSet() const;
+
 
                 // The name of the module.
                 static const std::string moduleName;