From b36b460a4e4f54db44e2327f9d7c891d98248c19 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Jun 2013 10:28:59 +0200 Subject: [PATCH] Added some comments to scheduler guessing. Former-commit-id: 6a256210a35f470d3d2e03de35b1dbf3810cf7d0 --- .../prctl/SparseMdpPrctlModelChecker.h | 138 +++++++----------- src/utility/graph.h | 56 ++++--- 2 files changed, 83 insertions(+), 111 deletions(-) diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 3c04bcfbe..b5a474129 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -288,8 +288,6 @@ namespace storm { // Create resulting vector. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - std::vector guessedScheduler; - // Check whether we need to compute exact probabilities for some states. if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) { if (qualitative) { @@ -316,7 +314,7 @@ namespace storm { std::vector b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, submatrix.getRowCount()); // Create vector for results for maybe states. - std::vector x = this->getInitialValueIterationValues(minimize, submatrix, subNondeterministicChoiceIndices, b, statesWithProbability1, maybeStates, &guessedScheduler); + std::vector x = this->getInitialValueIterationValues(minimize, submatrix, subNondeterministicChoiceIndices, b, statesWithProbability1, maybeStates); // Solve the corresponding system of equations. if (linearEquationSolver != nullptr) { @@ -332,45 +330,7 @@ namespace storm { // Set values of resulting vector that are known exactly. storm::utility::vector::setVectorValues(*result, statesWithProbability0, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(*result, statesWithProbability1, storm::utility::constGetOne()); - - // Output a scheduler for debug purposes. - std::vector myScheduler(this->getModel().getNumberOfStates()); - this->computeTakenChoices(this->minimumOperatorStack.top(), false, *result, myScheduler, this->getModel().getNondeterministicChoiceIndices()); - - std::vector stateColoring(this->getModel().getNumberOfStates()); - for (auto target : statesWithProbability1) { - stateColoring[target] = 1; - } - - std::vector colors(2); - colors[0] = "white"; - colors[1] = "blue"; - - std::ofstream outFile; - outFile.open("real.dot"); - storm::storage::BitVector filterStates(this->getModel().getNumberOfStates(), true); - this->getModel().writeDotToStream(outFile, true, &filterStates, result, nullptr, &stateColoring, &colors, &myScheduler); - outFile.close(); - - std::cout << "=========== Scheduler Comparison ===========" << std::endl; - uint_fast64_t index = 0; - for (auto state : maybeStates) { - if (myScheduler[state] != guessedScheduler[index]) { - std::cout << state << " right: " << myScheduler[state] << ", wrong: " << guessedScheduler[index] << std::endl; - std::cout << "Correct: " << std::endl; - typename storm::storage::SparseMatrix::Rows correctRow = this->getModel().getTransitionMatrix().getRow(this->getModel().getNondeterministicChoiceIndices()[state] + myScheduler[state]); - for (auto& transition : correctRow) { - std::cout << "target " << transition.column() << " with prob " << transition.value() << std::endl; - } - std::cout << "Incorrect: " << std::endl; - typename storm::storage::SparseMatrix::Rows incorrectRow = this->getModel().getTransitionMatrix().getRow(this->getModel().getNondeterministicChoiceIndices()[state] + myScheduler[state]); - for (auto& transition : incorrectRow) { - std::cout << "target " << transition.column() << " with prob " << transition.value() << std::endl; - } - } - ++index; - } - + // If we were required to generate a scheduler, do so now. if (scheduler != nullptr) { this->computeTakenChoices(this->minimumOperatorStack.top(), false, *result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); @@ -580,20 +540,6 @@ namespace storm { storm::utility::vector::setVectorValues(*result, *targetStates, storm::utility::constGetZero()); storm::utility::vector::setVectorValues(*result, infinityStates, storm::utility::constGetInfinity()); -// std::vector myScheduler(this->getModel().getNumberOfStates()); -// this->computeTakenChoices(this->minimumOperatorStack.top(), true, *result, myScheduler, this->getModel().getNondeterministicChoiceIndices()); -// -// std::vector stateColoring(this->getModel().getNumberOfStates()); -// for (auto target : *targetStates) { -// stateColoring[target] = 1; -// } -// -// std::vector colors(2); -// colors[0] = "white"; -// colors[1] = "blue"; -// -// this->getModel().writeDotToStream(std::cout, true, storm::storage::BitVector(this->getModel().getNumberOfStates(), true), result, nullptr, &stateColoring, &colors, &myScheduler); - // If we were required to generate a scheduler, do so now. if (scheduler != nullptr) { this->computeTakenChoices(this->minimumOperatorStack.top(), true, *result, *scheduler, this->getModel().getNondeterministicChoiceIndices()); @@ -684,41 +630,43 @@ namespace storm { * Retrieves the values to be used as the initial values for the value iteration techniques. * * @param submatrix The matrix that will be used for value iteration later. + * @param subNondeterministicChoiceIndices A vector indicating which rows represent the nondeterministic choices + * of which state in the system that will be used for value iteration. + * @param rightHandSide The right-hand-side of the equation system used for value iteration. + * @param targetStates A set of target states that is to be reached. + * @param maybeStates A set of states that was selected as the system on which to perform value iteration. + * @param guessedScheduler If not the nullptr, this vector will be filled with the scheduler that was + * derived as a preliminary guess. + * @param distancePairs If not the nullptr, this pair of vectors contains the minimal path distances from + * each state to a target state and a non-target state, respectively. + * @return The initial values to be used for the value iteration for the given system. */ std::vector getInitialValueIterationValues(bool minimize, storm::storage::SparseMatrix const& submatrix, std::vector const& subNondeterministicChoiceIndices, std::vector const& rightHandSide, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& maybeStates, - std::vector* guessedScheduler = nullptr) const { + std::vector* guessedScheduler = nullptr, + std::pair, std::vector>* distancePairs = nullptr) const { storm::settings::Settings* s = storm::settings::instance(); double precision = s->get("precision"); if (s->get("use-heuristic-presolve")) { - std::pair, std::vector> distancesAndPredecessorsPair = storm::utility::graph::performDijkstra(this->getModel(), - this->getModel().template getBackwardTransitions([](Type const& value) -> Type { return value; }), - minimize ? ~(maybeStates | targetStates) : targetStates, &maybeStates); + // Compute both the most probable paths to target states as well as the most probable path to non-target states. + // Note that here target state means a state does not *not* satisfy the property that is to be reached + // if we want to minimize the reachability probability. + std::pair, std::vector> maxDistancesAndPredecessorsPairToTarget = storm::utility::graph::performDijkstra(this->getModel(), + this->getModel().template getBackwardTransitions([](Type const& value) -> Type { return value; }), + minimize ? ~(maybeStates | targetStates) : targetStates, &maybeStates); - std::pair, std::vector> distancesAndPredecessorsPair2 = storm::utility::graph::performDijkstra(this->getModel(), - this->getModel().template getBackwardTransitions([](Type const& value) -> Type { return value; }), - minimize ? targetStates : ~(maybeStates | targetStates), &maybeStates); - - std::vector scheduler = this->convertShortestPathsToScheduler(false, maybeStates, distancesAndPredecessorsPair.first, distancesAndPredecessorsPair.second); - - std::vector stateColoring(this->getModel().getNumberOfStates()); - for (auto target : targetStates) { - stateColoring[target] = 1; - } + std::pair, std::vector> maxDistancesAndPredecessorsPairToNonTarget = storm::utility::graph::performDijkstra(this->getModel(), + this->getModel().template getBackwardTransitions([](Type const& value) -> Type { return value; }), + minimize ? targetStates : ~(maybeStates | targetStates), &maybeStates); - std::vector colors(2); - colors[0] = "white"; - colors[1] = "blue"; - - std::ofstream outFile; - outFile.open("guessed.dot"); - storm::storage::BitVector filterStates(this->getModel().getNumberOfStates(), true); - this->getModel().writeDotToStream(outFile, true, &filterStates, &distancesAndPredecessorsPair.first, &distancesAndPredecessorsPair2.first, &stateColoring, &colors); - outFile.close(); + // Now guess the scheduler that could possibly maximize the probability of reaching the target states. + std::vector scheduler = this->getSchedulerGuess(maybeStates, maxDistancesAndPredecessorsPairToTarget.first, maxDistancesAndPredecessorsPairToNonTarget.first); + // Now that we have a guessed scheduler, we can compute the reachability probability of the system + // under the given scheduler and take these values as the starting point for value iteration. std::vector result(scheduler.size(), Type(0.5)); std::vector b(scheduler.size()); storm::utility::vector::selectVectorValues(b, scheduler, subNondeterministicChoiceIndices, rightHandSide); @@ -735,38 +683,52 @@ namespace storm { } } + // If some of the parameters were given, we fill them with the information that they are supposed + // to contain. if (guessedScheduler != nullptr) { *guessedScheduler = std::move(scheduler); } + if (distancePairs != nullptr) { + distancePairs->first = std::move(maxDistancesAndPredecessorsPairToTarget.first); + distancePairs->second = std::move(maxDistancesAndPredecessorsPairToNonTarget.first); + } return result; } else { + // If guessing a scheduler was not requested, we just return the constant zero vector as the + // starting point for value iteration. return std::vector(submatrix.getColumnCount()); } } - std::vector convertShortestPathsToScheduler(bool minimize, storm::storage::BitVector const& maybeStates, std::vector const& distances, std::vector const& shortestPathSuccessors) const { + /*! + * Guesses a scheduler that possibly maximizes the probabiliy of reaching the target states. + * + * @param maybeStates The states for which the scheduler needs to resolve the nondeterminism. + * @param distancesToTarget Contains the minimal distance of reaching a target state for each state. + * @param distancesToNonTarget Contains the minimal distance of reaching a non-target state for each state. + * @return The scheduler that was guessed based on the given distance information. + */ + std::vector getSchedulerGuess(storm::storage::BitVector const& maybeStates, std::vector const& distancesToTarget, std::vector const& distancesToNonTarget) const { std::vector scheduler(maybeStates.getNumberOfSetBits()); - Type extremalProbability = minimize ? 1 : 0; + // For each of the states we need to resolve the nondeterministic choice based on the information we are given. + Type maxProbability = 0; Type currentProbability = 0; uint_fast64_t currentStateIndex = 0; for (auto state : maybeStates) { - extremalProbability = minimize ? 1 : 0; + maxProbability = 0; for (uint_fast64_t row = 0, rowEnd = this->getModel().getNondeterministicChoiceIndices()[state + 1] - this->getModel().getNondeterministicChoiceIndices()[state]; row < rowEnd; ++row) { typename storm::storage::SparseMatrix::Rows currentRow = this->getModel().getTransitionMatrix().getRow(this->getModel().getNondeterministicChoiceIndices()[state] + row); currentProbability = 0; for (auto& transition : currentRow) { - currentProbability += transition.value() * (1 / std::exp(distances[transition.column()])); + currentProbability += transition.value() * distancesToTarget[transition.column()]; } - if (minimize && currentProbability < extremalProbability) { - extremalProbability = currentProbability; - scheduler[currentStateIndex] = row; - } else if (!minimize && currentProbability > extremalProbability) { - extremalProbability = currentProbability; + if (currentProbability < maxProbability) { + maxProbability = currentProbability; scheduler[currentStateIndex] = row; } } diff --git a/src/utility/graph.h b/src/utility/graph.h index 9d79f72ed..6f5ab401f 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -618,7 +618,7 @@ namespace graph { // If the current state is the root of a SCC, we need to pop all states of the SCC from // the algorithm's stack. if (lowlinks[currentState] == stateIndices[currentState]) { - stronglyConnectedComponents.push_back(std::vector()); + stronglyConnectedComponents.emplace_back(); uint_fast64_t lastState = 0; do { @@ -761,6 +761,9 @@ namespace graph { return topologicalSort; } + /*! + * A class needed to compare the distances for two states in the Dijkstra search. + */ template struct DistanceCompare { bool operator()(std::pair const& lhs, std::pair const& rhs) const { @@ -768,62 +771,69 @@ namespace graph { } }; + /*! + * Performs a Dijkstra search from the given starting states to determine the most probable paths to all other states + * by only passing through the given state set. + * + * @param model The model whose state space is to be searched. + * @param transitions The transitions wrt to which to compute the most probable paths. + * @param startingStates The starting states of the Dijkstra search. + * @param filterStates A set of states that must not be left on any path. + */ template std::pair, std::vector> performDijkstra(storm::models::AbstractModel const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, -// FIXME: The case in which there are target states given should be handled properly. -// storm::storage::BitVector* targetStates = nullptr, storm::storage::BitVector const* filterStates = nullptr) { LOG4CPLUS_INFO(logger, "Performing Dijkstra search."); - const uint_fast64_t noPredecessorValue = std::numeric_limits::max(); - std::vector distances(model.getNumberOfStates(), storm::utility::constGetInfinity()); + const uint_fast64_t noPredecessorValue = storm::utility::constGetZero(); + std::vector probabilities(model.getNumberOfStates(), storm::utility::constGetZero()); std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); - // Set the distance to 0 for all starting states. - std::set, DistanceCompare> distanceStateSet; + // Set the probability to 1 for all starting states. + std::set, DistanceCompare> probabilityStateSet; for (auto state : startingStates) { - distanceStateSet.emplace(storm::utility::constGetZero(), state); - distances[state] = 0; + probabilityStateSet.emplace(storm::utility::constGetZero(), state); + probabilities[state] = 1; } - while (!distanceStateSet.empty()) { + // As long as there is one reachable state, we need to consider it. + while (!probabilityStateSet.empty()) { // Get the state with the least distance from the set and remove it. - std::pair distanceStatePair = *distanceStateSet.begin(); - distanceStateSet.erase(distanceStateSet.begin()); + std::pair probabilityStatePair = *probabilityStateSet.begin(); + probabilityStateSet.erase(probabilityStateSet.begin()); // Now check the new distances for all successors of the current state. - typename storm::storage::SparseMatrix::Rows row = transitions.getRows(distanceStatePair.second, distanceStatePair.second); + typename storm::storage::SparseMatrix::Rows row = transitions.getRows(probabilityStatePair.second, probabilityStatePair.second); for (auto& transition : row) { // Only follow the transition if it lies within the filtered states. if (filterStates != nullptr && filterStates->get(transition.column())) { // Calculate the distance we achieve when we take the path to the successor via the current state. - T newDistance = distanceStatePair.first + std::log(storm::utility::constGetOne() / transition.value()); + T newDistance = probabilityStatePair.first * transition.value(); // We found a cheaper way to get to the target state of the transition. - if (newDistance < distances[transition.column()]) { + if (newDistance > probabilities[transition.column()]) { // Remove the old distance. - if (distances[transition.column()] != noPredecessorValue) { - distanceStateSet.erase(std::make_pair(distances[transition.column()], transition.column())); + if (probabilities[transition.column()] != noPredecessorValue) { + probabilityStateSet.erase(std::make_pair(probabilities[transition.column()], transition.column())); } // Set and add the new distance. - distances[transition.column()] = newDistance; - predecessors[transition.column()] = distanceStatePair.second; - distanceStateSet.insert(std::make_pair(newDistance, transition.column())); + probabilities[transition.column()] = newDistance; + predecessors[transition.column()] = probabilityStatePair.second; + probabilityStateSet.insert(std::make_pair(newDistance, transition.column())); } } } } + // Move the values into the result and return it. std::pair, std::vector> result; - result.first = std::move(distances); + result.first = std::move(probabilities); result.second = std::move(predecessors); - LOG4CPLUS_INFO(logger, "Done performing Dijkstra search."); - return result; }