diff --git a/resources/examples/testfiles/dtmc/die.pm b/resources/examples/testfiles/dtmc/die.pm index e41139001..1873bb8c1 100644 --- a/resources/examples/testfiles/dtmc/die.pm +++ b/resources/examples/testfiles/dtmc/die.pm @@ -1,5 +1,5 @@ // Knuth's model of a fair die using only fair coins -dtmc +mdp module die diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 0237985f0..e659209a3 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1,5 +1,4 @@ -#ifndef STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ -#define STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ +#pragma once #include #include @@ -11,7 +10,8 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/sparse/PrismChoiceOrigins.h" -#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" @@ -44,6 +44,9 @@ namespace storm { // The set of relevant labels. boost::container::flat_set relevantLabels; + // The set of labels that matter in terms of minimality. + boost::container::flat_set minimalityLabels; + // A set of labels that is definitely known to be taken in the final solution. boost::container::flat_set knownLabels; @@ -58,6 +61,9 @@ namespace storm { // The variables associated with the relevant labels. std::vector labelVariables; + // The variables associated with the labels that matter in terms of minimality. + std::vector minimalityLabelVariables; + // A mapping from relevant labels to their indices in the variable vector. std::map labelToIndexMap; @@ -93,30 +99,30 @@ namespace storm { * Computes the set of relevant labels in the model. Relevant labels are choice labels such that there exists * a scheduler that satisfies phi until psi with a nonzero probability. * - * @param mdp The MDP to search for relevant labels. + * @param model The model to search for relevant labels. * @param phiStates A bit vector representing all states that satisfy phi. * @param psiStates A bit vector representing all states that satisfy psi. + * @param dontCareLabels A set of labels that are "don't care" labels wrt. minimality. * @return A structure containing the relevant labels as well as states. */ - static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& dontCareLabels) { // Create result. RelevancyInformation relevancyInformation; // Compute all relevant states, i.e. states for which there exists a scheduler that has a non-zero // probabilitiy of satisfying phi until psi. - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates); relevancyInformation.relevantStates &= ~psiStates; STORM_LOG_DEBUG("Found " << relevancyInformation.relevantStates.getNumberOfSetBits() << " relevant states."); - STORM_LOG_DEBUG(relevancyInformation.relevantStates); // Retrieve some references for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); // Now traverse all choices of all relevant states and check whether there is a successor target state. - // If so, the associated labels become relevant. Also, if a choice of relevant state has at least one + // If so, the associated labels become relevant. Also, if a choice of a relevant state has at least one // relevant successor, the choice becomes relevant. for (auto state : relevancyInformation.relevantStates) { relevancyInformation.relevantChoicesForRelevantStates.emplace(state, std::list()); @@ -130,6 +136,7 @@ namespace storm { for (auto const& label : labelSets[row]) { relevancyInformation.relevantLabels.insert(label); } + if (!currentChoiceRelevant) { currentChoiceRelevant = true; relevancyInformation.relevantChoicesForRelevantStates[state].push_back(row); @@ -140,15 +147,15 @@ namespace storm { } // Compute the set of labels that are known to be taken in any case. - relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(mdp, labelSets, psiStates, relevancyInformation.relevantLabels); + relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(model, labelSets, psiStates, relevancyInformation.relevantLabels); if (!relevancyInformation.knownLabels.empty()) { boost::container::flat_set remainingLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); relevancyInformation.relevantLabels = remainingLabels; } - std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels." << std::endl; - + std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), dontCareLabels.begin(), dontCareLabels.end(), std::inserter(relevancyInformation.minimalityLabels, relevancyInformation.minimalityLabels.begin())); + STORM_LOG_DEBUG("Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels."); return relevancyInformation; } @@ -160,7 +167,7 @@ namespace storm { * @param relevantCommands A set of relevant labels for which to create the expressions. * @return A mapping from relevant labels to their corresponding expressions. */ - static VariableInformation createVariables(std::shared_ptr const& manager, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, RelevancyInformation const& relevancyInformation, bool createReachabilityVariables) { + static VariableInformation createVariables(std::shared_ptr const& manager, storm::models::sparse::Model const& model, storm::storage::BitVector const& psiStates, RelevancyInformation const& relevancyInformation, bool createReachabilityVariables) { VariableInformation variableInformation; variableInformation.manager = manager; @@ -178,6 +185,11 @@ namespace storm { variableInformation.labelVariables.push_back(manager->declareBooleanVariable(variableName.str())); + // Record if the label is among the ones that matter for minimality. + if (relevancyInformation.minimalityLabels.find(label) != relevancyInformation.minimalityLabels.end()) { + variableInformation.minimalityLabelVariables.push_back(variableInformation.labelVariables.back()); + } + // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); @@ -197,7 +209,7 @@ namespace storm { if (createReachabilityVariables) { variableInformation.hasReachabilityVariables = true; - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); for (auto state : relevancyInformation.relevantStates) { variableInformation.relevantStatesToOrderVariableIndexMap[state] = variableInformation.stateOrderVariables.size(); @@ -253,13 +265,10 @@ namespace storm { /*! * Asserts the constraints that are initially needed for the Fu-Malik procedure. * - * @param program The program for which to build the constraints. - * @param mdp The MDP that results from the given program. - * @param context The Z3 context in which to build the expressions. * @param solver The solver in which to assert the constraints. * @param variableInformation A structure with information about the variables for the labels. */ - static void assertFuMalikInitialConstraints(storm::prism::Program const& program, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, z3::context& context, z3::solver& solver, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { + static void assertFuMalikInitialConstraints(z3::solver& solver, VariableInformation const& variableInformation) { // Assert that at least one of the labels must be taken. z3::expr formula = variableInformation.labelVariables.at(0); for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) { @@ -272,12 +281,12 @@ namespace storm { * Asserts cuts that are derived from the explicit representation of the model and rule out a lot of * suboptimal solutions. * - * @param mdp The labeled MDP for which to compute the cuts. + * @param model The labeled model for which to compute the cuts. * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. */ - static void assertExplicitCuts(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { - // Walk through the MDP and + static void assertExplicitCuts(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + // Walk through the model and // * identify labels enabled in initial states // * identify labels that can directly precede a given action // * identify labels that directly reach a target state @@ -291,10 +300,10 @@ namespace storm { std::map, std::set>> followingLabels; std::map>> synchronizingLabels; - // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - storm::storage::BitVector const& initialStates = mdp.getInitialStates(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + storm::storage::BitVector const& initialStates = model.getInitialStates(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { @@ -552,16 +561,16 @@ namespace storm { * @param program The symbolic representation of the model in terms of a program. * @param solver The solver to use for the satisfiability evaluation. */ - static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Model const& model, std::vector> const& labelSets, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { // A container storing the label sets that may precede a given label set. std::map, std::set>> precedingLabelSets; // A container that maps labels to their reachable synchronization sets. std::map>> synchronizingLabels; - // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Compute the set of labels that may precede a given action. for (auto currentState : relevancyInformation.relevantStates) { @@ -871,22 +880,22 @@ namespace storm { /*! * Asserts constraints necessary to encode the reachability of at least one target state from the initial states. */ - static void assertReachabilityCuts(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertReachabilityCuts(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { if (!variableInformation.hasReachabilityVariables) { throw storm::exceptions::InvalidStateException() << "Impossible to assert reachability cuts without the necessary variables."; } - // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // First, we add the formulas that encode // (1) if an incoming transition is chosen, an outgoing one is chosen as well (for non-initial states) // (2) an outgoing transition out of the initial states is taken. storm::expressions::Expression initialStateExpression = variableInformation.manager->boolean(false); for (auto relevantState : relevancyInformation.relevantStates) { - if (!mdp.getInitialStates().get(relevantState)) { + if (!model.getInitialStates().get(relevantState)) { // Assert the constraints (1). boost::container::flat_set relevantPredecessors; for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { @@ -1300,7 +1309,7 @@ namespace storm { std::stringstream variableName; std::vector result; - std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.labelVariables); + std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.minimalityLabelVariables); for (uint_fast64_t i = 0; i < adderVariables.size(); ++i) { variableName.str(""); variableName.clear(); @@ -1340,32 +1349,32 @@ namespace storm { } /*! - * Analyzes the given sub-MDP that has a maximal reachability of zero (i.e. no psi states are reachable) and tries to construct assertions that aim to make at least one psi state reachable. + * Analyzes the given sub-model that has a maximal reachability of zero (i.e. no psi states are reachable) and tries to construct assertions that aim to make at least one psi state reachable. * * @param solver The solver to use for the satisfiability evaluation. - * @param subMdp The sub-MDP resulting from restricting the original MDP to the given command set. - * @param originalMdp The original MDP. + * @param subModel The sub-model resulting from restricting the original model to the given command set. + * @param originalModel The original model. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiState A bit vector characterizing all psi states in the model. * @param commandSet The currently chosen set of commands. * @param variableInformation A structure with information about the variables of the solver. */ - static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, std::vector> const& subLabelSets, storm::models::sparse::Mdp const& originalMdp, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { - storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); + static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + storm::storage::BitVector reachableStates(subModel.getNumberOfStates()); STORM_LOG_DEBUG("Analyzing solution with zero probability."); // Initialize the stack for the DFS. bool targetStateIsReachable = false; std::vector stack; - stack.reserve(subMdp.getNumberOfStates()); - for (auto initialState : subMdp.getInitialStates()) { + stack.reserve(subModel.getNumberOfStates()); + for (auto initialState : subModel.getInitialStates()) { stack.push_back(initialState); reachableStates.set(initialState, true); } - storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix const& transitionMatrix = subModel.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = subModel.getNondeterministicChoiceIndices(); // Now determine which states and labels are actually reachable. boost::container::flat_set reachableLabels; @@ -1404,12 +1413,12 @@ namespace storm { } storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; - storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subModel.getBackwardTransitions(), phiStates, psiStates); boost::container::flat_set locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); STORM_LOG_DEBUG("Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states."); // Search for states on the border of the reachable state space, i.e. states that are still reachable @@ -1421,7 +1430,7 @@ namespace storm { bool isBorderChoice = false; // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. - for (auto const& successorEntry : originalMdp.getTransitionMatrix().getRow(currentChoice)) { + for (auto const& successorEntry : originalModel.getTransitionMatrix().getRow(currentChoice)) { if (unreachableRelevantStates.get(successorEntry.getColumn())) { isBorderChoice = true; } @@ -1463,33 +1472,33 @@ namespace storm { } /*! - * Analyzes the given sub-MDP that has a non-zero maximal reachability and tries to construct assertions that aim to guide the solver to solutions + * Analyzes the given sub-model that has a non-zero maximal reachability and tries to construct assertions that aim to guide the solver to solutions * with an improved probability value. * * @param solver The solver to use for the satisfiability evaluation. - * @param subMdp The sub-MDP resulting from restricting the original MDP to the given command set. - * @param originalMdp The original MDP. + * @param subModel The sub-model resulting from restricting the original model to the given command set. + * @param originalModel The original model. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiState A bit vector characterizing all psi states in the model. * @param commandSet The currently chosen set of commands. * @param variableInformation A structure with information about the variables of the solver. */ - static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, std::vector> const& subLabelSets, storm::models::sparse::Mdp const& originalMdp, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Model const& subModel, std::vector> const& subLabelSets, storm::models::sparse::Model const& originalModel, std::vector> const& originalLabelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { STORM_LOG_DEBUG("Analyzing solution with insufficient probability."); - storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); + storm::storage::BitVector reachableStates(subModel.getNumberOfStates()); // Initialize the stack for the DFS. std::vector stack; - stack.reserve(subMdp.getNumberOfStates()); - for (auto initialState : subMdp.getInitialStates()) { + stack.reserve(subModel.getNumberOfStates()); + for (auto initialState : subModel.getInitialStates()) { stack.push_back(initialState); reachableStates.set(initialState, true); } - storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix const& transitionMatrix = subModel.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = subModel.getNondeterministicChoiceIndices(); // Now determine which states and labels are actually reachable. boost::container::flat_set reachableLabels; @@ -1522,12 +1531,12 @@ namespace storm { STORM_LOG_DEBUG("Successfully determined reachable state space."); storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; - storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subModel.getBackwardTransitions(), phiStates, psiStates); boost::container::flat_set locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); // Search for states for which we could enable another option and possibly improve the reachability probability. std::set> cutLabels; @@ -1570,20 +1579,20 @@ namespace storm { /*! - * Returns the submdp obtained from removing all choices that do not originate from the specified filterLabelSet. - * Also returns the Labelsets of the submdp + * Returns the sub-model obtained from removing all choices that do not originate from the specified filterLabelSet. + * Also returns the Labelsets of the sub-model. */ - static std::pair, std::vector>> restrictMdpToLabelSet(storm::models::sparse::Mdp const& mdp, boost::container::flat_set const& filterLabelSet) { + static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet) { std::vector> resultLabelSet; - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, mdp.getTransitionMatrix().getColumnCount(), 0, true, true, mdp.getTransitionMatrix().getRowGroupCount()); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, model.getTransitionMatrix().getColumnCount(), 0, true, true, model.getTransitionMatrix().getRowGroupCount()); // Check for each choice of each state, whether the choice commands are fully contained in the given command set. uint_fast64_t currentRow = 0; - for(uint_fast64_t state = 0; state < mdp.getNumberOfStates(); ++state) { + for(uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state) { bool stateHasValidChoice = false; - for (uint_fast64_t choice = mdp.getTransitionMatrix().getRowGroupIndices()[state]; choice < mdp.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { - auto const& choiceLabelSet = mdp.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(choice); + for (uint_fast64_t choice = model.getTransitionMatrix().getRowGroupIndices()[state]; choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { + auto const& choiceLabelSet = model.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(choice); bool choiceValid = std::includes(filterLabelSet.begin(), filterLabelSet.end(), choiceLabelSet.begin(), choiceLabelSet.end()); // If the choice is valid, copy over all its elements. @@ -1592,7 +1601,7 @@ namespace storm { transitionMatrixBuilder.newRowGroup(currentRow); } stateHasValidChoice = true; - for (auto const& entry : mdp.getTransitionMatrix().getRow(choice)) { + for (auto const& entry : model.getTransitionMatrix().getRow(choice)) { transitionMatrixBuilder.addNextValue(currentRow, entry.getColumn(), entry.getValue()); } resultLabelSet.push_back(choiceLabelSet); @@ -1610,17 +1619,40 @@ namespace storm { } } - storm::models::sparse::Mdp resultMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(mdp.getStateLabeling())); + std::shared_ptr> resultModel; + if (model.isOfType(storm::models::ModelType::Dtmc)) { + resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling())); + } else { + resultModel = std::make_shared>(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(model.getStateLabeling())); + } - return std::make_pair(std::move(resultMdp), std::move(resultLabelSet)); + return std::make_pair(resultModel, std::move(resultLabelSet)); } + static T computeMaximalReachabilityProbability(Environment const& env, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + T result = storm::utility::zero(); + + std::vector allStatesResult; + + STORM_LOG_DEBUG("Invoking model checker."); + if (model.isOfType(storm::models::ModelType::Dtmc)) { + allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false, storm::solver::GeneralLinearEquationSolverFactory()); + } else { + storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; + allStatesResult = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); + } + for (auto state : model.getInitialStates()) { + result = std::max(result, allStatesResult[state]); + } + return result; + } + public: /*! - * Computes the minimal command set that is needed in the given MDP to exceed the given probability threshold for satisfying phi until psi. + * Computes the minimal command set that is needed in the given model to exceed the given probability threshold for satisfying phi until psi. * - * @param program The program that was used to build the MDP. - * @param mdp The MDP in which to find the minimal command set. + * @param program The program that was used to build the model. + * @param model The sparse model in which to find the minimal command set. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiStates A bit vector characterizing all psi states in the model. * @param probabilityThreshold The threshold that is to be achieved or exceeded. @@ -1628,7 +1660,7 @@ namespace storm { * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check * is made and fails, an exception is thrown. */ - static boost::container::flat_set getMinimalCommandSet(Environment const& env,storm::prism::Program program, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { + static boost::container::flat_set getMinimalCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { #ifdef STORM_HAVE_Z3 // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); @@ -1649,37 +1681,33 @@ namespace storm { // (0) Obtain the label sets for each choice. // The label set of a choice corresponds to the set of prism commands that induce the choice. - STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to minimal command set is impossible for model without choice origins."); - STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); + STORM_LOG_THROW(model.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to minimal command set is impossible for model without choice origins."); + STORM_LOG_THROW(model.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = model.getChoiceOrigins()->asPrismChoiceOrigins(); std::vector> labelSets; - labelSets.reserve(mdp.getNumberOfChoices()); - for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) { + labelSets.reserve(model.getNumberOfChoices()); + for (uint_fast64_t choice = 0; choice < model.getNumberOfChoices(); ++choice) { labelSets.push_back(choiceOrigins.getCommandSet(choice)); } // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { - storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; - STORM_LOG_DEBUG("Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, mdp.getTransitionMatrix(), mdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); - for (auto state : mdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); - } + maximalReachabilityProbability = computeMaximalReachabilityProbability(env, model, phiStates, psiStates); + STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; } // (2) Identify all states and commands that are relevant, because only these need to be considered later. - RelevancyInformation relevancyInformation = determineRelevantStatesAndLabels(mdp, labelSets, phiStates, psiStates); + RelevancyInformation relevancyInformation = determineRelevantStatesAndLabels(model, labelSets, phiStates, psiStates, dontCareLabels); // (3) Create a solver. std::shared_ptr manager = std::make_shared(); std::unique_ptr solver = std::make_unique(*manager); // (4) Create the variables for the relevant commands. - VariableInformation variableInformation = createVariables(manager, mdp, psiStates, relevancyInformation, includeReachabilityEncoding); + VariableInformation variableInformation = createVariables(manager, model, psiStates, relevancyInformation, includeReachabilityEncoding); STORM_LOG_DEBUG("Created variables."); // (5) Now assert an adder whose result variables can later be used to constrain the nummber of label @@ -1690,12 +1718,12 @@ namespace storm { // (6) Add constraints that cut off a lot of suboptimal solutions. STORM_LOG_DEBUG("Asserting cuts."); - assertExplicitCuts(mdp, labelSets, psiStates, variableInformation, relevancyInformation, *solver); + assertExplicitCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted explicit cuts."); - assertSymbolicCuts(program, mdp, labelSets, variableInformation, relevancyInformation, *solver); + assertSymbolicCuts(program, model, labelSets, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted symbolic cuts."); if (includeReachabilityEncoding) { - assertReachabilityCuts(mdp, labelSets, psiStates, variableInformation, relevancyInformation, *solver); + assertReachabilityCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted reachability cuts."); } @@ -1706,12 +1734,18 @@ namespace storm { // satisfying phi until psi exceeds the given threshold, the set of labels is minimal and can be returned. // Otherwise, the current solution has to be ruled out and the next smallest solution is retrieved from // the solver. + + boost::container::flat_set commandSet(relevancyInformation.knownLabels); - // Set up some variables for the iterations. - boost::container::flat_set commandSet(relevancyInformation.relevantLabels); + // If there are no relevant labels, return directly. if (relevancyInformation.relevantLabels.empty()) { return commandSet; + } else if (relevancyInformation.minimalityLabels.empty()) { + commandSet.insert(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end()); + return commandSet; } + + // Set up some variables for the iterations. bool done = false; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; @@ -1724,24 +1758,16 @@ namespace storm { totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock; STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << "."); - // Restrict the given MDP to the current set of labels and compute the reachability probability. + // Restrict the given model to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); - auto subMdpChoiceOrigins = restrictMdpToLabelSet(mdp, commandSet); - storm::models::sparse::Mdp const& subMdp = subMdpChoiceOrigins.first; - std::vector> const& subLabelSets = subMdpChoiceOrigins.second; + auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet); + std::shared_ptr> const& subModel = subChoiceOrigins.first; + std::vector> const& subLabelSets = subChoiceOrigins.second; - storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; - STORM_LOG_DEBUG("Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); - STORM_LOG_DEBUG("Computed model checking results."); + // Now determine the maximal reachability probability in the sub-model. + maximalReachabilityProbability = computeMaximalReachabilityProbability(env, *subModel, phiStates, psiStates); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; - - // Now determine the maximal reachability probability by checking all initial states. - maximalReachabilityProbability = 0; - for (auto state : mdp.getInitialStates()) { - maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); - } // Depending on whether the threshold was successfully achieved or not, we proceed by either analyzing the bad solution or stopping the iteration process. analysisClock = std::chrono::high_resolution_clock::now(); @@ -1750,11 +1776,11 @@ namespace storm { ++zeroProbabilityCount; // If there was no target state reachable, analyze the solution and guide the solver into the right direction. - analyzeZeroProbabilitySolution(*solver, subMdp, subLabelSets, mdp, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeZeroProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } else { // If the reachability probability was greater than zero (i.e. there is a reachable target state), but the probability was insufficient to exceed // the given threshold, we analyze the solution and try to guide the solver into the right direction. - analyzeInsufficientProbabilitySolution(*solver, subMdp, subLabelSets, mdp, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeInsufficientProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } } else { done = true; @@ -1791,14 +1817,14 @@ namespace storm { #endif } - static void extendCommandSetLowerBound(storm::models::sparse::Mdp const& mdp, boost::container::flat_set& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static void extendCommandSetLowerBound(storm::models::sparse::Model const& model, boost::container::flat_set& commandSet, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { auto startTime = std::chrono::high_resolution_clock::now(); - // Create sub-MDP that only contains the choices allowed by the given command set. - storm::models::sparse::Mdp subMdp = restrictMdpToLabelSet(mdp, commandSet).first; + // Create sub-model that only contains the choices allowed by the given command set. + storm::models::sparse::Model subModel = restrictModelToLabelSet(model, commandSet).first; - // Then determine all prob0E(psi) states that are reachable in the sub-MDP. - storm::storage::BitVector reachableProb0EStates = storm::utility::graph::getReachableStates(subMdp.getTransitionMatrix(), subMdp.getInitialStates(), phiStates, psiStates); + // Then determine all prob0E(psi) states that are reachable in the sub-model. + storm::storage::BitVector reachableProb0EStates = storm::utility::graph::getReachableStates(subModel.getTransitionMatrix(), subModel.getInitialStates(), phiStates, psiStates); // Create a queue of reachable prob0E(psi) states so we can check which commands need to be added // to give them a strategy that avoids psi states. @@ -1816,12 +1842,12 @@ namespace storm { // Now iterate over the original choices of the prob0E(psi) state and add at least one. bool hasLabeledChoice = false; uint64_t smallestCommandSetSize = 0; - uint64_t smallestCommandChoice = mdp.getTransitionMatrix().getRowGroupIndices()[state]; + uint64_t smallestCommandChoice = model.getTransitionMatrix().getRowGroupIndices()[state]; // Determine the choice with the least amount of commands (bad heuristic). - for (uint64_t choice = smallestCommandChoice; choice < mdp.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { + for (uint64_t choice = smallestCommandChoice; choice < model.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { bool onlyProb0ESuccessors = true; - for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(choice)) { + for (auto const& successorEntry : model.getTransitionMatrix().getRow(choice)) { if (!psiStates.get(successorEntry.getColumn())) { onlyProb0ESuccessors = false; break; @@ -1829,7 +1855,7 @@ namespace storm { } if (onlyProb0ESuccessors) { - auto const& labelSet = mdp.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(choice); + auto const& labelSet = model.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(choice); hasLabeledChoice |= !labelSet.empty(); if (smallestCommandChoice == 0 || labelSet.size() < smallestCommandSetSize) { @@ -1841,11 +1867,11 @@ namespace storm { if (hasLabeledChoice) { // Take all labels of the selected choice. - auto const& labelSet = mdp.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(smallestCommandChoice); + auto const& labelSet = model.getChoiceOrigins()->asPrismChoiceOrigins().getCommandSet(smallestCommandChoice); commandSet.insert(labelSet.begin(), labelSet.end()); // Check for which successor states choices need to be added - for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(smallestCommandChoice)) { + for (auto const& successorEntry : model.getTransitionMatrix().getRow(smallestCommandChoice)) { if (!storm::utility::isZero(successorEntry.getValue())) { if (!reachableProb0EStates.get(successorEntry.getColumn())) { reachableProb0EStates.set(successorEntry.getColumn()); @@ -1860,7 +1886,7 @@ namespace storm { std::cout << std::endl << "Extended command for lower bounded property to size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; } - static boost::container::flat_set computeCounterexampleCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { + static boost::container::flat_set computeCounterexampleCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); @@ -1874,7 +1900,7 @@ namespace storm { storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(mdp); + storm::modelchecker::SparsePropositionalModelChecker> modelchecker(model); if (probabilityOperator.getSubformula().isUntilFormula()) { STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for eventually formulas."); @@ -1895,7 +1921,7 @@ namespace storm { storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); - phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true); + phiStates = storm::storage::BitVector(model.getNumberOfStates(), true); psiStates = subQualitativeResult.getTruthValuesVector(); } @@ -1907,7 +1933,7 @@ namespace storm { // reaching psi states completely. // This means that from all states in prob0E(psi) we need to include labels such that \sigma_0 - // is actually included in the resulting MDP. This prevents us from guaranteeing the minimality of + // is actually included in the resulting model. This prevents us from guaranteeing the minimality of // the returned counterexample, so we warn about that. STORM_LOG_WARN("Generating counterexample for lower-bounded property. The resulting command set need not be minimal."); @@ -1916,7 +1942,7 @@ namespace storm { threshold = storm::utility::one() - threshold; // Modify the phi and psi states appropriately. - storm::storage::BitVector statesWithProbability0E = storm::utility::graph::performProb0E(mdp.getTransitionMatrix(), mdp.getTransitionMatrix().getRowGroupIndices(), mdp.getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector statesWithProbability0E = storm::utility::graph::performProb0E(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates); phiStates = ~psiStates; psiStates = std::move(statesWithProbability0E); @@ -1927,20 +1953,20 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto commandSet = getMinimalCommandSet(env, program, mdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); + auto commandSet = getMinimalCommandSet(env, program, model, phiStates, psiStates, threshold, strictBound, boost::container::flat_set(), true, storm::settings::getModule().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; // Extend the command set properly. if (lowerBoundedFormula) { - extendCommandSetLowerBound(mdp, commandSet, phiStates, psiStates); + extendCommandSetLowerBound(model, commandSet, phiStates, psiStates); } return commandSet; } - static std::shared_ptr computeCounterexample(Environment const& env, storm::prism::Program program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { + static std::shared_ptr computeCounterexample(Environment const& env, storm::prism::Program program, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 - auto commandSet = computeCounterexampleCommandSet(env, program, mdp, formula); + auto commandSet = computeCounterexampleCommandSet(env, program, model, formula); return std::make_shared(program.restrictCommands(commandSet)); @@ -1955,4 +1981,3 @@ namespace storm { } // namespace counterexamples } // namespace storm -#endif /* STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ */ diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index 9eace3911..e816adac6 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -71,7 +71,14 @@ namespace storm { * @return The number of (non-zero) transitions of the model. */ virtual uint_fast64_t getNumberOfTransitions() const = 0; - + + /*! + * Returns the number of choices ine the model. + * + * @return The number of choices in of the model. + */ + virtual uint_fast64_t getNumberOfChoices() const = 0; + /*! * Prints information about the model to the specified stream. * diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index b86f11c7a..edeefb825 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -98,7 +98,12 @@ namespace storm { uint_fast64_t Model::getNumberOfTransitions() const { return this->getTransitionMatrix().getNonzeroEntryCount(); } - + + template + uint_fast64_t Model::getNumberOfChoices() const { + return this->getTransitionMatrix().getRowCount(); + } + template storm::storage::BitVector const& Model::getInitialStates() const { return this->getStates("init"); diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index b796a30f9..aa61eb3bd 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -76,7 +76,14 @@ namespace storm { * @return The number of (non-zero) transitions of the model. */ virtual uint_fast64_t getNumberOfTransitions() const override; - + + /*! + * Returns the number of choices ine the model. + * + * @return The number of choices in of the model. + */ + virtual uint_fast64_t getNumberOfChoices() const override; + /*! * Retrieves the initial states of the model. * diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index cd67e384f..263f67c16 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -26,11 +26,6 @@ namespace storm { // Intentionally left empty } - template - uint_fast64_t NondeterministicModel::getNumberOfChoices() const { - return this->getTransitionMatrix().getRowCount(); - } - template std::vector const& NondeterministicModel::getNondeterministicChoiceIndices() const { return this->getTransitionMatrix().getRowGroupIndices(); diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index dd1335718..2274e137a 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -31,13 +31,6 @@ namespace storm { */ NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents const& components); NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents&& components); - - /*! - * Retrieves the number of (nondeterministic) choices in the model. - * - * @return The number of (nondeterministic) choices in the model. - */ - uint_fast64_t getNumberOfChoices() const; /*! * Retrieves the vector indicating which matrix rows represent non-deterministic choices of a certain state. diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index f468cc377..5364a4d4f 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -64,6 +64,11 @@ namespace storm { uint_fast64_t Model::getNumberOfTransitions() const { return transitionMatrix.getNonZeroCount(); } + + template + uint_fast64_t Model::getNumberOfChoices() const { + return reachableStates.getNonZeroCount(); + } template storm::dd::DdManager& Model::getManager() const { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index fd0839a2b..2f39d3970 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -119,6 +119,8 @@ namespace storm { virtual uint_fast64_t getNumberOfTransitions() const override; + virtual uint_fast64_t getNumberOfChoices() const override; + /*! * Retrieves the manager responsible for the DDs that represent this model. * diff --git a/src/storm/models/symbolic/NondeterministicModel.h b/src/storm/models/symbolic/NondeterministicModel.h index c75874644..7fb42cf7b 100644 --- a/src/storm/models/symbolic/NondeterministicModel.h +++ b/src/storm/models/symbolic/NondeterministicModel.h @@ -90,7 +90,7 @@ namespace storm { * * @return The number of nondeterministic choices in the model. */ - uint_fast64_t getNumberOfChoices() const; + virtual uint_fast64_t getNumberOfChoices() const override; /*! * Retrieves the meta variables used to encode the nondeterminism in the model.