From 512a1ec5584e214c58d6fb4aef279a5c6d378628 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 17 Jun 2016 11:09:20 +0200 Subject: [PATCH] added special label 'deadlock' to models and builders Former-commit-id: 4edc57216ecdc210e8d4dbb8bb3745e0d21f6fdb --- src/builder/DdJaniModelBuilder.cpp | 32 ++++++---- src/builder/DdPrismModelBuilder.cpp | 63 ++++++++++++------- src/builder/ExplicitModelBuilder.cpp | 7 ++- src/generator/JaniNextStateGenerator.cpp | 6 +- src/generator/JaniNextStateGenerator.h | 2 +- src/generator/NextStateGenerator.cpp | 18 ++++-- src/generator/NextStateGenerator.h | 4 +- src/generator/PrismNextStateGenerator.cpp | 19 ++++-- src/generator/PrismNextStateGenerator.h | 2 +- src/models/symbolic/Ctmc.cpp | 3 +- src/models/symbolic/Ctmc.h | 2 + src/models/symbolic/DeterministicModel.cpp | 3 +- src/models/symbolic/DeterministicModel.h | 2 + src/models/symbolic/Dtmc.cpp | 3 +- src/models/symbolic/Dtmc.h | 2 + src/models/symbolic/Mdp.cpp | 3 +- src/models/symbolic/Mdp.h | 2 + src/models/symbolic/Model.cpp | 23 +++++-- src/models/symbolic/Model.h | 5 ++ src/models/symbolic/NondeterministicModel.cpp | 3 +- src/models/symbolic/NondeterministicModel.h | 2 + .../symbolic/StochasticTwoPlayerGame.cpp | 3 +- src/models/symbolic/StochasticTwoPlayerGame.h | 2 + src/storage/sparse/StateStorage.cpp | 2 +- src/storage/sparse/StateStorage.h | 3 + 25 files changed, 152 insertions(+), 64 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index a6770551d..2fe35e2c6 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1585,6 +1585,7 @@ namespace storm { struct ModelComponents { storm::dd::Bdd reachableStates; storm::dd::Bdd initialStates; + storm::dd::Bdd deadlockStates; storm::dd::Add transitionMatrix; std::unordered_map> rewardModels; }; @@ -1592,11 +1593,11 @@ namespace storm { template std::shared_ptr> createModel(storm::jani::ModelType const& modelType, CompositionVariables const& variables, ModelComponents const& modelComponents) { if (modelType == storm::jani::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Dtmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); } else if (modelType == storm::jani::ModelType::CTMC) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map(), modelComponents.rewardModels)); } else if (modelType == storm::jani::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map(), modelComponents.rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map(), modelComponents.rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } @@ -1624,7 +1625,7 @@ namespace storm { } template - void postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { + storm::dd::Bdd postprocessSystem(storm::jani::Model const& model, ComposerResult& system, CompositionVariables const& variables, typename DdJaniModelBuilder::Options const& options) { // For DTMCs, we normalize each row to 1 (to account for non-determinism). if (model.getModelType() == storm::jani::ModelType::DTMC) { system.transitions = system.transitions / system.transitions.sumAbstract(variables.columnMetaVariables); @@ -1647,7 +1648,9 @@ namespace storm { } system.transitions *= (!terminalStatesBdd).template toAdd(); + return terminalStatesBdd; } + return variables.manager->getBddZero(); } template @@ -1667,18 +1670,19 @@ namespace storm { } template - void fixDeadlocks(storm::jani::ModelType const& modelType, storm::dd::Add& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& reachableStates, CompositionVariables const& variables) { + storm::dd::Bdd fixDeadlocks(storm::jani::ModelType const& modelType, storm::dd::Add& transitionMatrix, storm::dd::Bdd const& transitionMatrixBdd, storm::dd::Bdd const& reachableStates, CompositionVariables const& variables) { // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(variables.columnMetaVariables); - storm::dd::Add deadlockStates = (reachableStates && !statesWithTransition).template toAdd(); + storm::dd::Bdd deadlockStates = reachableStates && !statesWithTransition; if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. if (!storm::settings::getModule().isDontFixDeadlocksSet()) { STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); + storm::dd::Add deadlockStatesAdd = deadlockStates.template toAdd(); uint_fast64_t count = 0; - for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) { + for (auto it = deadlockStatesAdd.begin(), ite = deadlockStatesAdd.end(); it != ite && count < 3; ++it, ++count) { STORM_LOG_INFO((*it).first.toPrettyString(variables.rowMetaVariables) << std::endl); } @@ -1693,7 +1697,7 @@ namespace storm { if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) { // For DTMCs, we can simply add the identity of the global module for all deadlock states. - transitionMatrix += deadlockStates * globalIdentity; + transitionMatrix += deadlockStatesAdd * globalIdentity; } else if (modelType == storm::jani::ModelType::MDP) { // For MDPs, however, we need to select an action associated with the self-loop, if we do not // want to attach a lot of self-loops to the deadlock states. @@ -1704,12 +1708,13 @@ namespace storm { for (auto const& variable : variables.localNondeterminismVariables) { action *= variables.manager->template getIdentity(variable); } - transitionMatrix += deadlockStates * globalIdentity * action; + transitionMatrix += deadlockStatesAdd * globalIdentity * action; } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); } } + return deadlockStates; } template @@ -1726,8 +1731,8 @@ namespace storm { // Postprocess the variables in place. postprocessVariables(this->model->getModelType(), system, variables); - // Postprocess the system in place. - postprocessSystem(*this->model, system, variables, options); + // Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off). + storm::dd::Bdd terminalStates = postprocessSystem(*this->model, system, variables, options); // Start creating the model components. ModelComponents modelComponents; @@ -1751,7 +1756,10 @@ namespace storm { modelComponents.transitionMatrix = system.transitions * reachableStatesAdd; // Fix deadlocks if existing. - fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables); + modelComponents.deadlockStates = fixDeadlocks(this->model->getModelType(), modelComponents.transitionMatrix, transitionMatrixBdd, modelComponents.reachableStates, variables); + + // Cut the deadlock states by removing all states that we 'converted' to deadlock states by making them terminal. + modelComponents.deadlockStates = modelComponents.deadlockStates && !terminalStates; // Finally, create the model. return createModel(this->model->getModelType(), variables, modelComponents); diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index dae747228..1f38fa4a8 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1265,39 +1265,51 @@ namespace storm { storm::dd::Add stateActionDd = system.stateActionDd; // If we were asked to treat some states as terminal states, we cut away their transitions now. + storm::dd::Bdd terminalStatesBdd = generationInfo.manager->getBddZero(); if (options.terminalStates || options.negatedTerminalStates) { std::map constantsSubstitution = preparedProgram->getConstantsSubstitution(); - storm::dd::Bdd terminalStatesBdd = generationInfo.manager->getBddZero(); if (options.terminalStates) { storm::expressions::Expression terminalExpression; if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { terminalExpression = boost::get(options.terminalStates.get()); } else { std::string const& labelName = boost::get(options.terminalStates.get()); - terminalExpression = preparedProgram->getLabelExpression(labelName); - } - - // If the expression refers to constants of the model, we need to substitute them. - terminalExpression = terminalExpression.substitute(constantsSubstitution); + if (program.hasLabel(labelName)) { + terminalExpression = preparedProgram->getLabelExpression(labelName); + } else { + STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + } + } - STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); - terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); + if (terminalExpression.isInitialized()) { + // If the expression refers to constants of the model, we need to substitute them. + terminalExpression = terminalExpression.substitute(constantsSubstitution); + + STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal."); + terminalStatesBdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression).toBdd(); + } } if (options.negatedTerminalStates) { storm::expressions::Expression negatedTerminalExpression; if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) { negatedTerminalExpression = boost::get(options.negatedTerminalStates.get()); } else { - std::string const& labelName = boost::get(options.terminalStates.get()); - negatedTerminalExpression = preparedProgram->getLabelExpression(labelName); + std::string const& labelName = boost::get(options.negatedTerminalStates.get()); + if (program.hasLabel(labelName)) { + negatedTerminalExpression = preparedProgram->getLabelExpression(labelName); + } else { + STORM_LOG_THROW(labelName == "init" || labelName == "deadlock", storm::exceptions::InvalidArgumentException, "Terminal states refer to illegal label '" << labelName << "'."); + } } - // If the expression refers to constants of the model, we need to substitute them. - negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution); - - STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); - terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); + if (negatedTerminalExpression.isInitialized()) { + // If the expression refers to constants of the model, we need to substitute them. + negatedTerminalExpression = negatedTerminalExpression.substitute(constantsSubstitution); + + STORM_LOG_TRACE("Making the states *not* satisfying " << negatedTerminalExpression << " terminal."); + terminalStatesBdd |= !generationInfo.rowExpressionAdapter->translateExpression(negatedTerminalExpression).toBdd(); + } } transitionMatrix *= (!terminalStatesBdd).template toAdd(); @@ -1318,15 +1330,17 @@ namespace storm { // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise. storm::dd::Bdd statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables); - storm::dd::Add deadlockStates = (reachableStates && !statesWithTransition).template toAdd(); + storm::dd::Bdd deadlockStates = reachableStates && !statesWithTransition; + // If there are deadlocks, either fix them or raise an error. if (!deadlockStates.isZero()) { // If we need to fix deadlocks, we do so now. if (!storm::settings::getModule().isDontFixDeadlocksSet()) { STORM_LOG_INFO("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states. The first three of these states are: "); - + + storm::dd::Add deadlockStatesAdd = deadlockStates.template toAdd(); uint_fast64_t count = 0; - for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) { + for (auto it = deadlockStatesAdd.begin(), ite = deadlockStatesAdd.end(); it != ite && count < 3; ++it, ++count) { STORM_LOG_INFO((*it).first.toPrettyString(generationInfo.rowMetaVariables) << std::endl); } @@ -1339,7 +1353,7 @@ namespace storm { } // For DTMCs, we can simply add the identity of the global module for all deadlock states. - transitionMatrix += deadlockStates * identity; + transitionMatrix += deadlockStatesAdd * identity; } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { // For MDPs, however, we need to select an action associated with the self-loop, if we do not // want to attach a lot of self-loops to the deadlock states. @@ -1351,13 +1365,16 @@ namespace storm { for (auto const& var : generationInfo.allGlobalVariables) { action *= generationInfo.variableToIdentityMap.at(var); } - transitionMatrix += deadlockStates * globalModule.identity * action; + transitionMatrix += deadlockStatesAdd * globalModule.identity * action; } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically."); } } + // Reduce the deadlock states by the states that we did simply not explore. + deadlockStates = deadlockStates && !terminalStatesBdd; + // Now build the reward models. std::vector> selectedRewardModels; @@ -1389,11 +1406,11 @@ namespace storm { } if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Dtmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels)); } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); + return std::shared_ptr>(new storm::models::symbolic::Mdp(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, generationInfo.allNondeterminismVariables, labelToExpressionMapping, rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type."); } diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index ff5cb2ea6..352694187 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -210,6 +210,11 @@ namespace storm { // If there is no behavior, we might have to introduce a self-loop. if (behavior.empty()) { if (!storm::settings::getModule().isDontFixDeadlocksSet() || !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); + } + if (generator->getOptions().isBuildChoiceLabelsSet()) { // Insert empty choice labeling for added self-loop transitions. choiceLabels.get().push_back(boost::container::flat_set()); @@ -342,7 +347,7 @@ namespace storm { template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { - return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices); + return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); } // Explicitly instantiate the class. diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 10186bb98..7202ebcc7 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -32,7 +32,7 @@ namespace storm { if (expressionOrLabelAndBool.first.isExpression()) { this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot make label terminal for JANI models."); + STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); } } } @@ -487,8 +487,8 @@ namespace storm { } template - storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { - return NextStateGenerator::label(states, initialStateIndices, {}); + storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { + return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, {}); } template class JaniNextStateGenerator; diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h index 350377eec..316d6e074 100644 --- a/src/generator/JaniNextStateGenerator.h +++ b/src/generator/JaniNextStateGenerator.h @@ -24,7 +24,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; private: /*! diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index 6e9f67fa6..00b8d794c 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -244,7 +244,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector> labelsAndExpressions) { + storm::models::sparse::StateLabeling NextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions) { // Make the labels unique. std::sort(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; } ); auto it = std::unique(labelsAndExpressions.begin(), labelsAndExpressions.end(), [] (std::pair const& a, std::pair const& b) { return a.first == b.first; } ); @@ -274,10 +274,18 @@ namespace storm { } } - // Also label the initial state with the special label "init". - result.addLabel("init"); - for (auto index : initialStateIndices) { - result.addLabelToState("init", index); + 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); + } } return result; diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 218efe32d..2e6214c70 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -177,7 +177,7 @@ namespace storm { storm::expressions::SimpleValuation toValuation(CompressedState const& state) const; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) = 0; + virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) = 0; NextStateGeneratorOptions const& getOptions() const; @@ -185,7 +185,7 @@ namespace storm { /*! * Creates the state labeling for the given states using the provided labels and expressions. */ - storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector> labelsAndExpressions); + storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions); /// The options to be used for next-state generation. NextStateGeneratorOptions options; diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index b746913a0..1fc7392d3 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -59,7 +59,12 @@ namespace storm { if (expressionOrLabelAndBool.first.isExpression()) { this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); } else { - this->terminalStates.push_back(std::make_pair(this->program.getLabelExpression(expressionOrLabelAndBool.first.getLabel()), expressionOrLabelAndBool.second)); + if (program.hasLabel(expressionOrLabelAndBool.first.getLabel())) { + this->terminalStates.push_back(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, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'."); + } } } } @@ -162,6 +167,7 @@ namespace storm { } // Get all choices for the state. + result.setExpanded(); std::vector> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback); std::vector> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback); for (auto& choice : allLabeledChoices) { @@ -229,7 +235,6 @@ namespace storm { result.addChoice(std::move(choice)); } - result.setExpanded(); return result; } @@ -498,7 +503,7 @@ namespace storm { } template - storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { + storm::models::sparse::StateLabeling PrismNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { // Gather a vector of labels and their expressions. std::vector> labels; if (this->options.isBuildAllLabelsSet()) { @@ -507,11 +512,15 @@ namespace storm { } } else { for (auto const& labelName : this->options.getLabelNames()) { - labels.push_back(std::make_pair(labelName, program.getLabelExpression(labelName))); + 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, "Cannot build labeling for unknown label '" << labelName << "'."); + } } } - return NextStateGenerator::label(states, initialStateIndices, labels); + return NextStateGenerator::label(states, initialStateIndices, deadlockStateIndices, labels); } template diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h index 1a49225d0..652903c98 100644 --- a/src/generator/PrismNextStateGenerator.h +++ b/src/generator/PrismNextStateGenerator.h @@ -25,7 +25,7 @@ namespace storm { virtual std::size_t getNumberOfRewardModels() const override; virtual RewardModelInformation getRewardModelInformation(uint64_t const& index) const override; - virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; + virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}, std::vector const& deadlockStateIndices = {}) override; private: /*! diff --git a/src/models/symbolic/Ctmc.cpp b/src/models/symbolic/Ctmc.cpp index 64c3868d3..2f1e65aec 100644 --- a/src/models/symbolic/Ctmc.cpp +++ b/src/models/symbolic/Ctmc.cpp @@ -14,6 +14,7 @@ namespace storm { Ctmc::Ctmc(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -22,7 +23,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : DeterministicModel(storm::models::ModelType::Ctmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { exitRates = this->getTransitionMatrix().sumAbstract(this->getColumnVariables()); } diff --git a/src/models/symbolic/Ctmc.h b/src/models/symbolic/Ctmc.h index 79e116ca8..a9bcd9c91 100644 --- a/src/models/symbolic/Ctmc.h +++ b/src/models/symbolic/Ctmc.h @@ -30,6 +30,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row @@ -44,6 +45,7 @@ namespace storm { Ctmc(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, diff --git a/src/models/symbolic/DeterministicModel.cpp b/src/models/symbolic/DeterministicModel.cpp index ed6ff3f4a..66f97bc87 100644 --- a/src/models/symbolic/DeterministicModel.cpp +++ b/src/models/symbolic/DeterministicModel.cpp @@ -15,6 +15,7 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -23,7 +24,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { // Intentionally left empty. } diff --git a/src/models/symbolic/DeterministicModel.h b/src/models/symbolic/DeterministicModel.h index 6fab1b8db..d8448ecf0 100644 --- a/src/models/symbolic/DeterministicModel.h +++ b/src/models/symbolic/DeterministicModel.h @@ -31,6 +31,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row @@ -46,6 +47,7 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, diff --git a/src/models/symbolic/Dtmc.cpp b/src/models/symbolic/Dtmc.cpp index 443577dae..a9483862f 100644 --- a/src/models/symbolic/Dtmc.cpp +++ b/src/models/symbolic/Dtmc.cpp @@ -14,6 +14,7 @@ namespace storm { Dtmc::Dtmc(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -22,7 +23,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : DeterministicModel(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { + : DeterministicModel(storm::models::ModelType::Dtmc, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels) { // Intentionally left empty. } diff --git a/src/models/symbolic/Dtmc.h b/src/models/symbolic/Dtmc.h index 91ba3be07..7fbce42e0 100644 --- a/src/models/symbolic/Dtmc.h +++ b/src/models/symbolic/Dtmc.h @@ -30,6 +30,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row @@ -44,6 +45,7 @@ namespace storm { Dtmc(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, diff --git a/src/models/symbolic/Mdp.cpp b/src/models/symbolic/Mdp.cpp index 4c68e0f44..70017195a 100644 --- a/src/models/symbolic/Mdp.cpp +++ b/src/models/symbolic/Mdp.cpp @@ -14,6 +14,7 @@ namespace storm { Mdp::Mdp(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -23,7 +24,7 @@ namespace storm { std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : NondeterministicModel(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels) { + : NondeterministicModel(storm::models::ModelType::Mdp, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels) { // Intentionally left empty. } diff --git a/src/models/symbolic/Mdp.h b/src/models/symbolic/Mdp.h index 56be6ad67..9b37e4cea 100644 --- a/src/models/symbolic/Mdp.h +++ b/src/models/symbolic/Mdp.h @@ -31,6 +31,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row @@ -46,6 +47,7 @@ namespace storm { Mdp(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, diff --git a/src/models/symbolic/Model.cpp b/src/models/symbolic/Model.cpp index b2549e5a2..25bc5404b 100644 --- a/src/models/symbolic/Model.cpp +++ b/src/models/symbolic/Model.cpp @@ -21,6 +21,7 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -29,7 +30,7 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : ModelBase(modelType), manager(manager), reachableStates(reachableStates), initialStates(initialStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), columnExpressionAdapter(columnExpressionAdapter), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) { + : ModelBase(modelType), manager(manager), reachableStates(reachableStates), initialStates(initialStates), deadlockStates(deadlockStates), transitionMatrix(transitionMatrix), rowVariables(rowVariables), rowExpressionAdapter(rowExpressionAdapter), columnVariables(columnVariables), columnExpressionAdapter(columnExpressionAdapter), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), labelToExpressionMap(labelToExpressionMap), rewardModels(rewardModels) { // Intentionally left empty. } @@ -65,8 +66,17 @@ namespace storm { template storm::dd::Bdd Model::getStates(std::string const& label) const { - STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); - return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)).toBdd() && this->reachableStates; + auto labelIt = labelToExpressionMap.find(label); + if (labelIt != labelToExpressionMap.end()) { + return rowExpressionAdapter->translateExpression(labelIt->second).toBdd() && this->reachableStates; + } else { + if (label == "init") { + return initialStates; + } else if (label == "deadlock") { + return deadlockStates; + } + } + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "The label " << label << " is invalid for the labeling of the model."); } template @@ -76,7 +86,12 @@ namespace storm { template bool Model::hasLabel(std::string const& label) const { - return labelToExpressionMap.find(label) != labelToExpressionMap.end(); + auto labelIt = labelToExpressionMap.find(label); + if (labelIt != labelToExpressionMap.end()) { + return true; + } else { + return label == "init" || label == "deadlock"; + } } template diff --git a/src/models/symbolic/Model.h b/src/models/symbolic/Model.h index 085c5075f..b2e9d3e87 100644 --- a/src/models/symbolic/Model.h +++ b/src/models/symbolic/Model.h @@ -66,6 +66,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row @@ -81,6 +82,7 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -291,6 +293,9 @@ namespace storm { // A vector representing the initial states of the model. storm::dd::Bdd initialStates; + // A vector representing the deadlock states of the model. + storm::dd::Bdd deadlockStates; + // A matrix representing transition relation. storm::dd::Add transitionMatrix; diff --git a/src/models/symbolic/NondeterministicModel.cpp b/src/models/symbolic/NondeterministicModel.cpp index 1ac1b5436..e5fead0a9 100644 --- a/src/models/symbolic/NondeterministicModel.cpp +++ b/src/models/symbolic/NondeterministicModel.cpp @@ -15,6 +15,7 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -24,7 +25,7 @@ namespace storm { std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : Model(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { + : Model(modelType, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, rewardModels), nondeterminismVariables(nondeterminismVariables) { // Prepare the mask of illegal nondeterministic choices. illegalMask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()); diff --git a/src/models/symbolic/NondeterministicModel.h b/src/models/symbolic/NondeterministicModel.h index 6596bffe9..749eac3f2 100644 --- a/src/models/symbolic/NondeterministicModel.h +++ b/src/models/symbolic/NondeterministicModel.h @@ -31,6 +31,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row @@ -47,6 +48,7 @@ namespace storm { std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp index 6d8183a61..8d2686d64 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp @@ -14,6 +14,7 @@ namespace storm { StochasticTwoPlayerGame::StochasticTwoPlayerGame(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, @@ -25,7 +26,7 @@ namespace storm { std::set const& nondeterminismVariables, std::map labelToExpressionMap, std::unordered_map const& rewardModels) - : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { + : NondeterministicModel(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, deadlockStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) { // Intentionally left empty. } diff --git a/src/models/symbolic/StochasticTwoPlayerGame.h b/src/models/symbolic/StochasticTwoPlayerGame.h index 4cf487dc8..754b15742 100644 --- a/src/models/symbolic/StochasticTwoPlayerGame.h +++ b/src/models/symbolic/StochasticTwoPlayerGame.h @@ -30,6 +30,7 @@ namespace storm { * @param manager The manager responsible for the decision diagrams. * @param reachableStates A DD representing the reachable states. * @param initialStates A DD representing the initial states of the model. + * @param deadlockStates A DD representing the deadlock states of the model. * @param transitionMatrix The matrix representing the transitions in the model. * @param rowVariables The set of row meta variables used in the DDs. * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row @@ -47,6 +48,7 @@ namespace storm { StochasticTwoPlayerGame(std::shared_ptr> manager, storm::dd::Bdd reachableStates, storm::dd::Bdd initialStates, + storm::dd::Bdd deadlockStates, storm::dd::Add transitionMatrix, std::set const& rowVariables, std::shared_ptr> rowExpressionAdapter, diff --git a/src/storage/sparse/StateStorage.cpp b/src/storage/sparse/StateStorage.cpp index 60af49179..f86bbcd48 100644 --- a/src/storage/sparse/StateStorage.cpp +++ b/src/storage/sparse/StateStorage.cpp @@ -5,7 +5,7 @@ namespace storm { namespace sparse { template - StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState) { + StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), deadlockStateIndices(), bitsPerState(bitsPerState) { // Intentionally left empty. } diff --git a/src/storage/sparse/StateStorage.h b/src/storage/sparse/StateStorage.h index eee1855c0..c35e743d1 100644 --- a/src/storage/sparse/StateStorage.h +++ b/src/storage/sparse/StateStorage.h @@ -21,6 +21,9 @@ namespace storm { // A list of initial states in terms of their global indices. std::vector initialStateIndices; + // A list of deadlock states. + std::vector deadlockStateIndices; + // The number of bits of each state. uint64_t bitsPerState;