diff --git a/src/storm/builder/BuilderOptions.cpp b/src/storm/builder/BuilderOptions.cpp index 069f44b68..a18bdbe49 100644 --- a/src/storm/builder/BuilderOptions.cpp +++ b/src/storm/builder/BuilderOptions.cpp @@ -37,7 +37,7 @@ namespace storm { return boost::get(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(); auto const& generalSettings = storm::settings::getModule(); 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; diff --git a/src/storm/builder/BuilderOptions.h b/src/storm/builder/BuilderOptions.h index 813f31b67..b592c1cba 100644 --- a/src/storm/builder/BuilderOptions.h +++ b/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; diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 3e41dcd57..9f764bee7 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/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() << "'."); } diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 74f073db8..f03ea7507 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/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() << "'."); } diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 3c06efc42..1f156cd8b 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/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> const& parallelAutomata, bool outOfBoundsState) : totalBitOffset(0) { + VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector> 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(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()); diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index a8d53090e..7189e3335 100644 --- a/src/storm/generator/VariableInformation.h +++ b/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> const& parallelAutomata, bool outOfBoundsState = false); + VariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata, uint64_t reservedBitsForUnboundedVariables, bool outOfBoundsState); VariableInformation() = default; uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const; diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 536dd26ea..2faa39fa5 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/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 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(); + } + } diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index e9ec41dc1..29575e2a3 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/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.