Skip to content

Commit

Permalink
Added option to limit the number of explored states (#521)
Browse files Browse the repository at this point in the history 
* Added option to limit the number of explored states

Added option `--build:state limit <number>` which, if set, stops expanding new states once the given `<number>` 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
  • Loading branch information
@tquatmann
tquatmann authored May 24, 2024
1 parent c066774 commit a8cc933
Show file tree
Hide file tree
Showing 12 changed files with 95 additions and 40 deletions.
24 changes: 18 additions & 6 deletions src/storm/builder/ExplicitModelBuilder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,9 +55,13 @@ uint64_t ExplicitStateLookup<StateType>::size() const {
}

template<typename ValueType, typename RewardModelType, typename StateType>
ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options()
: explorationOrder(storm::settings::getModule<storm::settings::modules::BuildSettings>().getExplorationOrder()) {
// Intentionally left empty.
ExplicitModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() {
auto const& buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
explorationOrder = buildSettings.getExplorationOrder();
fixDeadlocks = !buildSettings.isDontFixDeadlocksSet();
if (buildSettings.isExplorationStateLimitSet()) {
explorationStateLimit = buildSettings.getExplorationStateLimit();
}
}

template<typename ValueType, typename RewardModelType, typename StateType>
Expand Down Expand Up @@ -193,14 +197,22 @@ void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(
if (stateAndChoiceInformationBuilder.isBuildStateValuations()) {
generator->addStateValuation(currentIndex, stateAndChoiceInformationBuilder.stateValuationsBuilder());
}
storm::generator::StateBehavior<ValueType, StateType> behavior = generator->expand(stateToIdCallback);

storm::generator::StateBehavior<ValueType, StateType> 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<storm::settings::modules::BuildSettings>().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()) {
Expand Down Expand Up @@ -419,7 +431,7 @@ storm::storage::sparse::ModelComponents<ValueType, RewardModelType> ExplicitMode

template<typename ValueType, typename RewardModelType, typename StateType>
storm::models::sparse::StateLabeling ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);
return generator->label(stateStorage, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices, stateStorage.unexploredStateIndices);
}

// Explicitly instantiate the class.
Expand Down
6 changes: 6 additions & 0 deletions src/storm/builder/ExplicitModelBuilder.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<StateType> explorationStateLimit;
};

