Moved static analysis for guaranteed label set computation into utilities and improved MILP-based approach by using this information.

Former-commit-id: 611867288a

counterexamples.h

@@ -1,21 +0,0 @@
-/*
- * vector.h
- *
- *  Created on: 06.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_UTILITY_COUNTEREXAMPLE_H_
-#define STORM_UTILITY_COUNTEREXAMPLE_H_
-
-namespace storm {
-    namespace utility {
-        namespace counterexample{
-            
-            
-            
-        } // namespace counterexample
-    } // namespace utility
-} // namespace storm
-
-#endif /* STORM_UTILITY_COUNTEREXAMPLE_H_ */

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -24,6 +24,8 @@ extern "C" {
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidStateException.h"
 
+#include "src/utility/counterexamples.h"
+
 namespace storm {
     namespace counterexamples {
         
@@ -63,7 +65,7 @@ namespace storm {
             struct ChoiceInformation {
                 std::unordered_map<uint_fast64_t, std::list<uint_fast64_t>> relevantChoicesForRelevantStates;
                 std::unordered_map<uint_fast64_t, std::list<uint_fast64_t>> problematicChoicesForProblematicStates;
-                std::unordered_set<uint_fast64_t> allRelevantLabels;
+                std::set<uint_fast64_t> allRelevantLabels;
             };
 
             /*!
@@ -279,7 +281,7 @@ namespace storm {
              * variables, this value is increased.
              * @return A mapping from labels to variable indices.
              */
-            static std::unordered_map<uint_fast64_t, uint_fast64_t> createLabelVariables(GRBenv* env, GRBmodel* model, std::unordered_set<uint_fast64_t> const& relevantLabels, uint_fast64_t& nextFreeVariableIndex) {
+            static std::unordered_map<uint_fast64_t, uint_fast64_t> createLabelVariables(GRBenv* env, GRBmodel* model, std::set<uint_fast64_t> const& relevantLabels, uint_fast64_t& nextFreeVariableIndex) {
                 int error = 0;
                 std::stringstream variableNameBuffer;
                 std::unordered_map<uint_fast64_t, uint_fast64_t> resultingMap;
@@ -851,6 +853,37 @@ namespace storm {
                 return numberOfConstraintsCreated;
             }
             
+            /*
+             * Asserts that labels that are on all paths from initial to target states are definitely taken.
+             *
+             * @param env The Gurobi environment.
+             * @param model The Gurobi model.
+             * @param labeledMdp The labeled MDP.
+             * @param psiStates A bit vector characterizing the psi 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.
+             * @return The total number of constraints that were created.
+             */
+            static uint_fast64_t assertKnownLabels(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) {
+                uint_fast64_t numberOfConstraintsCreated = 0;
+                int error = 0;
+
+                std::set<uint_fast64_t> knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, choiceInformation.allRelevantLabels);
+                for (auto label : knownLabels) {
+                    double coefficient = 1;
+                    int variableIndex = variableInformation.labelToVariableIndexMap.at(label);
+                    
+                    error = GRBaddconstr(model, 1, &variableIndex, &coefficient, 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) << ").";
+                    }
+                    ++numberOfConstraintsCreated;
+                }
+
+                return numberOfConstraintsCreated;
+            }
+            
             /*!
              * Asserts constraints that rule out many suboptimal policies.
              *
@@ -1068,6 +1101,10 @@ namespace storm {
                 numberOfConstraints += assertUnproblematicStateReachable(env, model, labeledMdp, stateInformation, choiceInformation, variableInformation);
                 LOG4CPLUS_DEBUG(logger, "Asserted that unproblematic state reachable from problematic states.");
 
+                // Add constraints that express that certain labels are already known to be taken.
+                numberOfConstraints += assertKnownLabels(env, model, labeledMdp, psiStates, choiceInformation, variableInformation);
+                LOG4CPLUS_DEBUG(logger, "Asserted known labels are taken.");
+                
                 // If required, assert additional constraints that reduce the number of possible policies.
                 if (includeSchedulerCuts) {
                     numberOfConstraints += assertSchedulerCuts(env, model, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation);

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -23,6 +23,7 @@
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 
+#include "src/utility/counterexamples.h"
 #include "src/utility/IRUtility.h"
 
 namespace storm {
@@ -285,68 +286,11 @@ namespace storm {
                         assertDisjunction(context, solver, formulae);
                     }
                 }
-                
-                // Now we compute the set of labels that is present on all paths from the initial to the target states.
-                std::vector<std::set<uint_fast64_t>> analysisInformation(labeledMdp.getNumberOfStates(), relevancyInformation.relevantLabels);
-                std::queue<std::pair<uint_fast64_t, uint_fast64_t>> worklist;
-                
-                // Initially, put all predecessors of target states in the worklist and empty the analysis information
-                // them.
-                for (auto state : psiStates) {
-                    analysisInformation[state] = std::set<uint_fast64_t>();
-                    for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(state), predecessorIte = backwardTransitions.constColumnIteratorEnd(state); predecessorIt != predecessorIte; ++predecessorIt) {
-                        if (relevancyInformation.relevantStates.get(*predecessorIt)) {
-                            worklist.push(std::make_pair(*predecessorIt, state));
-                        }
-                    }
-                }
-                
-                // Iterate as long as the worklist is non-empty.
-                while (!worklist.empty()) {
-                    std::pair<uint_fast64_t, uint_fast64_t> const& currentStateTargetStatePair = worklist.front();
-                    uint_fast64_t currentState = currentStateTargetStatePair.first;
-                    uint_fast64_t targetState = currentStateTargetStatePair.second;
-                    
-                    // Iterate over the successor states for all choices and compute new analysis information.
-                    std::set<uint_fast64_t> intersection;
-                    for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) {
-                        for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
-                            // 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 labels.
-                            if (*successorIt == targetState) {
-                                std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[targetState].begin(), analysisInformation[targetState].end(), std::inserter(intersection, intersection.begin()));
-                                
-                                std::set<uint_fast64_t> choiceLabelIntersection;
-                                std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(intersection, intersection.begin()));
-                            }
-                        }
-                    }
-
-                    // If the analysis information changed, we need to update it and put all the predecessors of this
-                    // state in the worklist.
-                    if (analysisInformation[currentState] != intersection) {
-                        analysisInformation[currentState] = std::move(intersection);
-                        
-                        for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
-                            worklist.push(std::make_pair(*predecessorIt, currentState));
-                        }
-                    }
-
-                
-                    worklist.pop();
-                }
-
-                // Now build the intersection over the analysis information of all initial states.
-                std::set<uint_fast64_t> knownLabels(relevancyInformation.relevantLabels);
-                std::set<uint_fast64_t> tempIntersection;
-                for (auto initialState : labeledMdp.getInitialStates()) {
-                    std::set_intersection(knownLabels.begin(), knownLabels.end(), analysisInformation[initialState].begin(), analysisInformation[initialState].end(), std::inserter(tempIntersection, tempIntersection.begin()));
-                    std::swap(knownLabels, tempIntersection);
-                    tempIntersection.clear();
-                }
 
+                // Also, we can assert that all labels that are encountered along all paths from an initial to a target
+                // state are taken.
                 formulae.clear();
+                std::set<uint_fast64_t> knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, relevancyInformation.relevantLabels);
                 for (auto label : knownLabels) {
                     formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
                 }
@@ -858,6 +802,7 @@ namespace storm {
                     }
                     ++iterations;
                 } while (!done);
+                LOG4CPLUS_ERROR(logger, "Found minimal label set after " << iterations << " iterations.");
                 
                 // (8) Return the resulting command set after undefining the constants.
                 storm::utility::ir::undefineUndefinedConstants(program);

src/utility/counterexamples.h

@@ -0,0 +1,97 @@
+/*
+ * vector.h
+ *
+ *  Created on: 06.12.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_UTILITY_COUNTEREXAMPLE_H_
+#define STORM_UTILITY_COUNTEREXAMPLE_H_
+
+#include <queue>
+
+namespace storm {
+    namespace utility {
+        namespace counterexamples {
+            
+            /*!
+             * Computes a set of action labels that is visited along all paths from an initial to a target state.
+             *
+             * @return The set of action labels that is visited on all paths from an initial to a target state.
+             */
+            template <typename T>
+            std::set<uint_fast64_t> getGuaranteedLabelSet(storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, std::set<uint_fast64_t> const& relevantLabels) {
+                // Get some data from the MDP for convenient access.
+                storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
+                std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices();
+                std::vector<std::set<uint_fast64_t>> const& choiceLabeling = labeledMdp.getChoiceLabeling();
+                storm::storage::SparseMatrix<bool> backwardTransitions = labeledMdp.getBackwardTransitions();
+
+                // Now we compute the set of labels that is present on all paths from the initial to the target states.
+                std::vector<std::set<uint_fast64_t>> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels);
+                std::queue<std::pair<uint_fast64_t, uint_fast64_t>> worklist;
+                
+                // Initially, put all predecessors of target states in the worklist and empty the analysis information
+                // them.
+                for (auto state : psiStates) {
+                    analysisInformation[state] = std::set<uint_fast64_t>();
+                    for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(state), predecessorIte = backwardTransitions.constColumnIteratorEnd(state); predecessorIt != predecessorIte; ++predecessorIt) {
+                        if (*predecessorIt != state) {
+                            worklist.push(std::make_pair(*predecessorIt, state));
+                        }
+                    }
+                }
+                
+                // Iterate as long as the worklist is non-empty.
+                while (!worklist.empty()) {
+                    std::pair<uint_fast64_t, uint_fast64_t> const& currentStateTargetStatePair = worklist.front();
+                    uint_fast64_t currentState = currentStateTargetStatePair.first;
+                    uint_fast64_t targetState = currentStateTargetStatePair.second;
+                    
+                    // Iterate over the successor states for all choices and compute new analysis information.
+                    std::set<uint_fast64_t> intersection;
+                    for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) {
+                        for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator successorIt = transitionMatrix.constColumnIteratorBegin(currentChoice), successorIte = transitionMatrix.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) {
+                            // 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 labels.
+                            if (*successorIt == targetState) {
+                                std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[targetState].begin(), analysisInformation[targetState].end(), std::inserter(intersection, intersection.begin()));
+                                
+                                std::set<uint_fast64_t> choiceLabelIntersection;
+                                std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(intersection, intersection.begin()));
+                            }
+                        }
+                    }
+                    
+                    // If the analysis information changed, we need to update it and put all the predecessors of this
+                    // state in the worklist.
+                    if (analysisInformation[currentState] != intersection) {
+                        analysisInformation[currentState] = std::move(intersection);
+                        
+                        for (typename storm::storage::SparseMatrix<T>::ConstIndexIterator predecessorIt = backwardTransitions.constColumnIteratorBegin(currentState), predecessorIte = backwardTransitions.constColumnIteratorEnd(currentState); predecessorIt != predecessorIte; ++predecessorIt) {
+                            worklist.push(std::make_pair(*predecessorIt, currentState));
+                        }
+                    }
+                    
+                    
+                    worklist.pop();
+                }
+                
+                // Now build the intersection over the analysis information of all initial states.
+                std::set<uint_fast64_t> knownLabels(relevantLabels);
+                std::set<uint_fast64_t> tempIntersection;
+                for (auto initialState : labeledMdp.getInitialStates()) {
+                    std::set_intersection(knownLabels.begin(), knownLabels.end(), analysisInformation[initialState].begin(), analysisInformation[initialState].end(), std::inserter(tempIntersection, tempIntersection.begin()));
+                    std::swap(knownLabels, tempIntersection);
+                    tempIntersection.clear();
+                }
+
+                return knownLabels;
+            }
+            
+        } // namespace counterexample
+    } // namespace utility
+} // namespace storm
+
+#endif /* STORM_UTILITY_COUNTEREXAMPLE_H_ */