diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 348edc699..4871df253 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 1a2d51197..ab702703d 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 08394e13e..496ee8627 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -119,7 +119,8 @@ 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 (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock" && + expressionOrLabelAndBool.first.getLabel() != "unexplored") { STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()), storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); @@ -1213,7 +1214,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 +1226,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 4a2d34125..3a8817f45 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 daec34f1a..f1ca08be8 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. @@ -222,6 +223,12 @@ storm::models::sparse::StateLabeling NextStateGenerator::l result.addLabelToState("deadlock", index); } } + if (!result.containsLabel("unexplored") && !unexploredStateIndices.empty()) { + result.addLabel("unexplored"); + for (auto index : unexploredStateIndices) { + result.addLabelToState("unexplored", index); + } + } if (this->options.isAddOverlappingGuardLabelSet()) { STORM_LOG_THROW(!result.containsLabel("overlap_guards"), storm::exceptions::WrongFormatException, diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 1ccda3b0d..cefd4378e 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; @@ -144,6 +145,7 @@ class NextStateGenerator { */ 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 174d25b9e..f677b3fae 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -90,7 +90,8 @@ 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_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock" || + expressionOrLabelAndBool.first.getLabel() == "unexplored", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); } @@ -815,7 +816,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 +829,13 @@ storm::models::sparse::StateLabeling PrismNextStateGenerator::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 f499cf867..bd39af624 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 8cb1f8ad4..bc531f25e 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 345054eb5..ce885e011 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 467df5437..a24f3be52 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 238ca7900..c751ff5ae 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;