From 57b6208eee6fe4830167d2e2dace44d7db4548b1 Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 10 Feb 2014 00:42:59 +0100 Subject: [PATCH] Added a pseudo model which can be constructed from only a matrix to look and behave like a model for use in Decomposition classes Former-commit-id: f8fdc5a9b636837f60db1c57dfec2b2b405f421b --- ...ogicalValueIterationMdpPrctlModelChecker.h | 2 +- src/models/PseudoModel.cpp | 108 ++++++++++++++++++ src/models/PseudoModel.h | 90 +++++++++++++++ .../NondeterministicLinearEquationSolver.h | 2 +- ...onNondeterministicLinearEquationSolver.cpp | 105 ++++------------- ...ionNondeterministicLinearEquationSolver.h} | 3 +- src/storage/Decomposition.h | 5 +- ...tronglyConnectedComponentDecomposition.cpp | 37 ++++-- .../StronglyConnectedComponentDecomposition.h | 55 +++++++-- 9 files changed, 304 insertions(+), 103 deletions(-) create mode 100644 src/models/PseudoModel.cpp create mode 100644 src/models/PseudoModel.h rename src/solver/{TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h => TopologicalValueIterationNondeterministicLinearEquationSolver.h} (94%) diff --git a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h index 84bc1764d..750d068c8 100644 --- a/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h @@ -68,7 +68,7 @@ private: bool relative = s->getOptionByLongName("relative").getArgument(0).getValueAsBoolean(); // Now, we need to determine the SCCs of the MDP and a topological sort. - std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); diff --git a/src/models/PseudoModel.cpp b/src/models/PseudoModel.cpp new file mode 100644 index 000000000..37749a873 --- /dev/null +++ b/src/models/PseudoModel.cpp @@ -0,0 +1,108 @@ +#include "src/models/PseudoModel.h" +#include "src/utility/constants.h" +#include "src/models/AbstractModel.h" + +namespace storm { + namespace models { + + template + ModelBasedPseudoModel::ModelBasedPseudoModel(storm::models::AbstractModel const& model) : _model(model) { + // Intentionally left empty. + } + + template + NonDeterministicMatrixBasedPseudoModel::NonDeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix const& matrix, std::vector const& nondeterministicChoiceIndices) : _matrix(matrix), _nondeterministicChoiceIndices(nondeterministicChoiceIndices) { + // Intentionally left empty. + } + + template + DeterministicMatrixBasedPseudoModel::DeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix const& matrix) : _matrix(matrix) { + // Intentionally left empty. + } + + template + typename storm::storage::SparseMatrix::const_rows + ModelBasedPseudoModel::getRows(uint_fast64_t state) const { + return this->_model.getRows(state); + } + + template + typename storm::storage::SparseMatrix::const_rows + NonDeterministicMatrixBasedPseudoModel::getRows(uint_fast64_t state) const { + return this->_matrix.getRows(this->_nondeterministicChoiceIndices[state], this->_nondeterministicChoiceIndices[state + 1] - 1); + } + + template + typename storm::storage::SparseMatrix::const_rows + DeterministicMatrixBasedPseudoModel::getRows(uint_fast64_t state) const { + return this->_matrix.getRows(state, state); + } + + template + uint_fast64_t + ModelBasedPseudoModel::getNumberOfStates() const { + return this->_model.getNumberOfStates(); + } + + template + uint_fast64_t + NonDeterministicMatrixBasedPseudoModel::getNumberOfStates() const { + return this->_matrix.getColumnCount(); + } + + template + uint_fast64_t + DeterministicMatrixBasedPseudoModel::getNumberOfStates() const { + return this->_matrix.getColumnCount(); + } + + template + storm::storage::SparseMatrix + AbstractPseudoModel::extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const { + uint_fast64_t numberOfStates = decomposition.size(); + + // First, we need to create a mapping of states to their SCC index, to ease the computation of dependency transitions later. + std::vector stateToBlockMap(this->getNumberOfStates()); + for (uint_fast64_t i = 0; i < decomposition.size(); ++i) { + for (auto state : decomposition[i]) { + stateToBlockMap[state] = i; + } + } + + // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. + storm::storage::SparseMatrixBuilder dependencyGraphBuilder(numberOfStates, numberOfStates); + + for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) { + // Get the next block. + typename storm::storage::StateBlock const& block = decomposition[currentBlockIndex]; + + // Now, we determine the blocks which are reachable (in one step) from the current block. + boost::container::flat_set allTargetBlocks; + for (auto state : block) { + for (auto const& transitionEntry : this->getRows(state)) { + uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.first]; + + // We only need to consider transitions that are actually leaving the SCC. + if (targetBlock != currentBlockIndex) { + allTargetBlocks.insert(targetBlock); + } + } + } + + // Now we can just enumerate all the target SCCs and insert the corresponding transitions. + for (auto targetBlock : allTargetBlocks) { + dependencyGraphBuilder.addNextValue(currentBlockIndex, targetBlock, storm::utility::constantOne()); + } + } + + return dependencyGraphBuilder.build(); + } + + template class ModelBasedPseudoModel; + template class NonDeterministicMatrixBasedPseudoModel; + template class DeterministicMatrixBasedPseudoModel; + template class ModelBasedPseudoModel; + template class NonDeterministicMatrixBasedPseudoModel; + template class DeterministicMatrixBasedPseudoModel; + } // namespace models +} // namespace storm \ No newline at end of file diff --git a/src/models/PseudoModel.h b/src/models/PseudoModel.h new file mode 100644 index 000000000..6d3fd38da --- /dev/null +++ b/src/models/PseudoModel.h @@ -0,0 +1,90 @@ +#ifndef STORM_MODELS_PSEUDOMODEL_H_ +#define STORM_MODELS_PSEUDOMODEL_H_ + +#include +#include "src/storage/SparseMatrix.h" +#include "src/storage/Decomposition.h" + +namespace storm { + namespace models { + // Forward declare the abstract model class. + template class AbstractModel; + + /*! + * This classes encapsulate the model/transitionmatrix on which the SCC decomposition is performed. + * The Abstract Base class is specialized by the two possible representations: + * - For a model the implementation ModelBasedPseudoModel hands the call to getRows() through to the model + * - For a matrix of a nondeterministic model the implementation NonDeterministicMatrixBasedPseudoModel emulates the call + * on the matrix itself like the model function would + * - For a matrix of a deterministic model the implementation DeterministicMatrixBasedPseudoModel emulates the call + * on the matrix itself like the model function would + */ + template + class AbstractPseudoModel { + public: + AbstractPseudoModel() {} + virtual ~AbstractPseudoModel() {} + + virtual typename storm::storage::SparseMatrix::const_rows getRows(uint_fast64_t state) const = 0; + + /*! + * Calculates the number of states in the represented system. + * @return The Number of States in the underlying model/transition matrix + */ + virtual uint_fast64_t getNumberOfStates() const = 0; + + /*! + * Extracts the dependency graph from a (pseudo-) model according to the given partition. + * + * @param decomposition A decomposition containing the blocks of the partition of the system. + * @return A sparse matrix with bool entries that represents the dependency graph of the blocks of the partition. + */ + virtual storm::storage::SparseMatrix extractPartitionDependencyGraph(storm::storage::Decomposition const& decomposition) const; + }; + + template + class ModelBasedPseudoModel : public AbstractPseudoModel { + public: + /*! + * Creates an encapsulation for the SCC decomposition based on a model + * @param model The Model on which the decomposition is to be performed + */ + ModelBasedPseudoModel(storm::models::AbstractModel const& model); + virtual typename storm::storage::SparseMatrix::const_rows getRows(uint_fast64_t state) const override; + virtual uint_fast64_t getNumberOfStates() const override; + private: + storm::models::AbstractModel const& _model; + }; + + template + class NonDeterministicMatrixBasedPseudoModel : public AbstractPseudoModel { + public: + /*! + * Creates an encapsulation for the SCC decomposition based on a matrix + * @param matrix The Matrix on which the decomposition is to be performed + */ + NonDeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix const& matrix, std::vector const& nondeterministicChoiceIndices); + virtual typename storm::storage::SparseMatrix::const_rows getRows(uint_fast64_t state) const override; + virtual uint_fast64_t getNumberOfStates() const override; + private: + storm::storage::SparseMatrix const& _matrix; + std::vector const& _nondeterministicChoiceIndices; + }; + + template + class DeterministicMatrixBasedPseudoModel : public AbstractPseudoModel { + public: + /*! + * Creates an encapsulation for the SCC decomposition based on a matrix + * @param matrix The Matrix on which the decomposition is to be performed + */ + DeterministicMatrixBasedPseudoModel(storm::storage::SparseMatrix const& matrix); + virtual typename storm::storage::SparseMatrix::const_rows getRows(uint_fast64_t state) const override; + virtual uint_fast64_t getNumberOfStates() const override; + private: + storm::storage::SparseMatrix const& _matrix; + }; + } +} + +#endif // STORM_MODELS_PSEUDOMODEL_H_ \ No newline at end of file diff --git a/src/solver/NondeterministicLinearEquationSolver.h b/src/solver/NondeterministicLinearEquationSolver.h index 8c5bc2334..a6beafcbe 100644 --- a/src/solver/NondeterministicLinearEquationSolver.h +++ b/src/solver/NondeterministicLinearEquationSolver.h @@ -40,7 +40,7 @@ namespace storm { * @return The solution vector x of the system of linear equations as the content of the parameter x. */ virtual void solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& rowGroupIndices, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const = 0; - + /*! * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes * x[i+1] = min/max(A*x[i] + b) until x[n], where x[0] = x. After each multiplication and addition, the diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index 4b90dbb40..e075e2ee6 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -1,34 +1,49 @@ -#include "src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h" +#include "src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h" #include #include "src/settings/Settings.h" #include "src/utility/vector.h" +#include "src/utility/graph.h" +#include "src/models/PseudoModel.h" +#include "src/storage/StronglyConnectedComponentDecomposition.h" namespace storm { namespace solver { template TopologicalValueIterationNondeterministicLinearEquationSolver::TopologicalValueIterationNondeterministicLinearEquationSolver() { - // // Intentionally left empty. + // Get the settings object to customize solving. + storm::settings::Settings* settings = storm::settings::Settings::getInstance(); + + // Get appropriate settings. + maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger(); + precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); + relative = !settings->isSet("absolute"); } template - TopologicalValueIterationNondeterministicLinearEquationSolver::TopologicalValueIterationNondeterministicLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeNondeterministicLinearEquationSolver(precision, maximalNumberOfIterations, relative) { + TopologicalValueIterationNondeterministicLinearEquationSolver::TopologicalValueIterationNondeterministicLinearEquationSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeNondeterministicLinearEquationSolver(precision, maximalNumberOfIterations, relative) { // Intentionally left empty. } template - TopologicalValueIterationNondeterministicLinearEquationSolver* TopologicalValueIterationNondeterministicLinearEquationSolver::clone() const { - return new NativeNondeterministicLinearEquationSolver(*this); + NondeterministicLinearEquationSolver* TopologicalValueIterationNondeterministicLinearEquationSolver::clone() const { + return new TopologicalValueIterationNondeterministicLinearEquationSolver(*this); } template void TopologicalValueIterationNondeterministicLinearEquationSolver::solveEquationSystem(bool minimize, storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices, std::vector* multiplyResult, std::vector* newX) const { // Now, we need to determine the SCCs of the MDP and a topological sort. - std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); + //std::vector> stronglyConnectedComponents = storm::utility::graph::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + //storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); + + storm::models::NonDeterministicMatrixBasedPseudoModel pseudoModel(A, nondeterministicChoiceIndices); + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*static_cast*>(&pseudoModel), false, false); + storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = pseudoModel.extractPartitionDependencyGraph(sccDecomposition); + + std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. @@ -52,14 +67,14 @@ namespace storm { // Iterate over all SCCs of the MDP as specified by the topological sort. This guarantees that an SCC is only // solved after all SCCs it depends on have been solved. for (auto sccIndexIt = topologicalSort.begin(); sccIndexIt != topologicalSort.end() && converged; ++sccIndexIt) { - std::vector const& scc = stronglyConnectedComponents[*sccIndexIt]; + std::vector const& scc = sccDecomposition[*sccIndexIt]; // For the current SCC, we need to perform value iteration until convergence. localIterations = 0; converged = false; - while (!converged && localIterations < maxIterations) { + while (!converged && localIterations < maximalNumberOfIterations) { // Compute x' = A*x + b. - matrix.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult); + A.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult); storm::utility::addVectors(scc, nondeterministicChoiceIndices, multiplyResult, b); /* @@ -119,76 +134,6 @@ namespace storm { else { LOG4CPLUS_WARN(logger, "Iterative solver did not converged after " << currentMaxLocalIterations << " iterations."); } - - - /* - - !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - - */ - - // Set up the environment for the power method. If scratch memory was not provided, we need to create it. - bool multiplyResultMemoryProvided = true; - if (multiplyResult == nullptr) { - multiplyResult = new std::vector(A.getRowCount()); - multiplyResultMemoryProvided = false; - } - std::vector* currentX = &x; - bool xMemoryProvided = true; - if (newX == nullptr) { - newX = new std::vector(x.size()); - xMemoryProvided = false; - } - std::vector* swap = nullptr; - uint_fast64_t iterations = 0; - bool converged = false; - - // Keep track of which of the vectors for x is the auxiliary copy. - std::vector* copyX = newX; - - // Proceed with the iterations as long as the method did not converge or reach the - // user-specified maximum number of iterations. - while (!converged && iterations < maximalNumberOfIterations) { - // Compute x' = A*x + b. - A.multiplyWithVector(*currentX, *multiplyResult); - storm::utility::vector::addVectorsInPlace(*multiplyResult, b); - - // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost - // element of the min/max operator stack. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, nondeterministicChoiceIndices); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, nondeterministicChoiceIndices); - } - - // Determine whether the method converged. - converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, precision, relative); - - // Update environment variables. - std::swap(currentX, newX); - ++iterations; - } - - // Check if the solver converged and issue a warning otherwise. - if (converged) { - LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); - } else { - LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); - } - - // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result - // is currently stored in currentX, but x is the output vector. - if (currentX == copyX) { - std::swap(x, *currentX); - } - - if (!xMemoryProvided) { - delete copyX; - } - - if (!multiplyResultMemoryProvided) { - delete multiplyResult; - } } // Explicitly instantiate the solver. diff --git a/src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h similarity index 94% rename from src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h rename to src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h index 2dfc0206d..86262e062 100644 --- a/src/solver/TopologicalValueIterationNativeNondeterministicLinearEquationSolver.h +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.h @@ -1,7 +1,6 @@ #ifndef STORM_SOLVER_TOPOLOGICALVALUEITERATIONNONDETERMINISTICLINEAREQUATIONSOLVER_H_ #define STORM_SOLVER_TOPOLOGICALVALUEITERATIONNONDETERMINISTICLINEAREQUATIONSOLVER_H_ -#include "src/solver/NondeterministicLinearEquationSolver.h" #include "src/solver/NativeNondeterministicLinearEquationSolver.h" namespace storm { @@ -11,7 +10,7 @@ namespace storm { * A class that uses SCC Decompositions to solve a linear equation system */ template - class TopologicalValueIterationNondeterministicLinearEquationSolver : public NondeterministicLinearEquationSolver { + class TopologicalValueIterationNondeterministicLinearEquationSolver : public NativeNondeterministicLinearEquationSolver { public: /*! * Constructs a nondeterministic linear equation solver with parameters being set according to the settings diff --git a/src/storage/Decomposition.h b/src/storage/Decomposition.h index 0c44943c9..5808e2500 100644 --- a/src/storage/Decomposition.h +++ b/src/storage/Decomposition.h @@ -8,7 +8,7 @@ namespace storm { namespace storage { // A typedef that specifies the type of a block consisting of states only. typedef boost::container::flat_set StateBlock; - + /*! * Writes a string representation of the state block to the given output stream. * @@ -129,11 +129,10 @@ namespace storm { * @return The block with the given index. */ Block& operator[](uint_fast64_t index); - + // Declare the streaming operator as a friend function to enable output of decompositions. template friend std::ostream& operator<<(std::ostream& out, Decomposition const& decomposition); - protected: // The blocks of the decomposition. std::vector blocks; diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 6e9f08386..b46a5706f 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -1,5 +1,6 @@ #include "src/storage/StronglyConnectedComponentDecomposition.h" #include "src/models/AbstractModel.h" +#include "src/models/PseudoModel.h" namespace storm { namespace storage { @@ -10,19 +11,37 @@ namespace storm { template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs, bool onlyBottomSccs) : Decomposition() { - performSccDecomposition(model, dropNaiveSccs, onlyBottomSccs); + performSccDecomposition(storm::models::ModelBasedPseudoModel(model), dropNaiveSccs, onlyBottomSccs); } + + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractPseudoModel const& pseudoModel, bool dropNaiveSccs, bool onlyBottomSccs) : Decomposition() { + performSccDecomposition(pseudoModel, dropNaiveSccs, onlyBottomSccs); + } - template + template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { - storm::storage::BitVector subsystem(model.getNumberOfStates(), block.begin(), block.end()); - performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs); + storm::models::ModelBasedPseudoModel encapsulatedModel(model); + storm::storage::BitVector subsystem(encapsulatedModel.getNumberOfStates(), block.begin(), block.end()); + performSccDecomposition(*static_cast*>(&encapsulatedModel), subsystem, dropNaiveSccs, onlyBottomSccs); } + + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractPseudoModel const& pseudoModel, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs) { + storm::storage::BitVector subsystem(pseudoModel.getNumberOfStates(), block.begin(), block.end()); + performSccDecomposition(pseudoModel, subsystem, dropNaiveSccs, onlyBottomSccs); + } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { - performSccDecomposition(model, subsystem, dropNaiveSccs, onlyBottomSccs); + storm::models::ModelBasedPseudoModel encapsulatedModel(model); + performSccDecomposition(*static_cast*>(&encapsulatedModel), subsystem, dropNaiveSccs, onlyBottomSccs); } + + template + StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(storm::models::AbstractPseudoModel const& pseudoModel, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + performSccDecomposition(pseudoModel, subsystem, dropNaiveSccs, onlyBottomSccs); + } template StronglyConnectedComponentDecomposition::StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other) : Decomposition(other) { @@ -47,7 +66,7 @@ namespace storm { } template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractPseudoModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs) { // Set up the environment of Tarjan's algorithm. uint_fast64_t numberOfStates = model.getNumberOfStates(); std::vector tarjanStack; @@ -68,7 +87,7 @@ namespace storm { template - void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs, bool onlyBottomSccs) { + void StronglyConnectedComponentDecomposition::performSccDecomposition(storm::models::AbstractPseudoModel const& model, bool dropNaiveSccs, bool onlyBottomSccs) { // Prepare a block that contains all states for a call to the other overload of this function. storm::storage::BitVector fullSystem(model.getNumberOfStates(), true); @@ -77,7 +96,7 @@ namespace storm { } template - void StronglyConnectedComponentDecomposition::performSccDecompositionHelper(storm::models::AbstractModel const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs) { + void StronglyConnectedComponentDecomposition::performSccDecompositionHelper(storm::models::AbstractPseudoModel const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs) { // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm into an iterative // version. In particular, we keep one stack for states and one stack for the iterators. The last one is not // strictly needed, but reduces iteration work when all successors of a particular state are considered. @@ -201,7 +220,7 @@ namespace storm { } } } - + // Explicitly instantiate the SCC decomposition. template class StronglyConnectedComponentDecomposition; } // namespace storage diff --git a/src/storage/StronglyConnectedComponentDecomposition.h b/src/storage/StronglyConnectedComponentDecomposition.h index a8ce0403c..091e3f0ff 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.h +++ b/src/storage/StronglyConnectedComponentDecomposition.h @@ -3,11 +3,15 @@ #include "src/storage/Decomposition.h" #include "src/storage/BitVector.h" +#include "src/storage/SparseMatrix.h" namespace storm { namespace models { // Forward declare the abstract model class. template class AbstractModel; + + // Forward declare the abstract pseudo-model class. + template class AbstractPseudoModel; } namespace storage { @@ -33,6 +37,17 @@ namespace storm { * leaving the SCC), are kept. */ StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + + /* + * Creates an SCC decomposition of the given encapsulated model. + * + * @param pseudoModel The encapsulated model to decompose into SCCs. + * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state + * without a self-loop) are to be kept in the decomposition. + * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of + * leaving the SCC), are kept. + */ + StronglyConnectedComponentDecomposition(storm::models::AbstractPseudoModel const& pseudoModel, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /* * Creates an SCC decomposition of the given block in the given model. @@ -45,6 +60,18 @@ namespace storm { * leaving the SCC), are kept. */ StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + + /* + * Creates an SCC decomposition of the given block in the given encapsulated model. + * + * @param pseudoModel The encapsulated model whose block to decompose. + * @param block The block to decompose into SCCs. + * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state + * without a self-loop) are to be kept in the decomposition. + * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of + * leaving the SCC), are kept. + */ + StronglyConnectedComponentDecomposition(storm::models::AbstractPseudoModel const& pseudoModel, StateBlock const& block, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /* * Creates an SCC decomposition of the given subsystem in the given model. @@ -57,36 +84,50 @@ namespace storm { * leaving the SCC), are kept. */ StronglyConnectedComponentDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); + + /* + * Creates an SCC decomposition of the given subsystem in the given encapsulated model. + * + * @param pseudoModel The encapsulated model that contains the block. + * @param subsystem A bit vector indicating which subsystem to consider for the decomposition into SCCs. + * @param dropNaiveSccs A flag that indicates whether trivial SCCs (i.e. SCCs consisting of just one state + * without a self-loop) are to be kept in the decomposition. + * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of + * leaving the SCC), are kept. + */ + StronglyConnectedComponentDecomposition(storm::models::AbstractPseudoModel const& pseudoModel, storm::storage::BitVector const& subsystem, bool dropNaiveSccs = false, bool onlyBottomSccs = false); /*! * Creates an SCC decomposition by copying the given SCC decomposition. * - * @oaram other The SCC decomposition to copy. + * @param other The SCC decomposition to copy. */ StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition const& other); /*! * Assigns the contents of the given SCC decomposition to the current one by copying its contents. * - * @oaram other The SCC decomposition from which to copy-assign. + * @param other The SCC decomposition from which to copy-assign. */ StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition const& other); /*! * Creates an SCC decomposition by moving the given SCC decomposition. * - * @oaram other The SCC decomposition to move. + * @param other The SCC decomposition to move. */ StronglyConnectedComponentDecomposition(StronglyConnectedComponentDecomposition&& other); /*! * Assigns the contents of the given SCC decomposition to the current one by moving its contents. * - * @oaram other The SCC decomposition from which to copy-assign. + * @param other The SCC decomposition from which to copy-assign. */ StronglyConnectedComponentDecomposition& operator=(StronglyConnectedComponentDecomposition&& other); private: + + /*! * Performs the SCC decomposition of the given model. As a side-effect this fills the vector of * blocks of the decomposition. @@ -97,7 +138,7 @@ namespace storm { * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of * leaving the SCC), are kept. */ - void performSccDecomposition(storm::models::AbstractModel const& model, bool dropNaiveSccs, bool onlyBottomSccs); + void performSccDecomposition(storm::models::AbstractPseudoModel const& model, bool dropNaiveSccs, bool onlyBottomSccs); /* * Performs the SCC decomposition of the given block in the given model. As a side-effect this fills @@ -110,7 +151,7 @@ namespace storm { * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of * leaving the SCC), are kept. */ - void performSccDecomposition(storm::models::AbstractModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); + void performSccDecomposition(storm::models::AbstractPseudoModel const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs); /*! * A helper function that performs the SCC decomposition given all auxiliary data structures. As a @@ -130,7 +171,7 @@ namespace storm { * @param onlyBottomSccs If set to true, only bottom SCCs, i.e. SCCs in which all states have no way of * leaving the SCC), are kept. */ - void performSccDecompositionHelper(storm::models::AbstractModel const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs); + void performSccDecompositionHelper(storm::models::AbstractPseudoModel const& model, uint_fast64_t startState, storm::storage::BitVector const& subsystem, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, bool dropNaiveSccs, bool onlyBottomSccs); }; } }