diff --git a/src/counterexamples/MinimalLabelSetGenerator.h b/src/counterexamples/MinimalLabelSetGenerator.h index cc1edd255..087cc22c4 100644 --- a/src/counterexamples/MinimalLabelSetGenerator.h +++ b/src/counterexamples/MinimalLabelSetGenerator.h @@ -24,93 +24,142 @@ extern "C" { namespace storm { namespace counterexamples { - /*! - * A helper class that provides the functionality to compute a hash value for pairs of indices. - */ - class PairHash { - public: - std::size_t operator()(std::pair const& pair) const { - size_t seed = 0; - boost::hash_combine(seed, pair.first); - boost::hash_combine(seed, pair.second); - return seed; - } - }; - /*! * This class provides functionality to generate a minimal counterexample to a probabilistic reachability * property in terms of used labels. */ template class MinimalLabelSetGenerator { - - public: - - static std::unordered_set getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, T lowerProbabilityBound, bool checkThresholdFeasible = false) { -#ifdef HAVE_GUROBI - // (0) Check whether the MDP is indeed labeled. - if (!labeledMdp.hasChoiceLabels()) { - throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; + private: + /*! + * A helper class that provides the functionality to compute a hash value for pairs of state indices. + */ + class PairHash { + public: + std::size_t operator()(std::pair const& pair) const { + size_t seed = 0; + boost::hash_combine(seed, pair.first); + boost::hash_combine(seed, pair.second); + return seed; } - - // (1) TODO: check whether its possible to exceed the threshold if checkThresholdFeasible is set. - - // (2) Identify relevant and problematic states. - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); - storm::storage::BitVector relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); - relevantStates &= ~psiStates; - storm::storage::BitVector problematicStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); - problematicStates.complement(); - problematicStates &= relevantStates; - LOG4CPLUS_INFO(logger, "Found " << phiStates.getNumberOfSetBits() << " filter states (" << phiStates.toString() << ")."); - LOG4CPLUS_INFO(logger, "Found " << psiStates.getNumberOfSetBits() << " target states (" << psiStates.toString() << ")."); - LOG4CPLUS_INFO(logger, "Found " << relevantStates.getNumberOfSetBits() << " relevant states (" << relevantStates.toString() << ")."); - LOG4CPLUS_INFO(logger, "Found " << problematicStates.getNumberOfSetBits() << " problematic states (" << problematicStates.toString() << ")."); - - // (3) Determine sets of relevant labels and problematic choices. + }; + + /*! + * A helper struct storing which states are relevant or problematic. + */ + struct StateInformation { + storm::storage::BitVector relevantStates; + storm::storage::BitVector problematicStates; + }; + + /*! + * 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; - std::unordered_set relevantLabels; + std::unordered_set allRelevantLabels; + }; + + /*! + * A helper struct capturing information about the variables of the MILP formulation. + */ + struct VariableInformation { + std::unordered_map labelToVariableIndexMap; + std::unordered_map> stateToChoiceVariablesIndexMap; + std::unordered_map stateToProbabilityVariableIndexMap; + std::unordered_map problematicStateToVariableIndexMap; + std::unordered_map, uint_fast64_t, PairHash> problematicTransitionToVariableIndexMap; + uint_fast64_t nextFreeVariableIndex = 0; + }; + + /*! + * Determines the relevant and the problematic states of the given MDP with respect to the given phi and psi + * state sets. The relevant states are those for which there exists at least one scheduler that attains a + * non-zero probability of satisfying phi until psi. Problematic states are relevant states that have at + * least one scheduler such that the probability of satisfying phi until psi is zero. + * + * @param labeledMdp The MDP whose states to search. + * @param phiStates A bit vector characterizing all states satisfying phi. + * @param psiStates A bit vector characterizing all states satisfying psi. + * @return A structure that stores the relevant and problematic states. + */ + static struct StateInformation determineRelevantAndProblematicStates(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + StateInformation result; + storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + result.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); + result.relevantStates &= ~psiStates; + storm::storage::BitVector problematicStates = storm::utility::graph::performProbGreater0E(labeledMdp, backwardTransitions, phiStates, psiStates); + result.problematicStates.complement(); + result.problematicStates &= result.relevantStates; + LOG4CPLUS_DEBUG(logger, "Found " << phiStates.getNumberOfSetBits() << " filter states (" << phiStates.toString() << ")."); + LOG4CPLUS_DEBUG(logger, "Found " << psiStates.getNumberOfSetBits() << " target states (" << psiStates.toString() << ")."); + LOG4CPLUS_DEBUG(logger, "Found " << result.relevantStates.getNumberOfSetBits() << " relevant states (" << result.relevantStates.toString() << ")."); + LOG4CPLUS_DEBUG(logger, "Found " << result.problematicStates.getNumberOfSetBits() << " problematic states (" << result.problematicStates.toString() << ")."); + return result; + } + + /*! + * Determines the relevant and problematic choices of the given MDP with respect to the given parameters. + * + * @param labeledMdp The MDP whose choices to search. + * @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 labels. + */ + static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { + // Create result and shortcuts to needed data for convenience. + ChoiceInformation result; storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + // Now traverse all choices of all relevant states and check whether there is a relevant target state. - // If so, the associated labels become relevant. - for (auto state : relevantStates) { - relevantChoicesForRelevantStates.emplace(state, std::list()); - if (problematicStates.get(state)) { - problematicChoicesForProblematicStates.emplace(state, std::list()); + // 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()); + if (stateInformation.problematicStates.get(state)) { + result.problematicChoicesForProblematicStates.emplace(state, std::list()); } for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row) { bool currentChoiceRelevant = false; bool allSuccessorsProblematic = true; for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) { // If there is a relevant successor, we need to add the labels of the current choice. - if (relevantStates.get(*successorIt) || psiStates.get(*successorIt)) { + if (stateInformation.relevantStates.get(*successorIt) || psiStates.get(*successorIt)) { for (auto const& label : choiceLabeling[row]) { - relevantLabels.insert(label); + result.relevantLabels.insert(label); } if (!currentChoiceRelevant) { currentChoiceRelevant = true; - relevantChoicesForRelevantStates[state].emplace_back(row); + result.relevantChoicesForRelevantStates[state].emplace_back(row); } } - if (!problematicStates.get(*successorIt)) { + if (!stateInformation.problematicStates.get(*successorIt)) { allSuccessorsProblematic = false; } } - if (problematicStates.get(state) && allSuccessorsProblematic) { - problematicChoicesForProblematicStates[state].emplace_back(row); + + // If all successors of a problematic state are problematic themselves, we record this choice + // as being problematic. + if (stateInformation.problematicStates.get(state) && allSuccessorsProblematic) { + result.problematicChoicesForProblematicStates[state].emplace_back(row); } } } - LOG4CPLUS_INFO(logger, "Found " << relevantLabels.size() << " relevant labels."); - for (auto label : relevantLabels) { - LOG4CPLUS_INFO(logger, "Relevant label " << label << "."); - } - - // (3) Encode resulting system as MILP problem. - // (3.1) Initialize MILP solver and model. + LOG4CPLUS_DEBUG(logger, "Found " << result.relevantLabels.size() << " relevant labels."); + return result; + } + + /*! + * Creates a Gurobi environment and model and returns pointers to them. + * + * @return A pair of two pointers to a Gurobi environment and model, respectively. + */ + static std::pair getGurobiEnvironmentAndModel() { GRBenv* env = nullptr; int error = GRBloadenv(&env, "storm_gurobi.log"); if (error || env == NULL) { @@ -118,22 +167,29 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Could not initialize Gurobi (" << GRBgeterrormsg(env) << ")."; } GRBmodel* model = nullptr; - error = GRBnewmodel(env, &model, "storm_milp", 0, nullptr, nullptr, nullptr, nullptr, nullptr); + error = GRBnewmodel(env, &model, "minimal_label_milp", 0, nullptr, nullptr, nullptr, nullptr, nullptr); if (error) { LOG4CPLUS_ERROR(logger, "Could not initialize Gurobi model (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not initialize Gurobi model (" << GRBgeterrormsg(env) << ")."; } - - // (3.2) Create variables. - - // Prepare internal variables. + return std::make_pair(env, model); + } + + /*! + * Creates the variables for the labels of the model. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param relevantLabels The set of relevant labels of the model. + * @param nextFreeVariableIndex A reference to the next free variable index. Note: when creating new + * variables, this value is increased. + * @return A mapping from labels to variable indices. + */ + static std::unordered_map createLabelVariables(GRBenv* env, GRBmodel* model, std::unordered_set const& relevantLabels, uint_fast64_t& nextFreeVariableIndex) { + int error = 0; std::stringstream variableNameBuffer; - uint_fast64_t nextLabelIndex = 0; - - // Create variables for involved labels. - std::unordered_map labelToIndexMap; + std::unordered_map resultingMap; for (auto const& label : relevantLabels) { - // Reset stringstream properly to construct new variable name. variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "label" << label; @@ -142,17 +198,31 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."; } - labelToIndexMap[label] = nextLabelIndex; - ++nextLabelIndex; + resultingMap[label] = nextFreeVariableIndex; + ++nextFreeVariableIndex; } - - // Create scheduler variables for relevant states and their actions. - std::unordered_map stateToStartingIndexMap; - for (auto state : relevantStates) { - std::list const& relevantChoicesForState = relevantChoicesForRelevantStates[state]; - stateToStartingIndexMap[state] = nextLabelIndex; + return resultingMap; + } + + /*! + * Creates the variables for the relevant choices in the model. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param stateInformation The information about the states of the model. + * @param choiceInformation The information about the choices of the model. + * @param nextFreeVariableIndex A reference to the next free variable index. Note: when creating new + * variables, this value is increased. + * @return A mapping from states to a list of choice variable indices. + */ + static std::unordered_map> createSchedulerVariables(GRBenv* env, GRBmodel* model, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, uint_fast64_t& nextFreeVariableIndex) { + int error = 0; + std::stringstream variableNameBuffer; + std::unordered_map> resultingMap; + for (auto state : stateInformation.relevantStates) { + resultingMap.emplace(state, std::list()); + std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates[state]; for (uint_fast64_t row : relevantChoicesForState) { - // Reset stringstream properly to construct new variable name. variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "choice" << row << "in" << state; @@ -161,14 +231,28 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."; } - ++nextLabelIndex; + resultingMap[state].emplace_back(nextFreeVariableIndex); + ++nextFreeVariableIndex; } } - - // Create variables for probabilities for all relevant states. - std::unordered_map stateToProbabilityVariableIndex; - for (auto state : relevantStates) { - // Reset stringstream properly to construct new variable name. + return resultingMap; + } + + /*! + * Creates the variables for the probabilities in the model. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param stateInformation The information about the states in the model. + * @param nextFreeVariableIndex A reference to the next free variable index. Note: when creating new + * variables, this value is increased. + * @return A mapping from states to the index of the corresponding probability variables. + */ + static std::unordered_map createProbabilityVariables(GRBenv* env, GRBmodel* model, StateInformation const& stateInformation, uint_fast64_t& nextFreeVariableIndex) { + int error = 0; + std::stringstream variableNameBuffer; + std::unordered_map resultingMap; + for (auto state : stateInformation.relevantStates) { variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "p" << state; @@ -177,36 +261,48 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."; } - stateToProbabilityVariableIndex[state] = nextLabelIndex; - ++nextLabelIndex; + resultingMap[state] = nextFreeVariableIndex; + ++nextFreeVariableIndex; } - - // Create variables for problematic states, successors of problematic states and transitions of problematic states. - std::unordered_map problematicStateVariablesToIndexMap; - std::unordered_map, uint_fast64_t, PairHash> problematicTransitionVariables; - for (auto state : problematicStates) { - // First check whether there is not already a variable for this state and proceed with next state. - if (problematicStateVariablesToIndexMap.find(state) == problematicStateVariablesToIndexMap.end()) { - // Reset stringstream properly to construct new variable name. + return resultingMap; + } + + /*! + * Creates the variables for the problematic states in the model. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param labeledMdp The labeled MDP. + * @param stateInformation The information about the states in the model. + * @param nextFreeVariableIndex A reference to the next free variable index. Note: when creating new + * variables, this value is increased. + * @return A mapping from problematic states to the index of the corresponding variables. + */ + static std::unordered_map createProblematicStateVariables(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, uint_fast64_t& nextFreeVariableIndex) { + int error = 0; + std::stringstream variableNameBuffer; + std::unordered_map resultingMap; + for (auto state : stateInformation.problematicStates) { + // First check whether there is not already a variable for this state and advance to the next state + // in this case. + if (resultingMap.find(state) == resultingMap.end()) { variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "r" << state; - std::cout << "Creating r variable" << std::endl; error = GRBaddvar(model, 0, nullptr, nullptr, 0.0, 0.0, 1.0, GRB_CONTINUOUS, variableNameBuffer.str().c_str()); if (error) { LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."; } - problematicStateVariablesToIndexMap[state] = nextLabelIndex; - ++nextLabelIndex; + resultingMap[state] = nextFreeVariableIndex; + ++nextFreeVariableIndex; } - std::list const& relevantChoicesForState = relevantChoicesForRelevantStates[state]; - for (uint_fast64_t row : relevantChoicesForState) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(row); successorIt != transitionMatrix.constColumnIteratorEnd(row); ++successorIt) { - if (relevantStates.get(*successorIt)) { - if (problematicStateVariablesToIndexMap.find(*successorIt) == problematicStateVariablesToIndexMap.end()) { - // Reset stringstream properly to construct new variable name. + std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates[state]; + for (uint_fast64_t row : choiceInformation.relevantChoicesForState) { + for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(row); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(row); ++successorIt) { + if (stateInformation.relevantStates.get(*successorIt)) { + if (resultingMap.find(*successorIt) == resultingMap.end()) { variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "r" << *successorIt; @@ -215,9 +311,37 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."; } - problematicStateVariablesToIndexMap[state] = nextLabelIndex; - ++nextLabelIndex; + resultingMap[state] = nextFreeVariableIndex; + ++nextFreeVariableIndex; } + } + } + } + } + return resultingMap; + } + + /*! + * Creates the variables for the problematic choices in the model. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param labeledMdp The labeled MDP. + * @param stateInformation The information about the states in the model. + * @param choiceInformation The information about the choices in the model. + * @param nextFreeVariableIndex A reference to the next free variable index. Note: when creating new + * variables, this value is increased. + * @return A mapping from problematic choices to the index of the corresponding variables. + */ + static std::unordered_map, uint_fast64_t, PairHash> createProblematicChoiceVariables(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, uint_fast64_t& nextFreeVariableIndex) { + int error = 0; + std::stringstream variableNameBuffer; + std::unordered_map, uint_fast64_t, PairHash> resultingMap; + for (auto state : stateInformation.problematicStates) { + std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates[state]; + for (uint_fast64_t row : choiceInformation.relevantChoicesForState) { + for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = labeledMdp.getTransitionMatrix().constColumnIteratorBegin(row); successorIt != labeledMdp.getTransitionMatrix().constColumnIteratorEnd(row); ++successorIt) { + if (stateInformation.relevantStates.get(*successorIt)) { variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "t" << state << "to" << *successorIt; @@ -226,58 +350,134 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ")."; } - problematicTransitionVariables[std::make_pair(state, *successorIt)] = nextLabelIndex; - ++nextLabelIndex; + resultingMap[std::make_pair(state, *successorIt)] = nextFreeVariableIndex; + ++nextFreeVariableIndex; } } } } + return resultingMap; + } + + /*! + * Creates all variables needed to encode the problem as an MILP problem and returns a struct containing + * information about the variables that were created. This implicitly establishes the objective function + * passed to the solver. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param labeledMdp The labeled MDP. + * @param stateInformation The information about the states in the model. + * @param choiceInformation The information about the choices in the model. + */ + static VariableInformation createVariables(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + // Create a struct that stores all information about variables. + VariableInformation result; - LOG4CPLUS_INFO(logger, "Successfully created " << nextLabelIndex << " Gurobi variables."); + // Create variables for involved labels. + result.labelToVariableIndexMap = createLabelVariables(env, model, choiceInformation.relevantLabes, result.nextFreeVariableIndex); - // Update model to incorporate prior changes. - error = GRBupdatemodel(model); + // Create scheduler variables for relevant states and their actions. + result.stateToChoiceVariablesIndexMap = createSchedulerVariables(env, model, stateInformation, choiceInformation, result.nextFreeVariableIndex); + + // Create variables for probabilities for all relevant states. + result.stateToProbabilityVariableIndexMap = createProbabilityVariables(env, model, stateInformation, result.nextFreeVariableIndex); + + // Create variables for problematic states. + result.problematicStateToVariableIndexMap = createProblematicStateVariables(env, model, stateInformation, result.nextFreeVariableIndex); + + // Create variables for problematic choices. + result.problematicTransitionToVariableIndexMap = createProblematicChoiceVariables(env, model, stateInformation, choiceInformation, result.nextFreeVariableIndex); + + LOG4CPLUS_INFO(logger, "Successfully created " << result.nextFreeVariableIndex << " Gurobi variables."); + + // Finally, return variable information struct. + return result; + } + + /*! + * Updates the Gurobi model to incorporate any prior changes. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + */ + static void updateModel(GRBenv* env, GRBmodel* model) { + int error = GRBupdatemodel(model); if (error) { LOG4CPLUS_ERROR(logger, "Unable to update Gurobi model (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Unable to update Gurobi model (" << GRBgeterrormsg(env) << ")."; } - - // Make sure we have exactly one initial state and assert that it's probability is above the given threshold. + } + + /*! + * Asserts a constraint in the MILP problem that makes sure the reachability probability in the subsystem + * exceeds the given threshold. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param labeledMdp The labeled MDP. + * @param variableInformation A struct with information about the variables of the model. + * @param probabilityThreshold The probability that the subsystem must exceed. + */ + static void assertProbabilityGreaterThanThreshold(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, VariableInformation const& variableInformation, T probabilityThreshold) { + int error = 0; storm::storage::BitVector const& initialStates = labeledMdp.getLabeledStates("init"); if (initialStates.getNumberOfSetBits() != 1) { LOG4CPLUS_ERROR(logger, "Must have exactly one initial state, but got " << initialStates.getNumberOfSetBits() << "instead."); throw storm::exceptions::InvalidStateException() << "Must have exactly one initial state, but got " << initialStates.getNumberOfSetBits() << "instead."; } for (auto initialState : initialStates) { - int variableIndex = static_cast(stateToProbabilityVariableIndex[initialState]); + int variableIndex = static_cast(variableInformation.stateToProbabilityVariableIndexMap[initialState]); double coefficient = 1.0; - error = GRBaddconstr(model, 1, &variableIndex, &coefficient, GRB_GREATER_EQUAL, lowerProbabilityBound + 1e-6, nullptr); + error = GRBaddconstr(model, 1, &variableIndex, &coefficient, GRB_GREATER_EQUAL, probabilityThreshold + 1e-6, nullptr); if (error) { LOG4CPLUS_ERROR(logger, "Unable to assert constraint (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Unable to assert constraint (" << GRBgeterrormsg(env) << ")."; } } - - // Now add the constaints that ensure that the policy chooses at most one action in each state. - for (auto state : relevantStates) { - uint_fast64_t startingIndex = stateToStartingIndexMap[state]; - std::list const& relevantChoicesForState = relevantChoicesForRelevantStates[state]; + } + + /*! + * Asserts constraints that make sure the selected policy is valid, i.e. chooses at most one action in each state. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param stateInformation The information about the states in the model. + * @param variableInformation A struct with information about the variables of the model. + */ + static void assertValidPolicy(GRBenv* env, GRBmodel* model, StateInformation const& stateInformation, VariableInformation const& variableInformation) { + int error = 0; + for (auto state : stateInformation.relevantStates) { + std::list const& choiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap[state]; std::vector variables; - std::vector coefficients(relevantChoicesForState.size(), 1); - variables.reserve(relevantChoicesForState.size()); - for (auto choice : relevantChoicesForState) { - variables.push_back(static_cast(startingIndex++)); + std::vector coefficients(choiceVariableIndices.size(), 1); + variables.reserve(choiceVariableIndices.size()); + for (auto choiceVariableIndex : choiceVariableIndices) { + variables.push_back(static_cast(choiceVariableIndex)); } - error = GRBaddconstr(model, relevantChoicesForState.size(), &variables[0], &coefficients[0], GRB_LESS_EQUAL, 1, nullptr); + error = GRBaddconstr(model, choiceVariableIndices.size(), &variables[0], &coefficients[0], GRB_LESS_EQUAL, 1, nullptr); if (error) { LOG4CPLUS_ERROR(logger, "Unable to assert constraint (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Unable to assert constraint (" << GRBgeterrormsg(env) << ")."; } } - - // Add constraints that enforce that certain labels are put into the label set when the corresponding - // transitions get selected. - for (auto state : relevantStates) { + } + + /*! + * Asserts constraints that make sure the labels are included in the solution set if the policy selects a + * choice that is labeled with the label in question. + * + * @param env The Gurobi environment. + * @param model The Gurobi model. + * @param labeledMdp The labeled MDP. + * @param stateInformation The information about the states in the model. + * @param choiceInformation The information about the choices in the model. + * @param variableInformation A struct with information about the variables of the model. + */ + static void assertChoicesImplyLabels(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + int error = 0; + for (auto state : stateInformation.relevantStates) { + std::list const& choiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap[state]; uint_fast64_t currentChoiceVariableIndex = stateToStartingIndexMap[state]; for (auto choice : relevantChoicesForRelevantStates[state]) { int indices[2]; indices[0] = 0; indices[1] = currentChoiceVariableIndex; @@ -293,6 +493,53 @@ namespace storm { ++currentChoiceVariableIndex; } } + } + + static void buildConstraintSystem(GRBenv* env, GRBmodel* model, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, T probabilityThreshold) { + // Assert that the reachability probability in the subsystem exceeds the given threshold. + assertProbabilityGreaterThanThreshold(env, model, labeledMdp, variableInformation, probabilityThreshold); + + // Add constraints that assert the policy takes at most one action in each state. + assertValidPolicy(env, model, stateInformation, variableInformation); + + assertChoicesImplyLabels(env, model, labeledMdp, stateInformation, choiceInformation, variableInformation); + } + + // computeLabelSetFromSolution + + public: + + static std::unordered_set getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, T probabilityThreshold, bool checkThresholdFeasible = false) { +#ifdef HAVE_GUROBI + // (0) Check whether the MDP is indeed labeled. + if (!labeledMdp.hasChoiceLabels()) { + throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; + } + + // (1) TODO: check whether its possible to exceed the threshold if checkThresholdFeasible is set. + + // (2) Identify relevant and problematic states. + StateInformation stateInformation = determineRelevantAndProblematicStates(labeledMdp, phiStates, psiStates); + + // (3) Determine sets of relevant labels and problematic choices. + ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(labeledMdp, stateInformation); + + // (4) Encode resulting system as MILP problem. + // (4.1) Initialize MILP solver and model. + std::pair environmentModelPair = getGurobiEnvironmentAndModel(); + + // (4.2) Create variables. + VariableInformation variableInformation = createVariables(environmentModelPair.first, environmentModelPair.second, labeledMdp, stateInformation, choiceInformation); + + // Update model. + updateModel(environmentModelPair.first, environmentModelPair.second); + + // Create all constraints. + buildConstraintSystem(environmentModelPair.first, environmentModelPair.second, labeledMdp, stateInformation, choiceInformation, variableInformation, probabilityThreshold); + + + + // Add constraints that make sure the reachability probability for states that do not choose any action // is zero. @@ -440,8 +687,8 @@ namespace storm { // (4) Read off result from MILP variables. // (5) Shutdown MILP solver. - GRBfreemodel(model); - GRBfreeenv(env); + GRBfreemodel(environmentModelPair.second); + GRBfreeenv(environmentModelPair.first); // (6) Potentially verify whether the resulting system exceeds the given threshold. // (7) Return result.