From 2931436201a62da428489ccb6805c4bb384042ef Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 30 Apr 2017 14:46:13 +0200 Subject: [PATCH] added utility functions for end component analysis --- src/storm/utility/endComponents.h | 147 ++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 src/storm/utility/endComponents.h diff --git a/src/storm/utility/endComponents.h b/src/storm/utility/endComponents.h new file mode 100644 index 000000000..69b261d88 --- /dev/null +++ b/src/storm/utility/endComponents.h @@ -0,0 +1,147 @@ +#pragma once + +#include "storm/storage/BitVector.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/utility/graph.h" + +#include "storm/utility/macros.h" + +#include "storm/exceptions/InvalidArgumentException.h" + +#include "storm/utility/Stopwatch.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" + +namespace storm { + namespace utility { + namespace endComponents { + + + // Checks whether there is an End Component that + // 1. contains at least one of the specified choices and + // 2. only contains states given by the specified subsystem. + template + bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices) { + + STORM_LOG_THROW(subsystem.size() == transitionMatrix.getRowGroupCount(), storm::exceptions::InvalidArgumentException, "Invalid size of subsystem"); + STORM_LOG_THROW(choices.size() == transitionMatrix.getRowCount(), storm::exceptions::InvalidArgumentException, "Invalid size of choice vector"); + + if (subsystem.empty() || choices.empty()) { + return false; + } + + storm::storage::BitVector statesWithChoice(transitionMatrix.getRowGroupCount(), false); + uint_fast64_t state = 0; + for (auto const& choice : choices) { + // Get the correct state + while (choice >= transitionMatrix.getRowGroupIndices()[state + 1]) { + ++state; + } + assert(choice >= transitionMatrix.getRowGroupIndices()[state]); + // make sure that the choice originates from the subsystem and also stays within the subsystem + if (subsystem.get(state)) { + bool choiceStaysInSubsys = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (!subsystem.get(entry.getColumn())) { + choiceStaysInSubsys = false; + break; + } + } + if (choiceStaysInSubsys) { + statesWithChoice.set(state, true); + } + } + } + + // Initialize candidate states that satisfy some necessary conditions for being part of an EC with a specified choice: + + // Get the states for which a policy can enforce that a choice is reached while staying inside the subsystem + storm::storage::BitVector candidateStates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, subsystem, statesWithChoice); + + // Only keep the states that can stay in the set of candidates forever + candidateStates = storm::utility::graph::performProb0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, ~candidateStates); + + // Only keep the states that can be reached after performing one of the specified choices + statesWithChoice &= candidateStates; + storm::storage::BitVector choiceTargets(transitionMatrix.getRowGroupCount(), false); + for (auto const& state : statesWithChoice) { + for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { + bool choiceStaysInCandidateSet = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (!candidateStates.get(entry.getColumn())) { + choiceStaysInCandidateSet = false; + break; + } + } + if (choiceStaysInCandidateSet) { + for (auto const& entry : transitionMatrix.getRow(choice)) { + choiceTargets.set(entry.getColumn(), true); + } + } + } + } + candidateStates = storm::utility::graph::getReachableStates(transitionMatrix, choiceTargets, candidateStates, storm::storage::BitVector(candidateStates.size(), false)); + + storm::utility::Stopwatch fixPointSw(true); + // At this point we know that every candidate state can reach a choice at least once without leaving the set of candidate states. + // We now compute the states that can reach a choice at least twice, three times, four times, ... until a fixpoint is reached. + while (!candidateStates.empty()) { + // Update the states with a choice that stays within the set of candidates + statesWithChoice &= candidateStates; + for (auto const& state : statesWithChoice) { + bool stateHasChoice = false; + for (uint_fast64_t choice = choices.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state]); choice < transitionMatrix.getRowGroupIndices()[state + 1]; choice = choices.getNextSetIndex(choice + 1)) { + bool choiceStaysInCandidateSet = true; + for (auto const& entry : transitionMatrix.getRow(choice)) { + if (!candidateStates.get(entry.getColumn())) { + choiceStaysInCandidateSet = false; + break; + } + } + if (choiceStaysInCandidateSet) { + stateHasChoice = true; + break; + } + } + if (!stateHasChoice) { + statesWithChoice.set(state, false); + } + } + + // Update the candidates + storm::storage::BitVector newCandidates = storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, candidateStates, statesWithChoice); + + // Check if conferged + if (newCandidates == candidateStates) { + assert(!candidateStates.empty()); + // return true; + break; + } + } + // return false; + + fixPointSw.stop(); + bool result = !candidateStates.empty(); + + storm::utility::Stopwatch ecDecompSw(true); + bool otherresult = false; + auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition(transitionMatrix, backwardTransitions, candidateStates); + for (auto& mec : mecDecomposition) { + for (auto const& stateActionsPair : mec) { + for (auto const& action : stateActionsPair.second) { + if (choices.get(action)) { + otherresult = true; + break; + } + } + } + } + + STORM_LOG_THROW(result == otherresult, storm::exceptions::InvalidArgumentException, "Wrong result! Fixpoint says " << result << " mec says differently"); + ecDecompSw.stop(); + std::cout << "EC check: Fixpoint took " << fixPointSw << " seconds and MEC took " << ecDecompSw << " seconds." << std::endl; + return result; + + } + } + } +} \ No newline at end of file