diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 35390c7cb..d03cfe630 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/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(); } diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 00718e3f1..33152ca36 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -36,7 +36,7 @@ namespace storm { return boost::get(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; + } + } } diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index fe56994c7..c6106172b 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/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; }; diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 3217180f6..a1a683b5b 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/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>(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(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 << ")."); } diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 2be706715..bea64b0bf 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -1,3 +1,4 @@ +#include #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; } diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 54f7f1024..ce1dd1f7b 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -95,6 +95,9 @@ namespace storm { /// A comparator used to compare constants. storm::utility::ConstantsComparator comparator; + + /// A state that encodes the outOfBoundsState + CompressedState outOfBoundsState; }; } } diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index e5f4dc4e1..1de65ce30 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/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>(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() << "'."); } diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 26bd2ecf8..5da944839 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -13,6 +13,7 @@ #include "storm/exceptions/WrongFormatException.h" #include +#include 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> const& parallelAutomata) : totalBitOffset(0) { + VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector> 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()) { diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index 764881e80..2e51f7db7 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -3,6 +3,7 @@ #include #include +#include #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> const& parallelAutomata); + VariableInformation(storm::prism::Program const& program, bool outOfBoundsState = false); + VariableInformation(storm::jani::Model const& model, std::vector> 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 integerVariables; + private: + boost::optional deadlockBit; + /*! * Sorts the variables to establish a known ordering. */ diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index a813b08fa..536dd26ea 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/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 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(); diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index 4ef0f5193..e9ec41dc1 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/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;