From a8cc93386ff737b3ae8236862849e79fc99d9044 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Fri, 24 May 2024 16:53:37 +0200 Subject: [PATCH] Added option to limit the number of explored states (#521) * Added option to limit the number of explored states Added option `--build:state limit ` which, if set, stops expanding new states once the given `` of states has been found. This is useful for, e.g., debugging models that normally would be too large. Unexplored states get a label `"unexplored"` assigned to them. This even allows to calculate the probability to exit the fraction of the explored state space --- src/storm/builder/ExplicitModelBuilder.cpp | 24 ++++++++--- src/storm/builder/ExplicitModelBuilder.h | 6 +++ .../generator/JaniNextStateGenerator.cpp | 8 ++-- src/storm/generator/JaniNextStateGenerator.h | 3 +- src/storm/generator/NextStateGenerator.cpp | 40 +++++++++---------- src/storm/generator/NextStateGenerator.h | 9 ++++- .../generator/PrismNextStateGenerator.cpp | 10 ++--- src/storm/generator/PrismNextStateGenerator.h | 3 +- src/storm/settings/modules/BuildSettings.cpp | 16 ++++++++ src/storm/settings/modules/BuildSettings.h | 10 +++++ src/storm/storage/sparse/StateStorage.cpp | 3 +- src/storm/storage/sparse/StateStorage.h | 3 ++ 12 files changed, 95 insertions(+), 40 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 348edc699a..4871df253b 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -55,9 +55,13 @@ uint64_t ExplicitStateLookup::size() const { } template -ExplicitModelBuilder::Options::Options() - : explorationOrder(storm::settings::getModule().getExplorationOrder()) { - // Intentionally left empty. +ExplicitModelBuilder::Options::Options() { + auto const& buildSettings = storm::settings::getModule(); + explorationOrder = buildSettings.getExplorationOrder(); + fixDeadlocks = !buildSettings.isDontFixDeadlocksSet(); + if (buildSettings.isExplorationStateLimitSet()) { + explorationStateLimit = buildSettings.getExplorationStateLimit(); + } } template @@ -193,14 +197,22 @@ void ExplicitModelBuilder::buildMatrices( if (stateAndChoiceInformationBuilder.isBuildStateValuations()) { generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuationsBuilder()); } - storm::generator::StateBehavior behavior = generator->expand(stateToIdCallback); + + storm::generator::StateBehavior behavior; + // If the exploration state limit is set and the limit is reached, we stop the exploration. + bool const stateLimitExceeded = options.explorationStateLimit.has_value() && stateStorage.getNumberOfStates() >= options.explorationStateLimit.value(); + if (!stateLimitExceeded) { + behavior = generator->expand(stateToIdCallback); + } // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { - if (!storm::settings::getModule().isDontFixDeadlocksSet() || !behavior.wasExpanded()) { + if (options.fixDeadlocks || !behavior.wasExpanded()) { // If the behavior was actually expanded and yet there are no transitions, then we have a deadlock state. if (behavior.wasExpanded()) { this->stateStorage.deadlockStateIndices.push_back(currentIndex); + } else { + this->stateStorage.unexploredStateIndices.push_back(currentIndex); } if (!generator->isDeterministicModel()) { @@ -419,7 +431,7 @@ storm::storage::sparse::ModelComponents ExplicitMode template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { - return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); + return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices, stateStorage.unexploredStateIndices); } // Explicitly instantiate the class. diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 1a2d511977..ab702703d2 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -76,6 +76,12 @@ class ExplicitModelBuilder { // The order in which to explore the model. ExplorationOrder explorationOrder; + + // If set, deadlocks states will be fixed by adding a self-loop with probability 1. + bool fixDeadlocks; + + // If set, no further states will be explored once the given number is exceeded. + std::optional explorationStateLimit; }; /*! diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 28d6386538..f036d96849 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -119,7 +119,7 @@ JaniNextStateGenerator::JaniNextStateGenerator(storm::jani this->terminalStates.emplace_back(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second); } else { // If it's a label, i.e. refers to a transient boolean variable we do some sanity checks first - if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") { + if (!this->isSpecialLabel(expressionOrLabelAndBool.first.getLabel())) { STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()), storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); @@ -1213,7 +1213,8 @@ storm::builder::RewardModelInformation JaniNextStateGenerator storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, - std::vector const& deadlockStateIndices) { + std::vector const& deadlockStateIndices, + std::vector const& unexploredStateIndices) { // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. std::vector> transientVariableExpressions; @@ -1224,7 +1225,8 @@ storm::models::sparse::StateLabeling JaniNextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions); + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, unexploredStateIndices, + transientVariableExpressions); } template diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 4a2d341256..3a8817f458 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -59,7 +59,8 @@ class JaniNextStateGenerator : public NextStateGenerator { virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, - std::vector const& deadlockStateIndices = {}) override; + std::vector const& deadlockStateIndices = {}, + std::vector const& unexploredStateIndices = {}) override; virtual std::shared_ptr generateChoiceOrigins(std::vector& dataForChoiceOrigins) const override; diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 376fcc6021..1283510a38 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -174,7 +174,8 @@ storm::storage::sparse::StateValuations NextStateGenerator template storm::models::sparse::StateLabeling NextStateGenerator::label( storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, - std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { + std::vector const& deadlockStateIndices, std::vector const& unexploredStateIndices, + std::vector> labelsAndExpressions) { labelsAndExpressions.insert(labelsAndExpressions.end(), this->options.getExpressionLabels().begin(), this->options.getExpressionLabels().end()); // Make the labels unique. @@ -209,39 +210,36 @@ storm::models::sparse::StateLabeling NextStateGenerator::l } } - if (!result.containsLabel("init")) { - // Also label the initial state with the special label "init". - result.addLabel("init"); - for (auto index : initialStateIndices) { - result.addLabelToState("init", index); - } - } - if (!result.containsLabel("deadlock")) { - result.addLabel("deadlock"); - for (auto index : deadlockStateIndices) { - result.addLabelToState("deadlock", index); + auto addSpecialLabel = [&result](std::string const& label, auto const& indices) { + if (!result.containsLabel(label)) { + result.addLabel(label); + for (auto index : indices) { + result.addLabelToState(label, index); + } } - } - + }; + addSpecialLabel("init", initialStateIndices); + addSpecialLabel("deadlock", deadlockStateIndices); + addSpecialLabel("unexplored", unexploredStateIndices); if (this->options.isAddOverlappingGuardLabelSet()) { STORM_LOG_THROW(!result.containsLabel("overlap_guards"), storm::exceptions::WrongFormatException, "Label 'overlap_guards' is reserved when adding overlapping guard labels"); - result.addLabel("overlap_guards"); - for (auto index : overlappingGuardStates.get()) { - result.addLabelToState("overlap_guards", index); - } + addSpecialLabel("overlap_guards", overlappingGuardStates.get()); } - if (this->options.isAddOutOfBoundsStateSet() && 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)); + addSpecialLabel("out_of_bounds", std::vector{stateStorage.stateToId.getValue(outOfBoundsState)}); } return result; } +template +bool NextStateGenerator::isSpecialLabel(std::string const& label) const { + return label == "init" || label == "deadlock" || label == "unexplored" || label == "overlap_guards" || label == "out_of_bounds"; +} + template void NextStateGenerator::unpackTransientVariableValuesIntoEvaluator(CompressedState const&, storm::expressions::ExpressionEvaluator&) const { diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 1ccda3b0d2..2923b85a6e 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -123,7 +123,8 @@ class NextStateGenerator { virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, - std::vector const& deadlockStateIndices = {}) = 0; + std::vector const& deadlockStateIndices = {}, + std::vector const& unexploredStateIndices = {}) = 0; NextStateGeneratorOptions const& getOptions() const; @@ -139,11 +140,17 @@ class NextStateGenerator { void remapStateIds(std::function const& remapping); protected: + /*! + * Checks if the input label has a special purpose (e.g. "init", "deadlock", "unexplored", "overlap_guards", "out_of_bounds"). + */ + bool isSpecialLabel(std::string const& label) const; + /*! * Creates the state labeling for the given states using the provided labels and expressions. */ storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, + std::vector const& unexploredStateIndices, std::vector> labelsAndExpressions); /*! diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 174d25b9e9..1b321b6988 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -90,8 +90,7 @@ PrismNextStateGenerator::PrismNextStateGenerator(storm::pr std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second)); } else { // If the label is not present in the program and is not a special one, we raise an error. - STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", - storm::exceptions::InvalidArgumentException, + STORM_LOG_THROW(this->isSpecialLabel(expressionOrLabelAndBool.first.getLabel()), storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); } } @@ -815,7 +814,8 @@ std::map PrismNextStateGenerator storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices, - std::vector const& deadlockStateIndices) { + std::vector const& deadlockStateIndices, + std::vector const& unexploredStateIndices) { // Gather a vector of labels and their expressions. std::vector> labels; if (this->options.isBuildAllLabelsSet()) { @@ -827,13 +827,13 @@ storm::models::sparse::StateLabeling PrismNextStateGeneratorisSpecialLabel(labelName), storm::exceptions::InvalidArgumentException, "Cannot build labeling for unknown label '" << labelName << "'."); } } } - return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, labels); + return NextStateGenerator::label(stateStorage, initialStateIndices, deadlockStateIndices, unexploredStateIndices, labels); } template diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index f499cf8673..bd39af624f 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -43,7 +43,8 @@ class PrismNextStateGenerator : public NextStateGenerator virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage const& stateStorage, std::vector const& initialStateIndices = {}, - std::vector const& deadlockStateIndices = {}) override; + std::vector const& deadlockStateIndices = {}, + std::vector const& unexploredStateIndices = {}) override; virtual std::shared_ptr generateChoiceOrigins(std::vector& dataForChoiceOrigins) const override; diff --git a/src/storm/settings/modules/BuildSettings.cpp b/src/storm/settings/modules/BuildSettings.cpp index 8cb1f8ad4a..bc531f25e4 100644 --- a/src/storm/settings/modules/BuildSettings.cpp +++ b/src/storm/settings/modules/BuildSettings.cpp @@ -39,6 +39,7 @@ const std::string buildOverlappingGuardsLabelOptionName = "build-overlapping-gua const std::string noSimplifyOptionName = "no-simplify"; const std::string bitsForUnboundedVariablesOptionName = "int-bits"; const std::string performLocationElimination = "location-elimination"; +const std::string explorationStateLimitOptionName = "state-limit"; BuildSettings::BuildSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, @@ -115,6 +116,12 @@ BuildSettings::BuildSettings() : ModuleSettings(moduleName) { .makeOptional() .build()) .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, explorationStateLimitOptionName, false, + "Potentially stopped exploration once the specified number of states is exceeded.") + .setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "states to explore before stopping.").build()) + .build()); } bool BuildSettings::isExplorationOrderSet() const { @@ -206,6 +213,15 @@ uint64_t BuildSettings::getLocationEliminationLocationHeuristic() const { uint64_t BuildSettings::getLocationEliminationEdgesHeuristic() const { return this->getOption(performLocationElimination).getArgumentByName("edges-heuristic").getValueAsUnsignedInteger(); } + +bool BuildSettings::isExplorationStateLimitSet() const { + return this->getOption(explorationStateLimitOptionName).getHasOptionBeenSet(); +} + +uint64_t BuildSettings::getExplorationStateLimit() const { + return this->getOption(explorationStateLimitOptionName).getArgumentByName("number").getValueAsUnsignedInteger(); +} + } // namespace modules } // namespace settings diff --git a/src/storm/settings/modules/BuildSettings.h b/src/storm/settings/modules/BuildSettings.h index 345054eb54..ce885e0116 100644 --- a/src/storm/settings/modules/BuildSettings.h +++ b/src/storm/settings/modules/BuildSettings.h @@ -139,6 +139,16 @@ class BuildSettings : public ModuleSettings { */ uint64_t getLocationEliminationEdgesHeuristic() const; + /*! + * Retrieves whether an exploration state limit has been set in which case state space exploration might be stopped once the specified number is exceeded. + */ + bool isExplorationStateLimitSet() const; + + /*! + * Retrieves the state limit (if set). State space exploration might be stopped once the specified number is exceeded. + */ + uint64_t getExplorationStateLimit() const; + // The name of the module. static const std::string moduleName; }; diff --git a/src/storm/storage/sparse/StateStorage.cpp b/src/storm/storage/sparse/StateStorage.cpp index 467df54374..a24f3be529 100644 --- a/src/storm/storage/sparse/StateStorage.cpp +++ b/src/storm/storage/sparse/StateStorage.cpp @@ -5,8 +5,7 @@ namespace storage { namespace sparse { template -StateStorage::StateStorage(uint64_t bitsPerState) - : stateToId(bitsPerState, 100000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) { +StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 100000), bitsPerState(bitsPerState) { // Intentionally left empty. } diff --git a/src/storm/storage/sparse/StateStorage.h b/src/storm/storage/sparse/StateStorage.h index 238ca79009..c751ff5ae8 100644 --- a/src/storm/storage/sparse/StateStorage.h +++ b/src/storm/storage/sparse/StateStorage.h @@ -23,6 +23,9 @@ struct StateStorage { // A list of deadlock states. std::vector deadlockStateIndices; + // A list of unexplored states. + std::vector unexploredStateIndices; + // The number of bits of each state. uint64_t bitsPerState;