diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h new file mode 100644 index 000000000..80a4e2049 --- /dev/null +++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h @@ -0,0 +1,132 @@ +/* + * GmmxxDtmcPrctlModelChecker.h + * + * Created on: 06.12.2012 + * Author: Christian Dehnert + */ + +#ifndef STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ + +#include + +#include "src/models/Mdp.h" +#include "src/modelchecker/MdpPrctlModelChecker.h" +#include "src/utility/GraphAnalyzer.h" +#include "src/utility/Vector.h" +#include "src/utility/ConstTemplates.h" +#include "src/utility/Settings.h" +#include "src/adapters/GmmxxAdapter.h" +#include "src/exceptions/InvalidPropertyException.h" +#include "src/storage/JacobiDecomposition.h" + +#include "gmm/gmm_matrix.h" +#include "gmm/gmm_iter_solvers.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { + +namespace modelChecker { + +/* + * A model checking engine that makes use of the gmm++ backend. + */ +template +class TopologicalValueIterationMdpPrctlModelChecker : public MdpPrctlModelChecker { + +public: + explicit TopologicalValueIterationMdpPrctlModelChecker(storm::models::Mdp& mdp) : MdpPrctlModelChecker(mdp) { } + + virtual ~TopologicalValueIterationMdpPrctlModelChecker() { } + +private: + /*! + * Solves the given equation system under the given parameters using the power method. + * + * @param A The matrix A specifying the coefficients of the equations. + * @param x The vector x for which to solve the equations. The initial value of the elements of + * this vector are used as the initial guess and might thus influence performance and convergence. + * @param b The vector b specifying the values on the right-hand-sides of the equations. + * @return The solution of the system of linear equations in form of the elements of the vector + * x. + */ + void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { + // Get the settings object to customize solving. + storm::settings::Settings* s = storm::settings::instance(); + + // Get relevant user-defined settings for solving the equations. + double precision = s->get("precision"); + unsigned maxIterations = s->get("maxiter"); + bool relative = s->get("relative"); + + std::vector> stronglyConnectedComponents; + storm::models::GraphTransitions stronglyConnectedComponentsDependencyGraph; + storm::utility::GraphAnalyzer::performSccDecomposition(matrix, nondeterministicChoiceIndices, stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + + // Set up the environment for the power method. + std::vector multiplyResult(matrix.getRowCount()); + std::vector* currentX = &x; + std::vector* newX = new std::vector(x.size()); + std::vector* swap = nullptr; + uint_fast64_t iterations = 0; + bool converged = false; + + /* + for (auto sccIt = stronglyConnectedComponents.rbegin(), sccIte = stronglyConnectedComponents.rend(); sccIt != sccIte; ++sccIt) { + converged = false; + + std::cout << "for scc! " << *sccIt << std::endl; + while (!converged && iterations < maxIterations) { + std::cout << "first line " << std::endl; + // Compute x' = A*x + b. + matrix.multiplyWithVector(**sccIt, nondeterministicChoiceIndices, *currentX, multiplyResult); + std::cout << "after mult" << std::endl; + storm::utility::addVectors(**sccIt, nondeterministicChoiceIndices, multiplyResult, b); + std::cout << "after add " << std::endl; + + // Reduce the vector x' by applying min/max for all non-deterministic choices. + if (this->minimumOperatorStack.top()) { + storm::utility::reduceVectorMin(multiplyResult, newX, nondeterministicChoiceIndices); + } else { + storm::utility::reduceVectorMax(multiplyResult, newX, nondeterministicChoiceIndices); + } + + std::cout << "comp" << std::endl; + // Determine whether the method converged. + converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); + + // Update environment variables. + swap = currentX; + currentX = newX; + newX = swap; + ++iterations; + } + } + + if (iterations % 2 == 1) { + std::swap(x, *currentX); + delete currentX; + } else { + delete newX; + } + + // 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."); + } + + */ + } +}; + +} //namespace modelChecker + +} //namespace storm + +#endif /* STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ */