From ecf3c7e996c8267bd20b539d04c2e3cb608640cd Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 14 Jun 2017 09:29:16 +0200 Subject: [PATCH] reverted renaming of LabelSetGenerators to CommandSetGenerators. Potentially, these generators work for arbitrary sets of labels, not just for sets of Prism commands. --- src/storm/api/counterexamples.cpp | 4 +- src/storm/api/counterexamples.h | 4 +- src/storm/cli/cli.cpp | 2 +- ...rator.h => MILPMinimalLabelSetGenerator.h} | 141 ++-- ...erator.h => SMTMinimalLabelSetGenerator.h} | 610 +++++++++--------- src/storm/utility/counterexamples.h | 38 +- 6 files changed, 405 insertions(+), 394 deletions(-) rename src/storm/counterexamples/{MILPMinimalCommandSetGenerator.h => MILPMinimalLabelSetGenerator.h} (89%) rename src/storm/counterexamples/{SMTMinimalCommandSetGenerator.h => SMTMinimalLabelSetGenerator.h} (78%) diff --git a/src/storm/api/counterexamples.cpp b/src/storm/api/counterexamples.cpp index 52eb4335e..f60809f05 100644 --- a/src/storm/api/counterexamples.cpp +++ b/src/storm/api/counterexamples.cpp @@ -4,11 +4,11 @@ namespace storm { namespace api { std::shared_ptr computePrismHighLevelCounterexampleMilp(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula) { - return storm::counterexamples::MILPMinimalCommandSetGenerator::computeCounterexample(program, *mdp, formula); + return storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); } std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula) { - return storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, *mdp, formula); + return storm::counterexamples::SMTMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); } } diff --git a/src/storm/api/counterexamples.h b/src/storm/api/counterexamples.h index 8dfed91e8..d8f3d1ddd 100644 --- a/src/storm/api/counterexamples.h +++ b/src/storm/api/counterexamples.h @@ -1,7 +1,7 @@ #pragma once -#include "storm/counterexamples/MILPMinimalCommandSetGenerator.h" -#include "storm/counterexamples/SMTMinimalCommandSetGenerator.h" +#include "storm/counterexamples/MILPMinimalLabelSetGenerator.h" +#include "storm/counterexamples/SMTMinimalLabelSetGenerator.h" namespace storm { namespace api { diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 5ca091db5..6256a7574 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -497,7 +497,7 @@ namespace storm { void printCounterexample(std::shared_ptr const& counterexample, storm::utility::Stopwatch* watch = nullptr) { if (counterexample) { - STORM_PRINT_AND_LOG(counterexample << std::endl); + STORM_PRINT_AND_LOG(*counterexample << std::endl); if (watch) { STORM_PRINT_AND_LOG("Time for computation: " << *watch << "." << std::endl); } diff --git a/src/storm/counterexamples/MILPMinimalCommandSetGenerator.h b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h similarity index 89% rename from src/storm/counterexamples/MILPMinimalCommandSetGenerator.h rename to src/storm/counterexamples/MILPMinimalLabelSetGenerator.h index e27466542..c028f0e5a 100644 --- a/src/storm/counterexamples/MILPMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h @@ -2,6 +2,7 @@ #define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ #include +#include #include "storm/models/sparse/Mdp.h" #include "storm/logic/Formulas.h" @@ -33,10 +34,10 @@ namespace storm { /*! * This class provides functionality to generate a minimal counterexample to a probabilistic reachability - * property in terms of used commands. + * property in terms of used labels. */ template - class MILPMinimalCommandSetGenerator { + class MILPMinimalLabelSetGenerator { private: /*! * A helper class that provides the functionality to compute a hash value for pairs of state indices. @@ -60,21 +61,21 @@ namespace storm { }; /*! - * A helper struct capturing information about relevant and problematic choices of states and which commands + * A helper struct capturing information about relevant and problematic choices of states and which labels * are relevant. */ struct ChoiceInformation { std::unordered_map> relevantChoicesForRelevantStates; std::unordered_map> problematicChoicesForProblematicStates; - boost::container::flat_set allRelevantCommands; - boost::container::flat_set knownCommands; + boost::container::flat_set allRelevantLabels; + boost::container::flat_set knownLabels; }; /*! * A helper struct capturing information about the variables of the MILP formulation. */ struct VariableInformation { - std::unordered_map commandToVariableMap; + std::unordered_map labelToVariableMap; std::unordered_map> stateToChoiceVariablesMap; std::unordered_map initialStateToChoiceVariableMap; std::unordered_map stateToProbabilityVariableMap; @@ -117,17 +118,16 @@ namespace storm { * @param stateInformation The relevant and problematic states of the model. * @param psiStates A bit vector characterizing the psi states in the model. * @return A structure that stores the relevant and problematic choices in the model as well as the set - * of relevant commands. + * of relevant labels. */ - static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { + static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { // Create result and shortcuts to needed data for convenience. ChoiceInformation result; storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // Now traverse all choices of all relevant states and check whether there is a relevant target state. - // If so, the associated commands 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 relevant state has at least one // relevant successor, the choice is considered to be relevant. for (auto state : stateInformation.relevantStates) { result.relevantChoicesForRelevantStates.emplace(state, std::list()); @@ -138,10 +138,10 @@ namespace storm { bool currentChoiceRelevant = false; bool allSuccessorsProblematic = true; for (auto const& successorEntry : transitionMatrix.getRow(row)) { - // If there is a relevant successor, we need to add the commands of the current choice. + // If there is a relevant successor, we need to add the labels of the current choice. if (stateInformation.relevantStates.get(successorEntry.getColumn()) || psiStates.get(successorEntry.getColumn())) { - for (auto const& command : choiceOrigins.getCommandSet(row)) { - result.allRelevantCommands.insert(command); + for (auto const& label : labelSets[row]) { + result.allRelevantLabels.insert(label); } if (!currentChoiceRelevant) { currentChoiceRelevant = true; @@ -161,30 +161,30 @@ namespace storm { } } - // Finally, determine the set of commands that are known to be taken. - result.knownCommands = storm::utility::counterexamples::getGuaranteedCommandSet(mdp, psiStates, result.allRelevantCommands); - STORM_LOG_DEBUG("Found " << result.allRelevantCommands.size() << " relevant commands and " << result.knownCommands.size() << " known commands."); + // Finally, determine the set of labels that are known to be taken. + result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(mdp, labelSets, psiStates, result.allRelevantLabels); + STORM_LOG_DEBUG("Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels."); return result; } /*! - * Creates the variables for the commands of the model. + * Creates the variables for the labels of the model. * * @param solver The MILP solver. - * @param relevantCommands The set of relevant commands of the model. - * @return A mapping from commands to variable indices. + * @param relevantLabels The set of relevant labels of the model. + * @return A mapping from labels to variable indices. */ - static std::pair, uint_fast64_t> createCommandVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantCommands) { + static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { std::stringstream variableNameBuffer; std::unordered_map resultingMap; - for (auto const& command : relevantCommands) { + for (auto const& label : relevantLabels) { variableNameBuffer.str(""); variableNameBuffer.clear(); - variableNameBuffer << "command" << command; - resultingMap[command] = solver.addBinaryVariable(variableNameBuffer.str(), 1); + variableNameBuffer << "label" << label; + resultingMap[label] = solver.addBinaryVariable(variableNameBuffer.str(), 1); } - return std::make_pair(resultingMap, relevantCommands.size()); + return std::make_pair(resultingMap, relevantLabels.size()); } /*! @@ -363,11 +363,11 @@ namespace storm { // Create a struct that stores all information about variables. VariableInformation result; - // Create variables for involved commands. - std::pair, uint_fast64_t> commandVariableResult = createCommandVariables(solver, choiceInformation.allRelevantCommands); - result.commandToVariableMap = std::move(commandVariableResult.first); - result.numberOfVariables += commandVariableResult.second; - STORM_LOG_DEBUG("Created variables for commands."); + // Create variables for involved labels. + std::pair, uint_fast64_t> labelVariableResult = createLabelVariables(solver, choiceInformation.allRelevantLabels); + result.labelToVariableMap = std::move(labelVariableResult.first); + result.numberOfVariables += labelVariableResult.second; + STORM_LOG_DEBUG("Created variables for labels."); // Create scheduler variables for relevant states and their actions. std::pair>, uint_fast64_t> schedulerVariableResult = createSchedulerVariables(solver, stateInformation, choiceInformation); @@ -474,8 +474,8 @@ namespace storm { } /*! - * Asserts constraints that make sure the commands are included in the solution set if the policy selects a - * choice that originates from the command in question. + * Asserts constraints that make sure the labels are included in the solution set if the policy selects a + * choice that originates from the label in question. * * @param solver The MILP solver. * @param mdp The MDP. @@ -484,17 +484,16 @@ namespace storm { * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertChoicesImplyCommands(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); + static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin(); for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { - for (auto command : choiceOrigins.getCommandSet(choice)) { - storm::expressions::Expression constraint = variableInformation.commandToVariableMap.at(command) - *choiceVariableIterator >= solver.getConstant(0); - solver.addConstraint("ChoicesImplyCommands" + std::to_string(numberOfConstraintsCreated), constraint); + for (auto label : labelSets[choice]) { + storm::expressions::Expression constraint = variableInformation.labelToVariableMap.at(label) - *choiceVariableIterator >= solver.getConstant(0); + solver.addConstraint("ChoicesImplyLabels" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } ++choiceVariableIterator; @@ -623,19 +622,19 @@ namespace storm { } /* - * Asserts that commands that are on all paths from initial to target states are definitely taken. + * Asserts that labels that are on all paths from initial to target states are definitely taken. * * @param solver The MILP solver. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertKnownCommands(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; - for (auto command : choiceInformation.knownCommands) { - storm::expressions::Expression constraint = variableInformation.commandToVariableMap.at(command) == solver.getConstant(1); - solver.addConstraint("KnownCommands" + std::to_string(numberOfConstraintsCreated), constraint); + for (auto label : choiceInformation.knownLabels) { + storm::expressions::Expression constraint = variableInformation.labelToVariableMap.at(label) == solver.getConstant(1); + solver.addConstraint("KnownLabels" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } @@ -813,7 +812,7 @@ namespace storm { * @param includeSchedulerCuts If set to true, additional constraints are asserted that reduce the set of * possible choices. */ - static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { + static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { // Assert that the reachability probability in the subsystem exceeds the given threshold. uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, variableInformation, probabilityThreshold, strictBound); STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold."); @@ -822,9 +821,9 @@ namespace storm { numberOfConstraints += assertValidPolicy(solver, stateInformation, variableInformation); STORM_LOG_DEBUG("Asserted that policy is valid."); - // Add constraints that assert the commands that belong to some taken choices are taken as well. - numberOfConstraints += assertChoicesImplyCommands(solver, mdp, stateInformation, choiceInformation, variableInformation); - STORM_LOG_DEBUG("Asserted that commands implied by choices are taken."); + // Add constraints that assert the labels that belong to some taken choices are taken as well. + numberOfConstraints += assertChoicesImplyLabels(solver, mdp, labelSets, stateInformation, choiceInformation, variableInformation); + STORM_LOG_DEBUG("Asserted that labels implied by choices are taken."); // Add constraints that encode that the reachability probability from states which do not pick any action // is zero. @@ -839,9 +838,9 @@ namespace storm { numberOfConstraints += assertUnproblematicStateReachable(solver, mdp, stateInformation, choiceInformation, variableInformation); STORM_LOG_DEBUG("Asserted that unproblematic state reachable from problematic states."); - // Add constraints that express that certain commands are already known to be taken. - numberOfConstraints += assertKnownCommands(solver, choiceInformation, variableInformation); - STORM_LOG_DEBUG("Asserted known commands are taken."); + // Add constraints that express that certain labels are already known to be taken. + numberOfConstraints += assertKnownLabels(solver, choiceInformation, variableInformation); + STORM_LOG_DEBUG("Asserted known labels are taken."); // If required, assert additional constraints that reduce the number of possible policies. if (includeSchedulerCuts) { @@ -861,14 +860,14 @@ namespace storm { * @param solver The MILP solver. * @param variableInformation A struct with information about the variables of the model. */ - static boost::container::flat_set getUsedCommandsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { + static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { boost::container::flat_set result; - for (auto const& commandVariablePair : variableInformation.commandToVariableMap) { - bool commandTaken = solver.getBinaryValue(commandVariablePair.second); + for (auto const& labelVariablePair : variableInformation.labelToVariableMap) { + bool labelTaken = solver.getBinaryValue(labelVariablePair.second); - if (commandTaken) { - result.insert(commandVariablePair.first); + if (labelTaken) { + result.insert(labelVariablePair.first); } } return result; @@ -923,10 +922,9 @@ namespace storm { } public: - static boost::container::flat_set getMinimalCommandSet(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { - // (0) Check whether there are choice origins available - STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without choice origns."); - STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + static boost::container::flat_set getMinimalLabelSet(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { + // (0) Check whether the label sets are valid + STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; @@ -943,27 +941,27 @@ namespace storm { // (2) Identify relevant and problematic states. StateInformation stateInformation = determineRelevantAndProblematicStates(mdp, phiStates, psiStates); - // (3) Determine sets of relevant commands and problematic choices. - ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(mdp, stateInformation, psiStates); + // (3) Determine sets of relevant labels and problematic choices. + ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(mdp, labelSets, stateInformation, psiStates); // (4) Encode resulting system as MILP problem. - std::shared_ptr solver = storm::utility::solver::getLpSolver("MinimalCommandSetCounterexample"); + std::shared_ptr solver = storm::utility::solver::getLpSolver("MinimalLabelSetCounterexample"); // (4.1) Create variables. VariableInformation variableInformation = createVariables(*solver, mdp, stateInformation, choiceInformation); // (4.2) Construct constraint system. - buildConstraintSystem(*solver, mdp, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); + buildConstraintSystem(*solver, mdp, labelSets, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); // (4.3) Optimize the model. solver->optimize(); // (4.4) Read off result from variables. - boost::container::flat_set usedCommandSet = getUsedCommandsInSolution(*solver, variableInformation); - usedCommandSet.insert(choiceInformation.knownCommands.begin(), choiceInformation.knownCommands.end()); + boost::container::flat_set usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation); + usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end()); // (5) Return result. - return usedCommandSet; + return usedLabelSet; } /*! @@ -976,6 +974,10 @@ namespace storm { static std::shared_ptr computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; + // Check whether there are choice origins available + STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to minimal command set is impossible for model without choice origns."); + STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + 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."); storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); @@ -1012,9 +1014,18 @@ namespace storm { psiStates = subQualitativeResult.getTruthValuesVector(); } + // 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::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); + std::vector> labelSets; + labelSets.reserve(mdp.getNumberOfChoices()); + for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) { + labelSets.push_back(choiceOrigins.getCommandSet(choice)); + } + // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedCommandSet = getMinimalCommandSet(mdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); + boost::container::flat_set usedCommandSet = getMinimalLabelSet(mdp, labelSets, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal command set of size " << usedCommandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h similarity index 78% rename from src/storm/counterexamples/SMTMinimalCommandSetGenerator.h rename to src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 3361267e9..e2373b567 100644 --- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1,5 +1,5 @@ -#ifndef STORM_COUNTEREXAMPLES_SMTMINIMALCOMMANDSETGENERATOR_MDP_H_ -#define STORM_COUNTEREXAMPLES_SMTMINIMALCOMMANDSETGENERATOR_MDP_H_ +#ifndef STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ +#define STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ #include #include @@ -25,21 +25,21 @@ namespace storm { /*! * This class provides functionality to generate a minimal counterexample to a probabilistic reachability - * property in terms of used commands. + * property in terms of used labels. */ template - class SMTMinimalCommandSetGenerator { + class SMTMinimalLabelSetGenerator { #ifdef STORM_HAVE_Z3 private: struct RelevancyInformation { // The set of relevant states in the model. storm::storage::BitVector relevantStates; - // The set of relevant commands. - boost::container::flat_set relevantCommands; + // The set of relevant labels. + boost::container::flat_set relevantLabels; - // A set of commands that is definitely known to be taken in the final solution. - boost::container::flat_set knownCommands; + // A set of labels that is definitely known to be taken in the final solution. + boost::container::flat_set knownLabels; // A list of relevant choices for each relevant state. std::map> relevantChoicesForRelevantStates; @@ -49,11 +49,11 @@ namespace storm { // The manager responsible for the constraints we are building. std::shared_ptr manager; - // The variables associated with the relevant commands. - std::vector commandVariables; + // The variables associated with the relevant labels. + std::vector labelVariables; - // A mapping from relevant commands to their indices in the variable vector. - std::map commandToIndexMap; + // A mapping from relevant labels to their indices in the variable vector. + std::map labelToIndexMap; // A set of original auxiliary variables needed for the Fu-Malik procedure. std::vector originalAuxiliaryVariables; @@ -84,16 +84,15 @@ namespace storm { }; /*! - * Computes the set of relevant commands in the model. Relevant commands are choice origins such that there exists + * 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 commands. + * @param mdp The MDP 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. - * @return A structure containing the relevant commands as well as states. + * @return A structure containing the relevant labels as well as states. */ - static RelevancyInformation determineRelevantStatesAndCommands(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - + static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Create result. RelevancyInformation relevancyInformation; @@ -109,10 +108,9 @@ namespace storm { // Retrieve some references for convenient access. storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // Now traverse all choices of all relevant states and check whether there is a successor target state. - // If so, the associated commands 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 relevant state has at least one // relevant successor, the choice becomes relevant. for (auto state : relevancyInformation.relevantStates) { relevancyInformation.relevantChoicesForRelevantStates.emplace(state, std::list()); @@ -121,10 +119,10 @@ namespace storm { bool currentChoiceRelevant = false; for (auto const& entry : transitionMatrix.getRow(row)) { - // If there is a relevant successor, we need to add the commands of the current choice. + // If there is a relevant successor, we need to add the labels of the current choice. if (relevancyInformation.relevantStates.get(entry.getColumn()) || psiStates.get(entry.getColumn())) { - for (auto const& command : choiceOrigins.getCommandSet(row)) { - relevancyInformation.relevantCommands.insert(command); + for (auto const& label : labelSets[row]) { + relevancyInformation.relevantLabels.insert(label); } if (!currentChoiceRelevant) { currentChoiceRelevant = true; @@ -135,17 +133,17 @@ namespace storm { } } - // Compute the set of commands that are known to be taken in any case. - relevancyInformation.knownCommands = storm::utility::counterexamples::getGuaranteedCommandSet(mdp, psiStates, relevancyInformation.relevantCommands); - if (!relevancyInformation.knownCommands.empty()) { - boost::container::flat_set remainingCommands; - std::set_difference(relevancyInformation.relevantCommands.begin(), relevancyInformation.relevantCommands.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(remainingCommands, remainingCommands.end())); - relevancyInformation.relevantCommands = remainingCommands; + // 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); + 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.relevantCommands.size() << " relevant and " << relevancyInformation.knownCommands.size() << " known commands." << std::endl; + std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels." << std::endl; - STORM_LOG_DEBUG("Found " << relevancyInformation.relevantCommands.size() << " relevant and " << relevancyInformation.knownCommands.size() << " known commands."); + STORM_LOG_DEBUG("Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels."); return relevancyInformation; } @@ -153,8 +151,8 @@ namespace storm { * Creates all necessary variables. * * @param manager The manager in which to create the variables. - * @param relevantCommands A set of relevant commands for which to create the expressions. - * @return A mapping from relevant commands to their corresponding expressions. + * @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) { VariableInformation variableInformation; @@ -163,21 +161,21 @@ namespace storm { // Create stringstream to build expression names. std::stringstream variableName; - // Create the variables for the relevant commands. - for (auto command : relevancyInformation.relevantCommands) { - variableInformation.commandToIndexMap[command] = variableInformation.commandVariables.size(); + // Create the variables for the relevant labels. + for (auto label : relevancyInformation.relevantLabels) { + variableInformation.labelToIndexMap[label] = variableInformation.labelVariables.size(); // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); - variableName << "c" << command; + variableName << "c" << label; - variableInformation.commandVariables.push_back(manager->declareBooleanVariable(variableName.str())); + variableInformation.labelVariables.push_back(manager->declareBooleanVariable(variableName.str())); // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); - variableName << "h" << command; + variableName << "h" << label; variableInformation.originalAuxiliaryVariables.push_back(manager->declareBooleanVariable(variableName.str())); } @@ -253,13 +251,13 @@ namespace storm { * @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 commands. + * @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) { - // Assert that at least one of the commands must be taken. - z3::expr formula = variableInformation.commandVariables.at(0); - for (uint_fast64_t index = 1; index < variableInformation.commandVariables.size(); ++index) { - formula = formula || variableInformation.commandVariables.at(index); + // 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) { + formula = formula || variableInformation.labelVariables.at(index); } solver.add(formula); } @@ -268,69 +266,67 @@ 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 MDP for which to compute the cuts. + * @param mdp The labeled MDP 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, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + 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 - // * identify commands enabled in initial states - // * identify commands that can directly precede a given action - // * identify commands that directly reach a target state - // * identify commands that can directly follow a given action + // * identify labels enabled in initial states + // * identify labels that can directly precede a given action + // * identify labels that directly reach a target state + // * identify labels that can directly follow a given action - boost::container::flat_set initialCommands; + boost::container::flat_set initialLabels; std::set> initialCombinations; - std::map> precedingCommands; - boost::container::flat_set targetCommands; + std::map> precedingLabels; + boost::container::flat_set targetLabels; boost::container::flat_set> targetCombinations; - std::map, std::set>> followingCommands; - std::map>> synchronizingCommands; + 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(); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { - boost::container::flat_set const& commandsOfCurrentChoice = choiceOrigins.getCommandSet(currentChoice); // If the choice is a synchronization choice, we need to record it. - if (commandsOfCurrentChoice.size() > 1) { - for (auto command : commandsOfCurrentChoice) { - synchronizingCommands[command].emplace(commandsOfCurrentChoice); + if (labelSets[currentChoice].size() > 1) { + for (auto label : labelSets[currentChoice]) { + synchronizingLabels[label].emplace(labelSets[currentChoice]); } } - // If the state is initial, we need to add all the choice commands to the initial command set. + // If the state is initial, we need to add all the choice labels to the initial label set. if (initialStates.get(currentState)) { - initialCommands.insert(commandsOfCurrentChoice.begin(), commandsOfCurrentChoice.end()); - initialCombinations.insert(commandsOfCurrentChoice); + initialLabels.insert(labelSets[currentChoice].begin(), labelSets[currentChoice].end()); + initialCombinations.insert(labelSets[currentChoice]); } - // Iterate over successors and add relevant choices of relevant successors to the following command set. + // Iterate over successors and add relevant choices of relevant successors to the following label set. bool canReachTargetState = false; for (auto const& entry : transitionMatrix.getRow(currentChoice)) { if (relevancyInformation.relevantStates.get(entry.getColumn())) { for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.getColumn())) { - followingCommands[commandsOfCurrentChoice].insert(choiceOrigins.getCommandSet(relevantChoice)); + followingLabels[labelSets[currentChoice]].insert(labelSets[relevantChoice]); } } else if (psiStates.get(entry.getColumn())) { canReachTargetState = true; } } - // If the choice can reach a target state directly, we add all the commands to the target command set. + // If the choice can reach a target state directly, we add all the labels to the target label set. if (canReachTargetState) { - targetCommands.insert(commandsOfCurrentChoice.begin(), commandsOfCurrentChoice.end()); - targetCombinations.insert(commandsOfCurrentChoice); + targetLabels.insert(labelSets[currentChoice].begin(), labelSets[currentChoice].end()); + targetCombinations.insert(labelSets[currentChoice]); } } // Iterate over predecessors and add all choices that target the current state to the preceding - // command set of all commands of all relevant choices of the current state. + // label set of all labels of all relevant choices of the current state. for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { if (relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) { for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.getColumn())) { @@ -343,9 +339,9 @@ namespace storm { if (choiceTargetsCurrentState) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { - for (auto commandToAdd : choiceOrigins.getCommandSet(predecessorChoice)) { - for (auto commandForWhichToAdd : choiceOrigins.getCommandSet(currentChoice)) { - precedingCommands[commandForWhichToAdd].insert(commandToAdd); + for (auto labelToAdd : labelSets[predecessorChoice]) { + for (auto labelForWhichToAdd : labelSets[currentChoice]) { + precedingLabels[labelForWhichToAdd].insert(labelToAdd); } } } @@ -361,19 +357,19 @@ namespace storm { { std::vector formulae; - // Start by asserting that we take at least one initial command. We may do so only if there is no initial + // Start by asserting that we take at least one initial label. We may do so only if there is no initial // combination that is already known. Otherwise this condition would be too strong. bool initialCombinationKnown = false; for (auto const& combination : initialCombinations) { boost::container::flat_set tmpSet; - std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); if (tmpSet.size() == 0) { initialCombinationKnown = true; break; } else { storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto command : tmpSet) { - conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto label : tmpSet) { + conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } formulae.push_back(conj); } @@ -391,14 +387,14 @@ namespace storm { bool targetCombinationKnown = false; for (auto const& combination : targetCombinations) { boost::container::flat_set tmpSet; - std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); if (tmpSet.size() == 0) { targetCombinationKnown = true; break; } else { storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto command : tmpSet) { - conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto label : tmpSet) { + conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } formulae.push_back(conj); } @@ -408,94 +404,94 @@ namespace storm { } } - // Compute the sets of commands such that the transitions originating from this set possess at least one known successor. + // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor. boost::container::flat_set> hasKnownSuccessor; - for (auto const& commandSetFollowingSetsPair : followingCommands) { - for (auto const& set : commandSetFollowingSetsPair.second) { - if (std::includes(relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), set.begin(), set.end())) { + for (auto const& labelSetFollowingSetsPair : followingLabels) { + for (auto const& set : labelSetFollowingSetsPair.second) { + if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { hasKnownSuccessor.insert(set); break; } } } - STORM_LOG_DEBUG("Asserting taken commands are followed by another command if they are not a target command."); - // Now assert that for each non-target command, we take a following command. - for (auto const& commandSetFollowingSetsPair : followingCommands) { + STORM_LOG_DEBUG("Asserting taken labels are followed by another label if they are not a target label."); + // Now assert that for each non-target label, we take a following label. + for (auto const& labelSetFollowingSetsPair : followingLabels) { std::vector formulae; // Only build a constraint if the combination does not lead to a target state and // no successor set is already known. - if (targetCombinations.find(commandSetFollowingSetsPair.first) == targetCombinations.end() && hasKnownSuccessor.find(commandSetFollowingSetsPair.first) == hasKnownSuccessor.end()) { + if (targetCombinations.find(labelSetFollowingSetsPair.first) == targetCombinations.end() && hasKnownSuccessor.find(labelSetFollowingSetsPair.first) == hasKnownSuccessor.end()) { - // Compute the set of unknown commands on the left-hand side of the implication. - boost::container::flat_set unknownLhsCommands; - std::set_difference(commandSetFollowingSetsPair.first.begin(), commandSetFollowingSetsPair.first.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownLhsCommands, unknownLhsCommands.end())); - for (auto command : unknownLhsCommands) { - formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); + // Compute the set of unknown labels on the left-hand side of the implication. + boost::container::flat_set unknownLhsLabels; + std::set_difference(labelSetFollowingSetsPair.first.begin(), labelSetFollowingSetsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); + for (auto label : unknownLhsLabels) { + formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } - for (auto const& followingSet : commandSetFollowingSetsPair.second) { + for (auto const& followingSet : labelSetFollowingSetsPair.second) { boost::container::flat_set tmpSet; - // Check which commands of the current following set are not known. This set must be non-empty, because + // Check which labels of the current following set are not known. This set must be non-empty, because // otherwise a successor combination would already be known and control cannot reach this point. - std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); - // Construct an expression that enables all unknown commands of the current following set. + // Construct an expression that enables all unknown labels of the current following set. storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto command : tmpSet) { - conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto label : tmpSet) { + conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } formulae.push_back(conj); } - if (commandSetFollowingSetsPair.first.size() > 1) { - // Taking all commands of a combination does not necessarily mean that a following command set needs to be taken. + if (labelSetFollowingSetsPair.first.size() > 1) { + // Taking all commands of a combination does not necessarily mean that a following label set needs to be taken. // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need // to add an additional clause that says that the right-hand side of the implication is also true if all commands // of the current choice have enabled synchronization options. storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false); - for (auto command : commandSetFollowingSetsPair.first) { - storm::expressions::Expression alternativeExpressionForCommand = variableInformation.manager->boolean(false); - std::set> const& synchsForCommand = synchronizingCommands.at(command); + for (auto label : labelSetFollowingSetsPair.first) { + storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false); + std::set> const& synchsForCommand = synchronizingLabels.at(label); for (auto const& synchSet : synchsForCommand) { storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true); // If the current synchSet is the same as left-hand side of the implication, we need to skip it. - if (synchSet == commandSetFollowingSetsPair.first) continue; + if (synchSet == labelSetFollowingSetsPair.first) continue; - // Now that we have the commands that are unknown and "missing", we still need to check whether this other + // Now that we have the labels that are unknown and "missing", we still need to check whether this other // synchronizing set already has a known successor or leads directly to a target state. if (hasKnownSuccessor.find(synchSet) == hasKnownSuccessor.end() && targetCombinations.find(synchSet) == targetCombinations.end()) { // If not, we can assert that we take one of its possible successors. boost::container::flat_set unknownSynchs; - std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownSynchs, unknownSynchs.end())); - unknownSynchs.erase(command); + std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end())); + unknownSynchs.erase(label); - for (auto command : unknownSynchs) { - alternativeExpression = alternativeExpression && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto label : unknownSynchs) { + alternativeExpression = alternativeExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } storm::expressions::Expression disjunctionOverSuccessors = variableInformation.manager->boolean(false); - for (auto successorSet : followingCommands.at(synchSet)) { - storm::expressions::Expression conjunctionOverCommands = variableInformation.manager->boolean(true); - for (auto command : successorSet) { - if (relevancyInformation.knownCommands.find(command) == relevancyInformation.knownCommands.end()) { - conjunctionOverCommands = conjunctionOverCommands && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto successorSet : followingLabels.at(synchSet)) { + storm::expressions::Expression conjunctionOverLabels = variableInformation.manager->boolean(true); + for (auto label : successorSet) { + if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { + conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } } - disjunctionOverSuccessors = disjunctionOverSuccessors || conjunctionOverCommands; + disjunctionOverSuccessors = disjunctionOverSuccessors || conjunctionOverLabels; } alternativeExpression = alternativeExpression && disjunctionOverSuccessors; } - alternativeExpressionForCommand = alternativeExpressionForCommand || alternativeExpression; + alternativeExpressionForLabel = alternativeExpressionForLabel || alternativeExpression; } - finalDisjunct = finalDisjunct && alternativeExpressionForCommand; + finalDisjunct = finalDisjunct && alternativeExpressionForLabel; } formulae.push_back(finalDisjunct); @@ -508,24 +504,24 @@ namespace storm { } STORM_LOG_DEBUG("Asserting synchronization cuts."); - // Finally, assert that if we take one of the synchronizing commands, we also take one of the combinations - // the command appears in. - for (auto const& commandSynchronizingSetsPair : synchronizingCommands) { + // Finally, assert that if we take one of the synchronizing labels, we also take one of the combinations + // the label appears in. + for (auto const& labelSynchronizingSetsPair : synchronizingLabels) { std::vector formulae; - if (relevancyInformation.knownCommands.find(commandSynchronizingSetsPair.first) == relevancyInformation.knownCommands.end()) { - formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(commandSynchronizingSetsPair.first))); + if (relevancyInformation.knownLabels.find(labelSynchronizingSetsPair.first) == relevancyInformation.knownLabels.end()) { + formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first))); } - // We need to be careful, because there may be one synchronisation set out of which all commands are + // We need to be careful, because there may be one synchronisation set out of which all labels are // known, which means we must not assert anything. bool allImplicantsKnownForOneSet = false; - for (auto const& synchronizingSet : commandSynchronizingSetsPair.second) { + for (auto const& synchronizingSet : labelSynchronizingSetsPair.second) { storm::expressions::Expression currentCombination = variableInformation.manager->boolean(true); bool allImplicantsKnownForCurrentSet = true; - for (auto command : synchronizingSet) { - if (relevancyInformation.knownCommands.find(command) == relevancyInformation.knownCommands.end() && command != commandSynchronizingSetsPair.first) { - currentCombination = currentCombination && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto label : synchronizingSet) { + if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end() && label != labelSynchronizingSetsPair.first) { + currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } } formulae.push_back(currentCombination); @@ -550,32 +546,30 @@ 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, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { - // A container storing the command sets that may precede a given command set. - std::map, std::set>> precedingCommandSets; + 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) { + // A container storing the label sets that may precede a given label set. + std::map, std::set>> precedingLabelSets; - // A container that maps commands to their reachable synchronization sets. - std::map>> synchronizingCommands; + // 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(); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); - // Compute the set of commands that may precede a given action. + // Compute the set of labels that may precede a given action. for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { - boost::container::flat_set const& commandsOfCurrentChoice = choiceOrigins.getCommandSet(currentChoice); // If the choice is a synchronization choice, we need to record it. - if (commandsOfCurrentChoice.size() > 1) { - for (auto command : commandsOfCurrentChoice) { - synchronizingCommands[command].emplace(commandsOfCurrentChoice); + if (labelSets[currentChoice].size() > 1) { + for (auto label : labelSets[currentChoice]) { + synchronizingLabels[label].emplace(labelSets[currentChoice]); } } // Iterate over predecessors and add all choices that target the current state to the preceding - // command set of all commands of all relevant choices of the current state. + // label set of all labels of all relevant choices of the current state. for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { if (relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) { for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.getColumn())) { @@ -587,7 +581,7 @@ namespace storm { } if (choiceTargetsCurrentState) { - precedingCommandSets[commandsOfCurrentChoice].insert(choiceOrigins.getCommandSet(predecessorChoice)); + precedingLabelSets[labelSets.at(currentChoice)].insert(labelSets.at(predecessorChoice)); } } } @@ -610,7 +604,7 @@ namespace storm { // for (auto const& integerVariable : program.getGlobalIntegerVariables()) { // solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str())); // } -// +// // for (auto const& module : program.getModules()) { // for (auto const& booleanVariable : module.getBooleanVariables()) { // solverVariables.emplace(booleanVariable.getName(), localContext.bool_const(booleanVariable.getName().c_str())); @@ -619,7 +613,7 @@ namespace storm { // solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str())); // } // } -// +// // storm::adapters::Z3ExpressionAdapter expressionAdapter(localContext, false, solverVariables); // Then add the constraints for bounds of the integer variables.. @@ -637,13 +631,13 @@ namespace storm { // Construct an expression that exactly characterizes the initial state. storm::expressions::Expression initialStateExpression = program.getInitialStatesExpression(); - // Store the found implications in a container similar to the preceding command sets. + // Store the found implications in a container similar to the preceding label sets. std::map, std::set>> backwardImplications; // Now check for possible backward cuts. - for (auto const& commandSetAndPrecedingCommandSetsPair : precedingCommandSets) { + for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabelSets) { - // Find out the commands for the currently considered command set. + // Find out the commands for the currently considered label set. std::vector> currentCommandVector; for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { storm::prism::Module const& module = program.getModule(moduleIndex); @@ -652,7 +646,7 @@ namespace storm { storm::prism::Command const& command = module.getCommand(commandIndex); // If the current command is one of the commands we need to consider, store a reference to it in the container. - if (commandSetAndPrecedingCommandSetsPair.first.find(command.getGlobalIndex()) != commandSetAndPrecedingCommandSetsPair.first.end()) { + if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) { currentCommandVector.push_back(command); } } @@ -690,8 +684,8 @@ namespace storm { ++setIterator; } } else { - throw storm::exceptions::InvalidStateException() << "Choice command set is empty."; - STORM_LOG_DEBUG("Choice command set is empty."); + throw storm::exceptions::InvalidStateException() << "Choice label set is empty."; + STORM_LOG_DEBUG("Choice label set is empty."); } STORM_LOG_DEBUG("About to assert disjunction of negated guards."); @@ -707,12 +701,12 @@ namespace storm { localSolver->add(guardExpression); STORM_LOG_DEBUG("Asserted disjunction of negated guards."); - // Now check the possible preceding command sets for the essential ones. - for (auto const& precedingCommandSet : commandSetAndPrecedingCommandSetsPair.second) { + // Now check the possible preceding label sets for the essential ones. + for (auto const& precedingLabelSet : labelSetAndPrecedingLabelSetsPair.second) { // Create a restore point so we can easily pop-off all weakest precondition expressions. localSolver->push(); - // Find out the commands for the currently considered preceding command set. + // Find out the commands for the currently considered preceding label set. std::vector> currentPrecedingCommandVector; for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { storm::prism::Module const& module = program.getModule(moduleIndex); @@ -721,7 +715,7 @@ namespace storm { storm::prism::Command const& command = module.getCommand(commandIndex); // If the current command is one of the commands we need to consider, store a reference to it in the container. - if (precedingCommandSet.find(command.getGlobalIndex()) != precedingCommandSet.end()) { + if (precedingLabelSet.find(command.getGlobalIndex()) != precedingLabelSet.end()) { currentPrecedingCommandVector.push_back(command); } } @@ -777,7 +771,7 @@ namespace storm { STORM_LOG_DEBUG("Asserted disjunction of all weakest preconditions."); if (localSolver->check() == storm::solver::SmtSolver::CheckResult::Sat) { - backwardImplications[commandSetAndPrecedingCommandSetsPair.first].insert(precedingCommandSet); + backwardImplications[labelSetAndPrecedingLabelSetsPair.first].insert(precedingLabelSet); } localSolver->pop(); @@ -788,96 +782,96 @@ namespace storm { } } - // Compute the sets of commands such that the transitions originating from this set possess at least one known successor. + // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor. boost::container::flat_set> hasKnownPredecessor; - for (auto const& commandSetImplicationsPair : backwardImplications) { - for (auto const& set : commandSetImplicationsPair.second) { - if (std::includes(relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), set.begin(), set.end())) { + for (auto const& labelSetImplicationsPair : backwardImplications) { + for (auto const& set : labelSetImplicationsPair.second) { + if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { hasKnownPredecessor.insert(set); break; } } } - STORM_LOG_DEBUG("Asserting taken commands are preceded by another command if they are not an initial command."); - // Now assert that for each non-target command, we take a following command. - for (auto const& commandSetImplicationsPair : backwardImplications) { + STORM_LOG_DEBUG("Asserting taken labels are preceded by another label if they are not an initial label."); + // Now assert that for each non-target label, we take a following label. + for (auto const& labelSetImplicationsPair : backwardImplications) { std::vector formulae; // Only build a constraint if the combination no predecessor set is already known. - if (hasKnownPredecessor.find(commandSetImplicationsPair.first) == hasKnownPredecessor.end()) { + if (hasKnownPredecessor.find(labelSetImplicationsPair.first) == hasKnownPredecessor.end()) { - // Compute the set of unknown commands on the left-hand side of the implication. - boost::container::flat_set unknownLhsCommands; - std::set_difference(commandSetImplicationsPair.first.begin(), commandSetImplicationsPair.first.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownLhsCommands, unknownLhsCommands.end())); - for (auto command : unknownLhsCommands) { - formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); + // Compute the set of unknown labels on the left-hand side of the implication. + boost::container::flat_set unknownLhsLabels; + std::set_difference(labelSetImplicationsPair.first.begin(), labelSetImplicationsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); + for (auto label : unknownLhsLabels) { + formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } - for (auto const& precedingSet : commandSetImplicationsPair.second) { + for (auto const& precedingSet : labelSetImplicationsPair.second) { boost::container::flat_set tmpSet; - // Check which commands of the current following set are not known. This set must be non-empty, because + // Check which labels of the current following set are not known. This set must be non-empty, because // otherwise a predecessor combination would already be known and control cannot reach this point. - std::set_difference(precedingSet.begin(), precedingSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(precedingSet.begin(), precedingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); - // Construct an expression that enables all unknown commands of the current following set. + // Construct an expression that enables all unknown labels of the current following set. storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto command : tmpSet) { - conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto label : tmpSet) { + conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } formulae.push_back(conj); } - if (commandSetImplicationsPair.first.size() > 1) { - // Taking all commands of a combination does not necessarily mean that a predecessor command set needs to be taken. + if (labelSetImplicationsPair.first.size() > 1) { + // Taking all commands of a combination does not necessarily mean that a predecessor label set needs to be taken. // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need // to add an additional clause that says that the right-hand side of the implication is also true if all commands // of the current choice have enabled synchronization options. storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false); - for (auto command : commandSetImplicationsPair.first) { - storm::expressions::Expression alternativeExpressionForCommand = variableInformation.manager->boolean(false); - std::set> const& synchsForCommand = synchronizingCommands.at(command); + for (auto label : labelSetImplicationsPair.first) { + storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false); + std::set> const& synchsForCommand = synchronizingLabels.at(label); for (auto const& synchSet : synchsForCommand) { storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true); // If the current synchSet is the same as left-hand side of the implication, we need to skip it. - if (synchSet == commandSetImplicationsPair.first) continue; + if (synchSet == labelSetImplicationsPair.first) continue; - // Now that we have the commands that are unknown and "missing", we still need to check whether this other + // Now that we have the labels that are unknown and "missing", we still need to check whether this other // synchronizing set already has a known predecessor. if (hasKnownPredecessor.find(synchSet) == hasKnownPredecessor.end()) { // If not, we can assert that we take one of its possible predecessors. boost::container::flat_set unknownSynchs; - std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownSynchs, unknownSynchs.end())); - unknownSynchs.erase(command); + std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end())); + unknownSynchs.erase(label); - for (auto command : unknownSynchs) { - alternativeExpression = alternativeExpression && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + for (auto label : unknownSynchs) { + alternativeExpression = alternativeExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } storm::expressions::Expression disjunctionOverPredecessors = variableInformation.manager->boolean(false); - auto precedingCommandSetsIterator = precedingCommandSets.find(synchSet); - if (precedingCommandSetsIterator != precedingCommandSets.end()) { - for (auto precedingSet : precedingCommandSetsIterator->second) { - storm::expressions::Expression conjunctionOverCommands = variableInformation.manager->boolean(true); - for (auto command : precedingSet) { - if (relevancyInformation.knownCommands.find(command) == relevancyInformation.knownCommands.end()) { - conjunctionOverCommands = conjunctionOverCommands && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); + auto precedingLabelSetsIterator = precedingLabelSets.find(synchSet); + if (precedingLabelSetsIterator != precedingLabelSets.end()) { + for (auto precedingSet : precedingLabelSetsIterator->second) { + storm::expressions::Expression conjunctionOverLabels = variableInformation.manager->boolean(true); + for (auto label : precedingSet) { + if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { + conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); } } - disjunctionOverPredecessors = disjunctionOverPredecessors || conjunctionOverCommands; + disjunctionOverPredecessors = disjunctionOverPredecessors || conjunctionOverLabels; } } alternativeExpression = alternativeExpression && disjunctionOverPredecessors; } - alternativeExpressionForCommand = alternativeExpressionForCommand || alternativeExpression; + alternativeExpressionForLabel = alternativeExpressionForLabel || alternativeExpression; } - finalDisjunct = finalDisjunct && alternativeExpressionForCommand; + finalDisjunct = finalDisjunct && alternativeExpressionForLabel; } formulae.push_back(finalDisjunct); @@ -893,7 +887,7 @@ 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, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + 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) { if (!variableInformation.hasReachabilityVariables) { throw storm::exceptions::InvalidStateException() << "Impossible to assert reachability cuts without the necessary variables."; @@ -902,7 +896,6 @@ namespace storm { // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // 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) @@ -970,17 +963,17 @@ namespace storm { } } } - storm::expressions::Expression commandExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second); + storm::expressions::Expression labelExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second); for (auto choice : choicesForStatePair) { storm::expressions::Expression choiceExpression = variableInformation.manager->boolean(true); - for (auto element : choiceOrigins.getCommandSet(choice)) { - if (relevancyInformation.knownCommands.find(element) == relevancyInformation.knownCommands.end()) { - choiceExpression = choiceExpression && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(element)); + for (auto element : labelSets.at(choice)) { + if (relevancyInformation.knownLabels.find(element) == relevancyInformation.knownLabels.end()) { + choiceExpression = choiceExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(element)); } } - commandExpression = commandExpression || choiceExpression; + labelExpression = labelExpression || choiceExpression; } - solver.add(commandExpression); + solver.add(labelExpression); // Assert constraint for (2). storm::expressions::Expression orderExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second) || variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(sourceState)).getExpression() < variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(targetState)).getExpression(); @@ -1216,7 +1209,7 @@ namespace storm { * * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. - * @param variableInformation A structure with information about the variables for the commands. + * @param variableInformation A structure with information about the variables for the labels. * @return True iff the constraint system was satisfiable. */ static bool fuMalikMaxsatStep(z3::context& context, z3::solver& solver, std::vector& auxiliaryVariables, std::vector& softConstraints, uint_fast64_t& nextFreeVariableIndex) { @@ -1224,7 +1217,7 @@ namespace storm { for (auto const& auxiliaryVariable : auxiliaryVariables) { assumptions.push_back(!auxiliaryVariable); } - + // Check whether the assumptions are satisfiable. STORM_LOG_DEBUG("Invoking satisfiability checking."); z3::check_result result = solver.check(assumptions); @@ -1281,13 +1274,13 @@ namespace storm { * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. * @param commandSet The command set to rule out as a solution. - * @param variableInformation A structure with information about the variables for the commands. + * @param variableInformation A structure with information about the variables for the labels. */ static void ruleOutSolution(z3::context& context, z3::solver& solver, boost::container::flat_set const& commandSet, VariableInformation const& variableInformation) { z3::expr blockSolutionExpression = context.bool_val(false); - for (auto commandIndexPair : variableInformation.commandToIndexMap) { - if (commandSet.find(commandIndexPair.first) != commandSet.end()) { - blockSolutionExpression = blockSolutionExpression || variableInformation.commandVariables[commandIndexPair.second]; + for (auto labelIndexPair : variableInformation.labelToIndexMap) { + if (commandSet.find(labelIndexPair.first) != commandSet.end()) { + blockSolutionExpression = blockSolutionExpression || variableInformation.labelVariables[labelIndexPair.second]; } } @@ -1295,18 +1288,18 @@ namespace storm { } /*! - * Determines the set of commands that was chosen by the given model. + * Determines the set of labels that was chosen by the given model. * * @param model The model from which to extract the information. * @param variableInformation A structure with information about the variables of the solver. */ - static boost::container::flat_set getUsedCommandSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) { + static boost::container::flat_set getUsedLabelSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) { boost::container::flat_set result; - for (auto const& commandIndexPair : variableInformation.commandToIndexMap) { - bool commandIncluded = model.getBooleanValue(variableInformation.commandVariables.at(commandIndexPair.second)); + for (auto const& labelIndexPair : variableInformation.labelToIndexMap) { + bool commandIncluded = model.getBooleanValue(variableInformation.labelVariables.at(labelIndexPair.second)); if (commandIncluded) { - result.insert(commandIndexPair.first); + result.insert(labelIndexPair.first); } } return result; @@ -1323,7 +1316,7 @@ namespace storm { std::stringstream variableName; std::vector result; - std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.commandVariables); + std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.labelVariables); for (uint_fast64_t i = 0; i < adderVariables.size(); ++i) { variableName.str(""); variableName.clear(); @@ -1336,13 +1329,13 @@ namespace storm { } /*! - * Finds the smallest set of commands such that the constraint system of the solver is still satisfiable. + * Finds the smallest set of labels such that the constraint system of the solver is still satisfiable. * * @param solver The solver to use for the satisfiability evaluation. * @param variableInformation A structure with information about the variables of the solver. - * @param currentBound The currently known lower bound for the number of commands that need to be enabled + * @param currentBound The currently known lower bound for the number of labels that need to be enabled * in order to satisfy the constraint system. - * @return The smallest set of commands such that the constraint system of the solver is satisfiable. + * @return The smallest set of labels such that the constraint system of the solver is satisfiable. */ static boost::container::flat_set findSmallestCommandSet(storm::solver::SmtSolver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { // Check if we can find a solution with the current bound. @@ -1357,9 +1350,9 @@ namespace storm { assumption = !variableInformation.auxiliaryVariables.back(); } - // At this point we know that the constraint system was satisfiable, so compute the induced command + // At this point we know that the constraint system was satisfiable, so compute the induced label // set and return it. - return getUsedCommandSet(*solver.getModel(), variableInformation); + return getUsedLabelSet(*solver.getModel(), variableInformation); } /*! @@ -1373,7 +1366,7 @@ namespace storm { * @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, storm::models::sparse::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + 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()); STORM_LOG_DEBUG("Analyzing solution with zero probability."); @@ -1389,11 +1382,9 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); - storm::storage::sparse::PrismChoiceOrigins const& subChoiceOrigins = subMdp.getChoiceOrigins()->asPrismChoiceOrigins(); - // Now determine which states and commands are actually reachable. - - boost::container::flat_set reachableCommands; + // Now determine which states and labels are actually reachable. + boost::container::flat_set reachableLabels; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1414,8 +1405,8 @@ namespace storm { } if (choiceTargetsRelevantState) { - for (auto command : subChoiceOrigins.getCommandSet(currentChoice)) { - reachableCommands.insert(command); + for (auto label : subLabelSets[currentChoice]) { + reachableLabels.insert(label); } } } @@ -1431,20 +1422,18 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); - boost::container::flat_set locallyRelevantCommands; - std::set_difference(relevancyInformation.relevantCommands.begin(), relevancyInformation.relevantCommands.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantCommands, locallyRelevantCommands.begin())); + boost::container::flat_set locallyRelevantLabels; + std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - storm::storage::sparse::PrismChoiceOrigins const& originalChoiceOrigins = originalMdp.getChoiceOrigins()->asPrismChoiceOrigins(); - - std::vector> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantCommands); - STORM_LOG_DEBUG("Found " << reachableCommands.size() << " reachable commands and " << reachableStates.getNumberOfSetBits() << " reachable states."); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, 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 // and possess a (disabled) option to leave the reachable part of the state space. - std::set> cutCommands; + std::set> cutLabels; for (auto state : reachableStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { - if (!std::includes(commandSet.begin(), commandSet.end(), originalChoiceOrigins.getCommandSet(currentChoice).begin(), originalChoiceOrigins.getCommandSet(currentChoice).end())) { + if (!std::includes(commandSet.begin(), commandSet.end(), originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end())) { bool isBorderChoice = false; // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. @@ -1455,15 +1444,15 @@ namespace storm { } if (isBorderChoice) { - boost::container::flat_set currentCommandSet; - for (auto command : originalChoiceOrigins.getCommandSet(currentChoice)) { - if (commandSet.find(command) == commandSet.end()) { - currentCommandSet.insert(command); + boost::container::flat_set currentLabelSet; + for (auto label : originalLabelSets.at(currentChoice)) { + if (commandSet.find(label) == commandSet.end()) { + currentLabelSet.insert(label); } } - std::set_difference(guaranteedCommandSets[state].begin(), guaranteedCommandSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentCommandSet, currentCommandSet.end())); + std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); - cutCommands.insert(currentCommandSet); + cutLabels.insert(currentLabelSet); } } } @@ -1471,15 +1460,15 @@ namespace storm { // Given the results of the previous analysis, we construct the implications. std::vector formulae; - boost::container::flat_set unknownReachableCommands; - std::set_difference(reachableCommands.begin(), reachableCommands.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownReachableCommands, unknownReachableCommands.end())); - for (auto command : unknownReachableCommands) { - formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); + boost::container::flat_set unknownReachableLabels; + std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); + for (auto label : unknownReachableLabels) { + formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } - for (auto const& cutCommandSet : cutCommands) { + for (auto const& cutLabelSet : cutLabels) { storm::expressions::Expression cube = variableInformation.manager->boolean(true); - for (auto cutCommand : cutCommandSet) { - cube = cube && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(cutCommand)); + for (auto cutLabel : cutLabelSet) { + cube = cube && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel)); } formulae.push_back(cube); @@ -1501,7 +1490,7 @@ namespace storm { * @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, storm::models::sparse::Mdp const& originalMdp, 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::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_LOG_DEBUG("Analyzing solution with insufficient probability."); @@ -1517,10 +1506,9 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); - storm::storage::sparse::PrismChoiceOrigins const& subChoiceOrigins = subMdp.getChoiceOrigins()->asPrismChoiceOrigins(); - // Now determine which states and commands are actually reachable. - boost::container::flat_set reachableCommands; + // Now determine which states and labels are actually reachable. + boost::container::flat_set reachableLabels; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1541,8 +1529,8 @@ namespace storm { } if (choiceTargetsRelevantState) { - for (auto command : subChoiceOrigins.getCommandSet(currentChoice)) { - reachableCommands.insert(command); + for (auto label : subLabelSets[currentChoice]) { + reachableLabels.insert(label); } } } @@ -1552,42 +1540,40 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); - boost::container::flat_set locallyRelevantCommands; - std::set_difference(relevancyInformation.relevantCommands.begin(), relevancyInformation.relevantCommands.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantCommands, locallyRelevantCommands.begin())); - - storm::storage::sparse::PrismChoiceOrigins const& originalChoiceOrigins = originalMdp.getChoiceOrigins()->asPrismChoiceOrigins(); + 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> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantCommands); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); // Search for states for which we could enable another option and possibly improve the reachability probability. - std::set> cutCommands; + std::set> cutLabels; for (auto state : reachableStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { - if (!std::includes(commandSet.begin(), commandSet.end(), originalChoiceOrigins.getCommandSet(currentChoice).begin(), originalChoiceOrigins.getCommandSet(currentChoice).end())) { - boost::container::flat_set currentCommandSet; - for (auto command : originalChoiceOrigins.getCommandSet(currentChoice)) { - if (commandSet.find(command) == commandSet.end()) { - currentCommandSet.insert(command); + if (!std::includes(commandSet.begin(), commandSet.end(), originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end())) { + boost::container::flat_set currentLabelSet; + for (auto label : originalLabelSets[currentChoice]) { + if (commandSet.find(label) == commandSet.end()) { + currentLabelSet.insert(label); } } - std::set_difference(guaranteedCommandSets[state].begin(), guaranteedCommandSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentCommandSet, currentCommandSet.end())); + std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); - cutCommands.insert(currentCommandSet); + cutLabels.insert(currentLabelSet); } } } // Given the results of the previous analysis, we construct the implications std::vector formulae; - boost::container::flat_set unknownReachableCommands; - std::set_difference(reachableCommands.begin(), reachableCommands.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownReachableCommands, unknownReachableCommands.end())); - for (auto command : unknownReachableCommands) { - formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); + boost::container::flat_set unknownReachableLabels; + std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); + for (auto label : unknownReachableLabels) { + formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } - for (auto const& cutCommandSet : cutCommands) { + for (auto const& cutLabelSet : cutLabels) { storm::expressions::Expression cube = variableInformation.manager->boolean(true); - for (auto cutCommand : cutCommandSet) { - cube = cube && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(cutCommand)); + for (auto cutLabel : cutLabelSet) { + cube = cube && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel)); } formulae.push_back(cube); @@ -1597,27 +1583,25 @@ namespace storm { assertDisjunction(solver, formulae, *variableInformation.manager); } #endif - - public: + /*! - * Returns the submdp obtained from removing all choices that do not originate from the specified commandset. + * Returns the submdp obtained from removing all choices that do not originate from the specified filterLabelSet. + * Also returns the Labelsets of the submdp */ - static storm::models::sparse::Mdp restrictMdpToCommandSet(storm::models::sparse::Mdp const& mdp, boost::container::flat_set const& enabledCommands) { - STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to 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."); + static std::pair, std::vector>> restrictMdpToLabelSet(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, boost::container::flat_set const& filterLabelSet) { - storm::storage::sparse::PrismChoiceOrigins const& prismChoiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); + STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); + std::vector> resultLabelSet; storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, mdp.getTransitionMatrix().getColumnCount(), 0, true, true, mdp.getTransitionMatrix().getRowGroupCount()); - std::vector subMdpChoiceIndexMapping; // 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) { bool stateHasValidChoice = false; for (uint_fast64_t choice = mdp.getTransitionMatrix().getRowGroupIndices()[state]; choice < mdp.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { - bool choiceValid = std::includes(enabledCommands.begin(), enabledCommands.end(), prismChoiceOrigins.getCommandSet(choice).begin(), prismChoiceOrigins.getCommandSet(choice).end()); + bool choiceValid = std::includes(filterLabelSet.begin(), filterLabelSet.end(), labelSets[choice].begin(), labelSets[choice].end()); // If the choice is valid, copy over all its elements. if (choiceValid) { @@ -1628,7 +1612,7 @@ namespace storm { for (auto const& entry : mdp.getTransitionMatrix().getRow(choice)) { transitionMatrixBuilder.addNextValue(currentRow, entry.getColumn(), entry.getValue()); } - subMdpChoiceIndexMapping.push_back(choice); + resultLabelSet.push_back(labelSets[choice]); ++currentRow; } } @@ -1637,17 +1621,20 @@ namespace storm { if (!stateHasValidChoice) { transitionMatrixBuilder.newRowGroup(currentRow); transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::one()); - subMdpChoiceIndexMapping.push_back(std::numeric_limits::max()); + // Insert an empty label set for this choice + resultLabelSet.emplace_back(); ++currentRow; } } - storm::storage::sparse::ModelComponents resultComponents(transitionMatrixBuilder.build()); - resultComponents.stateLabeling = mdp.getStateLabeling(); - resultComponents.choiceOrigins = prismChoiceOrigins.selectChoices(subMdpChoiceIndexMapping); - return storm::models::sparse::Mdp(std::move(resultComponents)); + storm::models::sparse::Mdp resultMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(mdp.getStateLabeling())); + + return std::make_pair(std::move(resultMdp), std::move(resultLabelSet)); } + public: + + /*! * Computes the minimal command set that is needed in the given MDP to exceed the given probability threshold for satisfying phi until psi. * @@ -1680,7 +1667,16 @@ namespace storm { auto analysisClock = std::chrono::high_resolution_clock::now(); decltype(std::chrono::high_resolution_clock::now() - analysisClock) totalAnalysisTime(0); - STORM_LOG_THROW(mdp.hasChoiceOrigins() && mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to Prism command set is impossible for model without Prism choice origins."); + // (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 origns."); + 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(); + std::vector> labelSets; + labelSets.reserve(mdp.getNumberOfChoices()); + for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) { + labelSets.push_back(choiceOrigins.getCommandSet(choice)); + } // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; @@ -1696,7 +1692,7 @@ namespace storm { } // (2) Identify all states and commands that are relevant, because only these need to be considered later. - RelevancyInformation relevancyInformation = determineRelevantStatesAndCommands(mdp, phiStates, psiStates); + RelevancyInformation relevancyInformation = determineRelevantStatesAndLabels(mdp, labelSets, phiStates, psiStates); // (3) Create a solver. std::shared_ptr manager(new storm::expressions::ExpressionManager()); @@ -1706,20 +1702,20 @@ namespace storm { VariableInformation variableInformation = createVariables(manager, mdp, 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 command - // variables that were set to true. Initially, we are looking for a solution that has no command enabled + // (5) Now assert an adder whose result variables can later be used to constrain the nummber of label + // variables that were set to true. Initially, we are looking for a solution that has no label enabled // and subsequently relax that. variableInformation.adderVariables = assertAdder(*solver, variableInformation); variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(*solver, variableInformation, 0)); // (6) Add constraints that cut off a lot of suboptimal solutions. STORM_LOG_DEBUG("Asserting cuts."); - assertExplicitCuts(mdp, psiStates, variableInformation, relevancyInformation, *solver); + assertExplicitCuts(mdp, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted explicit cuts."); - assertSymbolicCuts(program, mdp, variableInformation, relevancyInformation, *solver); + assertSymbolicCuts(program, mdp, labelSets, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted symbolic cuts."); if (includeReachabilityEncoding) { - assertReachabilityCuts(mdp, psiStates, variableInformation, relevancyInformation, *solver); + assertReachabilityCuts(mdp, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted reachability cuts."); } @@ -1727,12 +1723,12 @@ namespace storm { totalSetupTime = std::chrono::high_resolution_clock::now() - setupTimeClock; // (7) Find the smallest set of commands that satisfies all constraints. If the probability of - // satisfying phi until psi exceeds the given threshold, the set of commands is minimal and can be returned. + // 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. // Set up some variables for the iterations. - boost::container::flat_set commandSet(relevancyInformation.relevantCommands); + boost::container::flat_set commandSet(relevancyInformation.relevantLabels); bool done = false; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; @@ -1743,14 +1739,15 @@ namespace storm { solverClock = std::chrono::high_resolution_clock::now(); commandSet = findSmallestCommandSet(*solver, variableInformation, currentBound); totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock; - STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownCommands.size()) << "."); + STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << "."); - // Restrict the given MDP to the current set of commands and compute the reachability probability. + // Restrict the given MDP to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); - commandSet.insert(relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end()); - storm::models::sparse::Mdp const& subMdp = restrictMdpToCommandSet(mdp, commandSet); - STORM_LOG_THROW(subMdp.hasChoiceOrigins() && subMdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Expected prism choice origins for submodel."); - + commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); + auto subMdpChoiceOrigins = restrictMdpToLabelSet(mdp, labelSets, commandSet); + storm::models::sparse::Mdp const& subMdp = subMdpChoiceOrigins.first; + std::vector> const& subLabelSets = subMdpChoiceOrigins.second; + storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; STORM_LOG_DEBUG("Invoking model checker."); std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); @@ -1770,11 +1767,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, mdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeZeroProbabilitySolution(*solver, subMdp, subLabelSets, mdp, 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, mdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeInsufficientProbabilitySolution(*solver, subMdp, subLabelSets, mdp, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } } else { done = true; @@ -1805,7 +1802,6 @@ namespace storm { std::cout << " * number of models that could not reach a target state: " << zeroProbabilityCount << " (" << 100 * static_cast(zeroProbabilityCount)/iterations << "%)" << std::endl << std::endl; } - return commandSet; #else throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3."; @@ -1814,7 +1810,7 @@ namespace storm { static std::shared_ptr computeCounterexample(storm::prism::Program program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 - std::cout << std::endl << "Generating minimal command set counterexample for formula " << *formula << std::endl; + 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."); storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); @@ -1859,8 +1855,10 @@ namespace storm { std::cout << std::endl << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; return std::make_shared(program.restrictCommands(commandSet)); + #else throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3."; + return nullptr; #endif } @@ -1869,4 +1867,4 @@ namespace storm { } // namespace counterexamples } // namespace storm -#endif /* STORM_COUNTEREXAMPLES_SMTMINIMALCOMMANDSETGENERATOR_MDP_H_ */ +#endif /* STORM_COUNTEREXAMPLES_SMTMINIMALLABELSETGENERATOR_MDP_H_ */ diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h index c77092923..ec20c20cb 100644 --- a/src/storm/utility/counterexamples.h +++ b/src/storm/utility/counterexamples.h @@ -11,23 +11,23 @@ namespace storm { namespace counterexamples { /*! - * Computes a set of Prism commands that is executed along all paths from any state to a target state. + * Computes a set of labels that is executed along all paths from any state to a target state. * - * @return The set of Prism commands that is visited on all paths from any state to a target state. + * @param labelSet the considered label sets (a label set is assigned to each choice) + * + * @return The set of labels that is visited on all paths from any state to a target state. */ template - std::vector> getGuaranteedCommandSets(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantCommands) { - STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without choice origns."); - STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + std::vector> getGuaranteedLabelSets(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); - storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); - // Now we compute the set of commands that is present on all paths from the initial to the target states. - std::vector> analysisInformation(mdp.getNumberOfStates(), relevantCommands); + // Now we compute the set of labels that is present on all paths from the initial to the target states. + std::vector> analysisInformation(mdp.getNumberOfStates(), relevantLabels); std::queue worklist; storm::storage::BitVector statesInWorkList(mdp.getNumberOfStates()); @@ -65,13 +65,13 @@ namespace storm { // If we can reach the target state with this choice, we need to intersect the current // analysis information with the union of the new analysis information of the target state - // and the choice commands. + // and the choice labels. if (modifiedChoice) { for (auto const& entry : transitionMatrix.getRow(currentChoice)) { if (markedStates.get(entry.getColumn())) { boost::container::flat_set tmpIntersection; std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceOrigins.getCommandSet(currentChoice).begin(), choiceOrigins.getCommandSet(currentChoice).end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); analysisInformation[currentState] = std::move(tmpIntersection); } } @@ -101,22 +101,24 @@ namespace storm { } /*! - * Computes a set of prism commands that is executed along all paths from an initial state to a target state. + * Computes a set of labels that is executed along all paths from an initial state to a target state. + * + * @param labelSet the considered label sets (a label set is assigned to each choice) * - * @return The set of prism commands that is executed on all paths from an initial state to a target state. + * @return The set of labels that is executed on all paths from an initial state to a target state. */ template - boost::container::flat_set getGuaranteedCommandSet(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantCommands) { - std::vector> guaranteedCommands = getGuaranteedCommandSets(mdp, psiStates, relevantCommands); + boost::container::flat_set getGuaranteedLabelSet(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(mdp, labelSets, psiStates, relevantLabels); - boost::container::flat_set knownCommands(relevantCommands); + boost::container::flat_set knownLabels(relevantLabels); boost::container::flat_set tempIntersection; for (auto initialState : mdp.getInitialStates()) { - std::set_intersection(knownCommands.begin(), knownCommands.end(), guaranteedCommands[initialState].begin(), guaranteedCommands[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); - std::swap(knownCommands, tempIntersection); + std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); + std::swap(knownLabels, tempIntersection); } - return knownCommands; + return knownLabels; } } // namespace counterexample