From 9e746549a8a90923c99e1089ea550021bcf5f92e Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 12 May 2014 11:41:07 +0200 Subject: [PATCH] Fully adapted MILP-based counterexample generator to new LP solver interface. Former-commit-id: 83f3b8c5075c5c614671b82ceb6cf6c762e3592c --- .../MILPMinimalLabelSetGenerator.h | 182 ++++++++---------- src/solver/GlpkLpSolver.h | 4 +- src/solver/GurobiLpSolver.h | 4 +- src/solver/LpSolver.h | 2 +- 4 files changed, 87 insertions(+), 105 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 8da1374c4..ad581e616 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -194,7 +194,7 @@ namespace storm { std::unordered_map> resultingMap; for (auto state : stateInformation.relevantStates) { - resultingMap.emplace(state, std::list()); + resultingMap.emplace(state, std::list()); std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { variableNameBuffer.str(""); @@ -260,7 +260,7 @@ namespace storm { } /*! - * Creates the variables for the probabilities in the model. + * Creates the variable for the probability of the virtual initial state. * * @param solver The MILP solver. * @param maximizeProbability If set to true, the objective function is constructed in a way that a @@ -308,8 +308,8 @@ namespace storm { variableNameBuffer.str(""); variableNameBuffer.clear(); variableNameBuffer << "r" << successorEntry.getColumn(); - resultingMap[state] = variableNameBuffer.str(); - solver.addBoundedContinuousVariable(resultingMap[state], 0, 1); + resultingMap[successorEntry.getColumn()] = variableNameBuffer.str(); + solver.addBoundedContinuousVariable(resultingMap[successorEntry.getColumn()], 0, 1); ++numberOfVariablesCreated; } } @@ -328,10 +328,10 @@ namespace storm { * @param choiceInformation The information about the choices in the model. * @return A mapping from problematic choices to the index of the corresponding variables. */ - static std::pair, uint_fast64_t, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair, std::string, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; - std::unordered_map, uint_fast64_t, PairHash> resultingMap; + std::unordered_map, std::string, PairHash> resultingMap; for (auto state : stateInformation.problematicStates) { std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); @@ -366,44 +366,44 @@ namespace storm { VariableInformation result; // Create variables for involved labels. - std::pair, uint_fast64_t> labelVariableResult = createLabelVariables(solver, choiceInformation.allRelevantLabels); - result.labelToVariableIndexMap = std::move(labelVariableResult.first); + std::pair, uint_fast64_t> labelVariableResult = createLabelVariables(solver, choiceInformation.allRelevantLabels); + result.labelToVariableMap = std::move(labelVariableResult.first); result.numberOfVariables += labelVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for labels."); // Create scheduler variables for relevant states and their actions. - std::pair>, uint_fast64_t> schedulerVariableResult = createSchedulerVariables(solver, stateInformation, choiceInformation); - result.stateToChoiceVariablesIndexMap = std::move(schedulerVariableResult.first); + std::pair>, uint_fast64_t> schedulerVariableResult = createSchedulerVariables(solver, stateInformation, choiceInformation); + result.stateToChoiceVariablesMap = std::move(schedulerVariableResult.first); result.numberOfVariables += schedulerVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for nondeterministic choices."); // Create scheduler variables for nondeterministically choosing an initial state. - std::pair, uint_fast64_t> initialChoiceVariableResult = createInitialChoiceVariables(solver, labeledMdp, stateInformation); - result.initialStateToChoiceVariableIndexMap = std::move(initialChoiceVariableResult.first); + std::pair, uint_fast64_t> initialChoiceVariableResult = createInitialChoiceVariables(solver, labeledMdp, stateInformation); + result.initialStateToChoiceVariableMap = std::move(initialChoiceVariableResult.first); result.numberOfVariables += initialChoiceVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for the nondeterministic choice of the initial state."); // Create variables for probabilities for all relevant states. - std::pair, uint_fast64_t> probabilityVariableResult = createProbabilityVariables(solver, stateInformation); - result.stateToProbabilityVariableIndexMap = std::move(probabilityVariableResult.first); + std::pair, uint_fast64_t> probabilityVariableResult = createProbabilityVariables(solver, stateInformation); + result.stateToProbabilityVariableMap = std::move(probabilityVariableResult.first); result.numberOfVariables += probabilityVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for the reachability probabilities."); // Create a probability variable for a virtual initial state that nondeterministically chooses one of the system's real initial states as its target state. std::pair virtualInitialStateVariableResult = createVirtualInitialStateVariable(solver); - result.virtualInitialStateVariableIndex = virtualInitialStateVariableResult.first; + result.virtualInitialStateVariable = virtualInitialStateVariableResult.first; result.numberOfVariables += virtualInitialStateVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for the virtual initial state."); // Create variables for problematic states. - std::pair, uint_fast64_t> problematicStateVariableResult = createProblematicStateVariables(solver, labeledMdp, stateInformation, choiceInformation); - result.problematicStateToVariableIndexMap = std::move(problematicStateVariableResult.first); + std::pair, uint_fast64_t> problematicStateVariableResult = createProblematicStateVariables(solver, labeledMdp, stateInformation, choiceInformation); + result.problematicStateToVariableMap = std::move(problematicStateVariableResult.first); result.numberOfVariables += problematicStateVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for the problematic states."); // Create variables for problematic choices. - std::pair, uint_fast64_t, PairHash>, uint_fast64_t> problematicTransitionVariableResult = createProblematicChoiceVariables(solver, labeledMdp, stateInformation, choiceInformation); - result.problematicTransitionToVariableIndexMap = problematicTransitionVariableResult.first; + std::pair, std::string, PairHash>, uint_fast64_t> problematicTransitionVariableResult = createProblematicChoiceVariables(solver, labeledMdp, stateInformation, choiceInformation); + result.problematicTransitionToVariableMap = problematicTransitionVariableResult.first; result.numberOfVariables += problematicTransitionVariableResult.second; LOG4CPLUS_DEBUG(logger, "Created variables for the problematic choices."); @@ -453,7 +453,7 @@ namespace storm { storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleLiteral(0); for (auto const& choiceVariable : choiceVariableIndices) { - constraint = constraint + storm::expressions::Expression::createDoubleVariable(choiceVariable); + constraint = constraint + storm::expressions::Expression::createIntegerVariable(choiceVariable); } constraint = constraint <= storm::expressions::Expression::createDoubleLiteral(1); @@ -466,9 +466,9 @@ namespace storm { // successor state. storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleLiteral(0); for (auto const& initialStateVariablePair : variableInformation.initialStateToChoiceVariableMap) { - constraint = constraint + storm::expressions::Expression::createDoubleVariable(initialStateVariablePair.second); + constraint = constraint + storm::expressions::Expression::createIntegerVariable(initialStateVariablePair.second); } - constraint = constraint <= storm::expressions::Expression::createDoubleLiteral(1); + constraint = constraint == storm::expressions::Expression::createDoubleLiteral(1); solver.addConstraint("VirtualInitialStateChoosesOneInitialState", constraint); ++numberOfConstraintsCreated; @@ -492,7 +492,7 @@ namespace storm { std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); for (auto state : stateInformation.relevantStates) { - std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin(); + std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin(); for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { for (auto label : choiceLabeling[choice]) { storm::expressions::Expression constraint = storm::expressions::Expression::createIntegerVariable(variableInformation.labelToVariableMap.at(label)) - storm::expressions::Expression::createIntegerVariable(*choiceVariableIterator) >= storm::expressions::Expression::createDoubleLiteral(0); @@ -520,7 +520,7 @@ namespace storm { for (auto state : stateInformation.relevantStates) { storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(variableInformation.stateToProbabilityVariableMap.at(state)); for (auto const& choiceVariable : variableInformation.stateToChoiceVariablesMap.at(state)) { - constraint = constraint - storm::expressions::Expression::createDoubleVariable(choiceVariable); + constraint = constraint - storm::expressions::Expression::createIntegerVariable(choiceVariable); } constraint = constraint <= storm::expressions::Expression::createDoubleLiteral(0); solver.addConstraint("ProbabilityIsZeroIfNoAction" + std::to_string(numberOfConstraintsCreated), constraint); @@ -556,7 +556,7 @@ namespace storm { } } - constraint = constraint + storm::expressions::Expression::createDoubleVariable(*choiceVariableIterator) <= storm::expressions::Expression::createDoubleLiteral(rightHandSide); + constraint = constraint + storm::expressions::Expression::createIntegerVariable(*choiceVariableIterator) <= storm::expressions::Expression::createDoubleLiteral(rightHandSide); solver.addConstraint("ReachabilityProbabilities" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; @@ -566,8 +566,8 @@ namespace storm { // Make sure that the virtual initial state is being assigned the probability from the initial state // that it selected as a successor state. - for (auto const& initialStateVariableIndexPair : variableInformation.initialStateToChoiceVariableIndexMap) { - storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(variableInformation.virtualInitialStateVariable) - storm::expressions::Expression::createDoubleVariable(variableInformation.stateToProbabilityVariableMap.at(initialStateVariableIndexPair.first)) + storm::expressions::Expression::createDoubleVariable(initialStateVariableIndexPair.second) <= storm::expressions::Expression::createDoubleLiteral(1); + for (auto const& initialStateVariablePair : variableInformation.initialStateToChoiceVariableMap) { + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(variableInformation.virtualInitialStateVariable) - storm::expressions::Expression::createDoubleVariable(variableInformation.stateToProbabilityVariableMap.at(initialStateVariablePair.first)) + storm::expressions::Expression::createDoubleVariable(initialStateVariablePair.second) <= storm::expressions::Expression::createDoubleLiteral(1); solver.addConstraint("VirtualInitialStateHasCorrectProbability" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } @@ -590,44 +590,34 @@ namespace storm { for (auto stateListPair : choiceInformation.problematicChoicesForProblematicStates) { for (auto problematicChoice : stateListPair.second) { - std::list::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(stateListPair.first).begin(); + std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(stateListPair.first).begin(); for (auto relevantChoice : choiceInformation.relevantChoicesForRelevantStates.at(stateListPair.first)) { if (relevantChoice == problematicChoice) { break; } - ++choiceVariableIndicesIterator; + ++choiceVariableIterator; } - std::vector variables; - std::vector coefficients; - - variables.push_back(*choiceVariableIndicesIterator); - coefficients.push_back(1); - + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(*choiceVariableIterator); for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) { - variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(stateListPair.first, successorEntry.getColumn()))); - coefficients.push_back(-1); + constraint = constraint - storm::expressions::Expression::createDoubleVariable(variableInformation.problematicTransitionToVariableMap.at(std::make_pair(stateListPair.first, successorEntry.getColumn()))); } + constraint = constraint <= storm::expressions::Expression::createDoubleLiteral(0); - solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS_EQUAL, 0); + solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } } for (auto state : stateInformation.problematicStates) { for (auto problematicChoice : choiceInformation.problematicChoicesForProblematicStates.at(state)) { - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(state)) { - std::vector variables; - std::vector coefficients; - - variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(state)); - coefficients.push_back(1); - variables.push_back(variableInformation.problematicStateToVariableIndexMap.at(successorEntry.getColumn())); - coefficients.push_back(-1); - variables.push_back(variableInformation.problematicTransitionToVariableIndexMap.at(std::make_pair(state, successorEntry.getColumn()))); - coefficients.push_back(1); + for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) { + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(variableInformation.problematicStateToVariableMap.at(state)); + constraint = constraint - storm::expressions::Expression::createDoubleVariable(variableInformation.problematicStateToVariableMap.at(successorEntry.getColumn())); + constraint = constraint + storm::expressions::Expression::createDoubleVariable(variableInformation.problematicTransitionToVariableMap.at(std::make_pair(state, successorEntry.getColumn()))); + constraint = constraint < storm::expressions::Expression::createDoubleLiteral(1); - solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS, 1); + solver.addConstraint("UnproblematicStateReachable" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } } @@ -649,7 +639,8 @@ namespace storm { uint_fast64_t numberOfConstraintsCreated = 0; for (auto label : choiceInformation.knownLabels) { - solver.addConstraint("KnownLabels" + std::to_string(numberOfConstraintsCreated), {variableInformation.labelToVariableIndexMap.at(label)}, {1}, storm::solver::LpSolver::EQUAL, 1); + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(variableInformation.labelToVariableMap.at(label)) == storm::expressions::Expression::createDoubleLiteral(1); + solver.addConstraint("KnownLabels" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } @@ -670,13 +661,11 @@ namespace storm { static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); uint_fast64_t numberOfConstraintsCreated = 0; - std::vector variables; - std::vector coefficients; for (auto state : stateInformation.relevantStates) { // Assert that all states, that select an action, this action either has a non-zero probability to // go to a psi state directly, or in the successor states, at least one action is selected as well. - std::list::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin(); + std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin(); for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { bool psiStateReachableInOneStep = false; for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { @@ -686,38 +675,31 @@ namespace storm { } if (!psiStateReachableInOneStep) { - variables.clear(); - coefficients.clear(); - - variables.push_back(static_cast(*choiceVariableIndicesIterator)); - coefficients.push_back(1); - + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(*choiceVariableIterator); for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { if (state != successorEntry.getColumn() && stateInformation.relevantStates.get(successorEntry.getColumn())) { - std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesIndexMap.at(successorEntry.getColumn()); + std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesMap.at(successorEntry.getColumn()); - for (auto choiceVariableIndex : successorChoiceVariableIndices) { - variables.push_back(choiceVariableIndex); - coefficients.push_back(-1); + for (auto const& choiceVariable : successorChoiceVariableIndices) { + constraint = constraint - storm::expressions::Expression::createDoubleVariable(choiceVariable); } } } + constraint = constraint <= storm::expressions::Expression::createDoubleLiteral(1); - solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS_EQUAL, 1); + solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } - ++choiceVariableIndicesIterator; + ++choiceVariableIterator; } // For all states assert that there is either a selected incoming transition in the subsystem or the // state is the chosen initial state if there is one selected action in the current state. - variables.clear(); - coefficients.clear(); - - for (auto choiceVariableIndex : variableInformation.stateToChoiceVariablesIndexMap.at(state)) { - variables.push_back(choiceVariableIndex); - coefficients.push_back(1); + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleLiteral(0); + + for (auto const& choiceVariable : variableInformation.stateToChoiceVariablesMap.at(state)) { + constraint = constraint + storm::expressions::Expression::createDoubleVariable(choiceVariable); } // Compute the set of predecessors. @@ -734,7 +716,7 @@ namespace storm { continue; } - std::list::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(predecessor).begin(); + std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(predecessor).begin(); for (auto relevantChoice : choiceInformation.relevantChoicesForRelevantStates.at(predecessor)) { bool choiceTargetsCurrentState = false; @@ -748,39 +730,36 @@ namespace storm { // If it does, we can add the choice to the sum. if (choiceTargetsCurrentState) { - variables.push_back(static_cast(*choiceVariableIndicesIterator)); - coefficients.push_back(-1); + constraint = constraint - storm::expressions::Expression::createDoubleVariable(*choiceVariableIterator); } - ++choiceVariableIndicesIterator; + ++choiceVariableIterator; } } // If the current state is an initial state and is selected as a successor state by the virtual // initial state, then this also justifies making a choice in the current state. if (labeledMdp.getLabeledStates("init").get(state)) { - variables.push_back(variableInformation.initialStateToChoiceVariableIndexMap.at(state)); - coefficients.push_back(-1); + constraint = constraint - storm::expressions::Expression::createDoubleVariable(variableInformation.initialStateToChoiceVariableMap.at(state)); } + constraint = constraint <= storm::expressions::Expression::createDoubleLiteral(0); - solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::LESS_EQUAL, 0); + solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } // Assert that at least one initial state selects at least one action. - variables.clear(); - coefficients.clear(); + storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleLiteral(0); for (auto initialState : labeledMdp.getLabeledStates("init")) { - for (auto choiceVariableIndex : variableInformation.stateToChoiceVariablesIndexMap.at(initialState)) { - variables.push_back(choiceVariableIndex); - coefficients.push_back(1); + for (auto const& choiceVariable : variableInformation.stateToChoiceVariablesMap.at(initialState)) { + constraint = constraint + storm::expressions::Expression::createDoubleVariable(choiceVariable); } } - solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::GREATER_EQUAL, 1); + constraint = constraint >= storm::expressions::Expression::createDoubleLiteral(1); + solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; // Add constraints that ensure at least one choice is selected that targets a psi state. - variables.clear(); - coefficients.clear(); + constraint = storm::expressions::Expression::createDoubleLiteral(0); std::unordered_set predecessors; for (auto psiState : psiStates) { // Compute the set of predecessors. @@ -797,7 +776,7 @@ namespace storm { continue; } - std::list::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(predecessor).begin(); + std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(predecessor).begin(); for (auto relevantChoice : choiceInformation.relevantChoicesForRelevantStates.at(predecessor)) { bool choiceTargetsPsiState = false; @@ -811,14 +790,14 @@ namespace storm { // If it does, we can add the choice to the sum. if (choiceTargetsPsiState) { - variables.push_back(*choiceVariableIndicesIterator); - coefficients.push_back(1); + constraint = constraint + storm::expressions::Expression::createDoubleVariable(*choiceVariableIterator); } - ++choiceVariableIndicesIterator; + ++choiceVariableIterator; } } + constraint = constraint >= storm::expressions::Expression::createDoubleLiteral(1); - solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), variables, coefficients, storm::solver::LpSolver::GREATER_EQUAL, 1); + solver.addConstraint("SchedulerCuts" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; return numberOfConstraintsCreated; @@ -875,6 +854,9 @@ namespace storm { LOG4CPLUS_DEBUG(logger, "Asserted scheduler cuts."); } + // Finally, we can tell the solver to incorporate the latest changes. + solver.update(); + LOG4CPLUS_INFO(logger, "Successfully created " << numberOfConstraints << " MILP constraints."); } @@ -887,7 +869,7 @@ namespace storm { static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { boost::container::flat_set result; - for (auto labelVariablePair : variableInformation.labelToVariableIndexMap) { + for (auto const& labelVariablePair : variableInformation.labelToVariableMap) { bool labelTaken = solver.getBinaryValue(labelVariablePair.second); if (labelTaken) { @@ -911,10 +893,10 @@ namespace storm { std::map result; for (auto state : stateInformation.relevantStates) { - std::list::const_iterator choiceVariableIndicesIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin(); + std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesIndexMap.at(state).begin(); for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { - bool choiceTaken = solver.getBinaryValue(*choiceVariableIndicesIterator); - ++choiceVariableIndicesIterator; + bool choiceTaken = solver.getBinaryValue(*choiceVariableIterator); + ++choiceVariableIterator; if (choiceTaken) { result.emplace_hint(result.end(), state, choice); } @@ -933,20 +915,20 @@ namespace storm { */ static std::pair getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::Mdp const& labeledMdp, VariableInformation const& variableInformation) { uint_fast64_t selectedInitialState = 0; - for (auto initialStateVariableIndexPair : variableInformation.initialStateToChoiceVariableIndexMap) { - bool initialStateChosen = solver.getBinaryValue(initialStateVariableIndexPair.second); + for (auto const& initialStateVariablePair : variableInformation.initialStateToChoiceVariableMap) { + bool initialStateChosen = solver.getBinaryValue(initialStateVariablePair.second); if (initialStateChosen) { - selectedInitialState = initialStateVariableIndexPair.first; + selectedInitialState = initialStateVariablePair.first; break; } } - double reachabilityProbability = solver.getContinuousValue(variableInformation.virtualInitialStateVariableIndex); + double reachabilityProbability = solver.getContinuousValue(variableInformation.virtualInitialStateVariable); return std::make_pair(selectedInitialState, reachabilityProbability); } public: - + static boost::container::flat_set getMinimalLabelSet(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabeling()) { diff --git a/src/solver/GlpkLpSolver.h b/src/solver/GlpkLpSolver.h index 1f6d7bd2a..0931e1ca5 100644 --- a/src/solver/GlpkLpSolver.h +++ b/src/solver/GlpkLpSolver.h @@ -68,7 +68,7 @@ namespace storm { virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; // Methods to add binary variables. - virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override; + virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; // Methods to incorporate recent changes. virtual void update() const override; @@ -184,7 +184,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } - virtual uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override { + virtual uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support."; } diff --git a/src/solver/GurobiLpSolver.h b/src/solver/GurobiLpSolver.h index e9eac0e85..90bef47eb 100644 --- a/src/solver/GurobiLpSolver.h +++ b/src/solver/GurobiLpSolver.h @@ -73,7 +73,7 @@ namespace storm { virtual void addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; // Methods to add binary variables. - virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override; + virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override; // Methods to incorporate recent changes. virtual void update() const override; @@ -176,7 +176,7 @@ namespace storm { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } - virtual uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) override { + virtual uint_fast64_t addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override { throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; } diff --git a/src/solver/LpSolver.h b/src/solver/LpSolver.h index 5e7a5f76e..8c729a323 100644 --- a/src/solver/LpSolver.h +++ b/src/solver/LpSolver.h @@ -130,7 +130,7 @@ namespace storm { * @param objectiveFunctionCoefficient The coefficient with which the variable appears in the objective * function. If omitted (or set to zero), the variable is irrelevant for the objective value. */ - virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient) = 0; + virtual void addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) = 0; /*! * Updates the model to make the variables that have been declared since the last call to update