/*!
Expand Down
8 changes: 5 additions & 3 deletions src/storm/generator/JaniNextStateGenerator.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ JaniNextStateGenerator<ValueType, StateType>::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() << "'.");
Expand Down Expand Up @@ -1213,7 +1213,8 @@ storm::builder::RewardModelInformation JaniNextStateGenerator<ValueType, StateTy
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage,
std::vector<StateType> const& initialStateIndices,
std::vector<StateType> const& deadlockStateIndices) {
std::vector<StateType> const& deadlockStateIndices,
std::vector<StateType> 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<std::pair<std::string, storm::expressions::Expression>> transientVariableExpressions;
Expand All @@ -1224,7 +1225,8 @@ storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType
}
}
}
return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, unexploredStateIndices,
transientVariableExpressions);
}

template<typename ValueType, typename StateType>
Expand Down
3 changes: 2 additions & 1 deletion src/storm/generator/JaniNextStateGenerator.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,8 @@ class JaniNextStateGenerator : public NextStateGenerator<ValueType, StateType> {

virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage,
std::vector<StateType> const& initialStateIndices = {},
std::vector<StateType> const& deadlockStateIndices = {}) override;
std::vector<StateType> const& deadlockStateIndices = {},
std::vector<StateType> const& unexploredStateIndices = {}) override;

virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;

Expand Down
40 changes: 19 additions & 21 deletions src/storm/generator/NextStateGenerator.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,8 @@ storm::storage::sparse::StateValuations NextStateGenerator<ValueType, StateType>
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::label(
storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices,
std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
std::vector<StateType> const& deadlockStateIndices, std::vector<StateType> const& unexploredStateIndices,
std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions) {
labelsAndExpressions.insert(labelsAndExpressions.end(), this->options.getExpressionLabels().begin(), this->options.getExpressionLabels().end());

// Make the labels unique.
Expand Down Expand Up @@ -209,39 +210,36 @@ storm::models::sparse::StateLabeling NextStateGenerator<ValueType, StateType>::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<typename ValueType, typename StateType>
bool NextStateGenerator<ValueType, StateType>::isSpecialLabel(std::string const& label) const {
return label == "init" || label == "deadlock" || label == "unexplored" || label == "overlap_guards" || label == "out_of_bounds";
}

template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::unpackTransientVariableValuesIntoEvaluator(CompressedState const&,
storm::expressions::ExpressionEvaluator<ValueType>&) const {
Expand Down
9 changes: 8 additions & 1 deletion src/storm/generator/NextStateGenerator.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,7 +123,8 @@ class NextStateGenerator {

virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage,
std::vector<StateType> const& initialStateIndices = {},
std::vector<StateType> const& deadlockStateIndices = {}) = 0;
std::vector<StateType> const& deadlockStateIndices = {},
std::vector<StateType> const& unexploredStateIndices = {}) = 0;

NextStateGeneratorOptions const& getOptions() const;

Expand All @@ -139,11 +140,17 @@ class NextStateGenerator {
void remapStateIds(std::function<StateType(StateType const&)> 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<StateType> const& stateStorage,
std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices,
std::vector<StateType> const& unexploredStateIndices,
std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);

/*!
Expand Down
10 changes: 5 additions & 5 deletions src/storm/generator/PrismNextStateGenerator.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,8 +90,7 @@ PrismNextStateGenerator<ValueType, StateType>::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() << "'.");
}
}
Expand Down Expand Up @@ -815,7 +814,8 @@ std::map<std::string, storm::storage::PlayerIndex> PrismNextStateGenerator<Value
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateType>::label(storm::storage::sparse::StateStorage<StateType> const& stateStorage,
std::vector<StateType> const& initialStateIndices,
std::vector<StateType> const& deadlockStateIndices) {
std::vector<StateType> const& deadlockStateIndices,
std::vector<StateType> const& unexploredStateIndices) {
// Gather a vector of labels and their expressions.
std::vector<std::pair<std::string, storm::expressions::Expression>> labels;
if (this->options.isBuildAllLabelsSet()) {
Expand All @@ -827,13 +827,13 @@ storm::models::sparse::StateLabeling PrismNextStateGenerator<ValueType, StateTyp
if (program.hasLabel(labelName)) {
labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName)));
} else {
STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException,
STORM_LOG_THROW(this->isSpecialLabel(labelName), storm::exceptions::InvalidArgumentException,
"Cannot build labeling for unknown label '" << labelName << "'.");
}
}
}

return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, labels);
return NextStateGenerator<ValueType, StateType>::label(stateStorage, initialStateIndices, deadlockStateIndices, unexploredStateIndices, labels);
}

template<typename ValueType, typename StateType>
Expand Down
3 changes: 2 additions & 1 deletion src/storm/generator/PrismNextStateGenerator.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,8 @@ class PrismNextStateGenerator : public NextStateGenerator<ValueType, StateType>

virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage,
std::vector<StateType> const& initialStateIndices = {},
std::vector<StateType> const& deadlockStateIndices = {}) override;
std::vector<StateType> const& deadlockStateIndices = {},
std::vector<StateType> const& unexploredStateIndices = {}) override;

virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;

Expand Down
16 changes: 16 additions & 0 deletions src/storm/settings/modules/BuildSettings.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions src/storm/settings/modules/BuildSettings.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
};
Expand Down
3 changes: 1 addition & 2 deletions src/storm/storage/sparse/StateStorage.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,7 @@ namespace storage {
namespace sparse {

template<typename StateType>
StateStorage<StateType>::StateStorage(uint64_t bitsPerState)
: stateToId(bitsPerState, 100000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) {
StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 100000), bitsPerState(bitsPerState) {
// Intentionally left empty.
}

Expand Down
3 changes: 3 additions & 0 deletions src/storm/storage/sparse/StateStorage.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,9 @@ struct StateStorage {
// A list of deadlock states.
std::vector<StateType> deadlockStateIndices;

// A list of unexplored states.
std::vector<StateType> unexploredStateIndices;

// The number of bits of each state.
uint64_t bitsPerState;

Expand Down

0 comments on commit a8cc933

Please sign in to comment.