diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index a583142bd..8fd066a00 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -16,7 +16,6 @@ #include "storm/utility/macros.h" #include "storm/utility/vector.h" #include "storm/utility/graph.h" -#include "storm/utility/endComponents.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/UnexpectedException.h" @@ -476,7 +475,7 @@ namespace storm { // Assert reward finitiness for maximizing objectives under all schedulers storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true); - if (storm::utility::endComponents::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck)) { + if (storm::utility::graph::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck)) { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "At least one of the maximizing objectives induces infinite expected reward (or time). This is not supported"); } diff --git a/src/storm/utility/endComponents.h b/src/storm/utility/endComponents.h deleted file mode 100644 index 69b261d88..000000000 --- a/src/storm/utility/endComponents.h +++ /dev/null @@ -1,147 +0,0 @@ -#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 diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index e1b7ca61a..7ff744662 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -103,6 +103,106 @@ namespace storm { return result; } + 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)); + + // 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; + } + } + return false; + } + + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem) { std::vector distances(transitionMatrix.getRowGroupCount()); @@ -1188,6 +1288,8 @@ namespace storm { template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1257,7 +1359,7 @@ namespace storm { template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); - + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1313,7 +1415,9 @@ namespace storm { template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); - + + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); @@ -1363,6 +1467,8 @@ namespace storm { template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1391,12 +1497,10 @@ namespace storm { template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0, boost::optional const& choiceConstraint = boost::none); - template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; @@ -1405,7 +1509,6 @@ namespace storm { template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; - template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index fca059920..9d6911479 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -74,7 +74,20 @@ namespace storm { */ template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); - + + /*! + * 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. + * + * @param transitionMatrix the transition matrix + * @param backwardTransitions The reversed transition relation of the graph structure to search + * @param subsystem the subsystem which we consider + * @param choices the choices which are to be checked + */ + template + bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + /*! * Performs a breadth-first search through the underlying graph structure to compute the distance from all * states to the starting states of the search.