From 1990567b84ffd7f25ee739072f83fff98a35b88a Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 23 Mar 2015 22:24:13 +0100 Subject: [PATCH] Started to improve performance of sparse CTMC model checker. Former-commit-id: 1d014412ec6717d9adc09f30c925794be8de38df --- .../csl/SparseCtmcCslModelChecker.cpp | 44 +++-- .../csl/SparseCtmcCslModelChecker.h | 3 +- .../SparseMarkovAutomatonCslModelChecker.cpp | 8 +- src/settings/modules/GeneralSettings.cpp | 4 + src/settings/modules/GeneralSettings.h | 7 + src/solver/GmmxxLinearEquationSolver.cpp | 2 +- src/solver/GmmxxLinearEquationSolver.h | 2 +- ...xxNondeterministicLinearEquationSolver.cpp | 2 +- src/solver/LinearEquationSolver.h | 2 +- src/solver/NativeLinearEquationSolver.cpp | 2 +- src/solver/NativeLinearEquationSolver.h | 2 +- ...alNondeterministicLinearEquationSolver.cpp | 5 +- src/utility/cli.h | 1 - src/utility/solver.cpp | 5 + src/utility/solver.h | 2 + .../GmmxxDtmcPrctModelCheckerTest.cpp | 6 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 159 ++++++++++++++++++ .../NativeDtmcPrctlModelCheckerTest.cpp | 84 +++++++++ ...cpp => NativeMdpPrctlModelCheckerTest.cpp} | 6 +- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 12 +- 20 files changed, 316 insertions(+), 42 deletions(-) create mode 100644 test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp create mode 100644 test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp rename test/performance/modelchecker/{SparseMdpPrctlModelCheckerTest.cpp => NativeMdpPrctlModelCheckerTest.cpp} (95%) diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 80d1147e6..4f649338e 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -117,15 +117,22 @@ namespace storm { STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); // Compute the uniformized matrix. - storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0, psiStates, uniformizationRate, exitRates); + storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0NonPsi, storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, exitRates); - // Finally compute the transient probabilities. - std::vector psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero()); - storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one()); + // Compute the vector that is to be added as a compensation for removing the absorbing states. + std::vector b = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(statesWithProbabilityGreater0NonPsi, psiStates); + for (auto& element : b) { + element /= uniformizationRate; + } + + std::vector values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero()); - std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, upperBound, uniformizationRate, psiStateValues, *this->linearEquationSolverFactory); + // Finally compute the transient probabilities. + std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, b, upperBound, uniformizationRate, values, *this->linearEquationSolverFactory); result = std::vector(this->getModel().getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult); + + storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0NonPsi, subresult); + storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } else if (comparator.isInfinity(upperBound)) { // In this case, the interval is of the form [t, inf] with t != 0. @@ -150,7 +157,7 @@ namespace storm { storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, storm::storage::BitVector(result.size()), uniformizationRate, exitRates); // Compute the transient probabilities. - subResult = this->computeTransientProbabilities(uniformizedMatrix, lowerBound, uniformizationRate, subResult, *this->linearEquationSolverFactory); + subResult = this->computeTransientProbabilities(uniformizedMatrix, std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()), lowerBound, uniformizationRate, subResult, *this->linearEquationSolverFactory); // Fill in the correct values. storm::utility::vector::setVectorValues(result, ~relevantStates, storm::utility::zero()); @@ -172,7 +179,7 @@ namespace storm { // Start by computing the transient probabilities of reaching a psi state in time t' - t. std::vector psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero()); storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one()); - std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, upperBound - lowerBound, uniformizationRate, psiStateValues, *this->linearEquationSolverFactory); + std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, std::vector(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero()), upperBound - lowerBound, uniformizationRate, psiStateValues, *this->linearEquationSolverFactory); // Determine the set of states that must be considered further. storm::storage::BitVector relevantStates = storm::utility::vector::filterGreaterZero(subresult); @@ -192,7 +199,7 @@ namespace storm { // Finally, we compute the second set of transient probabilities. uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, exitRates); - newSubresult = this->computeTransientProbabilities(uniformizedMatrix, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory); + newSubresult = this->computeTransientProbabilities(uniformizedMatrix, std::vector(relevantStates.getNumberOfSetBits(), storm::utility::zero()), lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory); // Fill in the correct values. result = std::vector(this->getModel().getNumberOfStates(), storm::utility::zero()); @@ -207,6 +214,9 @@ namespace storm { template storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeUniformizedMatrix(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& absorbingStates, ValueType uniformizationRate, std::vector const& exitRates) { + STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); + STORM_LOG_DEBUG("Keeping " << maybeStates.getNumberOfSetBits() << " rows."); + // Create the submatrix that only contains the states with a positive probability (including the // psi states) and reserve space for elements on the diagonal. storm::storage::SparseMatrix uniformizedMatrix = transitionMatrix.getSubmatrix(false, maybeStates, maybeStates, true); @@ -240,7 +250,8 @@ namespace storm { template template - std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) const { + std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const& b, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) const { + ValueType lambda = timeBound * uniformizationRate; // If no time can pass, the current values are the result. @@ -250,6 +261,7 @@ namespace storm { // Use Fox-Glynn to get the truncation points and the weights. std::tuple> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::generalSettings().getPrecision() / 8.0); + STORM_LOG_DEBUG("Fox-Glynn cutoff points: left=" << std::get<0>(foxGlynnResult) << ", right=" << std::get<1>(foxGlynnResult)); // Scale the weights so they add up to one. for (auto& element : std::get<3>(foxGlynnResult)) { @@ -266,12 +278,16 @@ namespace storm { } } + STORM_LOG_DEBUG("Starting iterations with " << uniformizedMatrix.getRowCount() << " x " << uniformizedMatrix.getColumnCount() << " matrix."); + // Initialize result. std::vector result; uint_fast64_t startingIteration = std::get<0>(foxGlynnResult); if (startingIteration == 0) { result = values; storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]); + std::function addAndScale = [&foxGlynnResult] (ValueType const& a, ValueType const& b) { return a + std::get<3>(foxGlynnResult)[0] * b; }; + storm::utility::vector::applyPointwiseInPlace(result, b, addAndScale); ++startingIteration; } else { if (computeCumulativeReward) { @@ -288,7 +304,7 @@ namespace storm { if (!computeCumulativeReward && std::get<0>(foxGlynnResult) > 1) { // Perform the matrix-vector multiplications (without adding). - solver->performMatrixVectorMultiplication(values, nullptr, std::get<0>(foxGlynnResult) - 1, &multiplicationResult); + solver->performMatrixVectorMultiplication(values, &b, std::get<0>(foxGlynnResult) - 1, &multiplicationResult); } else if (computeCumulativeReward) { std::function addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; }; @@ -304,7 +320,7 @@ namespace storm { ValueType weight = 0; std::function addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; }; for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) { - solver->performMatrixVectorMultiplication(values, nullptr, 1, &multiplicationResult); + solver->performMatrixVectorMultiplication(values, &b, 1, &multiplicationResult); weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)]; storm::utility::vector::applyPointwiseInPlace(result, values, addAndScale); @@ -341,7 +357,7 @@ namespace storm { STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive."); storm::storage::SparseMatrix uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector()); - result = this->computeTransientProbabilities(uniformizedMatrix, timeBound, uniformizationRate, result, *this->linearEquationSolverFactory); + result = this->computeTransientProbabilities(uniformizedMatrix, std::vector(this->getModel().getNumberOfStates(), storm::utility::zero()), timeBound, uniformizationRate, result, *this->linearEquationSolverFactory); } return result; @@ -386,7 +402,7 @@ namespace storm { } // Finally, compute the transient probabilities. - return this->computeTransientProbabilities(uniformizedMatrix, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory); + return this->computeTransientProbabilities(uniformizedMatrix, std::vector(this->getModel().getNumberOfStates(), storm::utility::zero()), timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolverFactory); } template diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index e604e04d4..8049dace2 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -51,6 +51,7 @@ namespace storm { * Computes the transient probabilities for lambda time steps. * * @param uniformizedMatrix The uniformized transition matrix. + * @param b A vector that is added in each step as a possible compensation for the removed absorbing states. * @param timeBound The time bound to use. * @param uniformizationRate The used uniformization rate. * @param values A vector mapping each state to an initial probability. @@ -60,7 +61,7 @@ namespace storm { * @return The vector of transient probabilities. */ template - std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) const; + std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, std::vector const& b, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) const; /*! * Converts the given rate-matrix into a time-abstract probability matrix. diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 45dd66b00..87fb93b00 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -106,7 +106,7 @@ namespace storm { storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed); // Now perform the inner value iteration for probabilistic states. - solver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); // (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic. aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian); @@ -119,7 +119,7 @@ namespace storm { // After the loop, perform one more step of the value iteration for PS states. aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); storm::utility::vector::addVectorsInPlace(bProbabilistic, bProbabilisticFixed); - solver->solveEquationSystem(min, aProbabilistic, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); + solver->solveEquationSystem(min, probabilisticNonGoalValues, bProbabilistic, &multiplicationResultScratchMemory, &aProbabilisticScratchMemory); } template @@ -380,7 +380,7 @@ namespace storm { std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(sspMatrix); - solver->solveEquationSystem(minimize, sspMatrix, x, b); + solver->solveEquationSystem(minimize, x, b); // Prepare result vector. std::vector result(model.getNumberOfStates()); @@ -564,7 +564,7 @@ namespace storm { // Solve the corresponding system of equations. std::unique_ptr> solver = nondeterministicLinearEquationSolverFactory->create(submatrix); - solver->solveEquationSystem(minimize, submatrix, x, b); + solver->solveEquationSystem(minimize, x, b); // Create resulting vector. std::vector result(model.getNumberOfStates()); diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 4133feeb1..b809f5a16 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -233,6 +233,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); } + bool GeneralSettings::isEquationSolverSet() const { + return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); + } + GeneralSettings::LpSolver GeneralSettings::getLpSolver() const { std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); if (lpSolverName == "gurobi") { diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index cde515b45..694f57c58 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -255,6 +255,13 @@ namespace storm { */ EquationSolver getEquationSolver() const; + /*! + * Retrieves whether a equation solver has been set. + * + * @return True iff an equation solver has been set. + */ + bool isEquationSolverSet() const; + /*! * Retrieves the selected LP solver. * diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp index d40e9bb70..0bc5a3c46 100644 --- a/src/solver/GmmxxLinearEquationSolver.cpp +++ b/src/solver/GmmxxLinearEquationSolver.cpp @@ -109,7 +109,7 @@ namespace storm { } template - void GmmxxLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void GmmxxLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. std::vector* currentX = &x; diff --git a/src/solver/GmmxxLinearEquationSolver.h b/src/solver/GmmxxLinearEquationSolver.h index 7ec0dcc8f..ec7aceb6d 100644 --- a/src/solver/GmmxxLinearEquationSolver.h +++ b/src/solver/GmmxxLinearEquationSolver.h @@ -48,7 +48,7 @@ namespace storm { virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; private: /*! diff --git a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp index 94fad460c..6f78f3caa 100644 --- a/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp +++ b/src/solver/GmmxxNondeterministicLinearEquationSolver.cpp @@ -95,7 +95,7 @@ namespace storm { void GmmxxNondeterministicLinearEquationSolver::performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { - multiplyResult = new std::vector(rowGroupIndices.size() - 1); + multiplyResult = new std::vector(gmmxxMatrix->nr); multiplyResultMemoryProvided = false; } diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 82a229659..43b3f9ad5 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -39,7 +39,7 @@ namespace storm { * @param multiplyResult If non-null, this memory is used as a scratch memory. If given, the length of this * vector must be equal to the number of rows of A. */ - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; }; } // namespace solver diff --git a/src/solver/NativeLinearEquationSolver.cpp b/src/solver/NativeLinearEquationSolver.cpp index 6b89d8134..47c72dae8 100644 --- a/src/solver/NativeLinearEquationSolver.cpp +++ b/src/solver/NativeLinearEquationSolver.cpp @@ -83,7 +83,7 @@ namespace storm { } template - void NativeLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector* b, uint_fast64_t n, std::vector* multiplyResult) const { + void NativeLinearEquationSolver::performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n, std::vector* multiplyResult) const { // Set up some temporary variables so that we can just swap pointers instead of copying the result after // each iteration. std::vector* currentX = &x; diff --git a/src/solver/NativeLinearEquationSolver.h b/src/solver/NativeLinearEquationSolver.h index ae008a5aa..f8f5a1378 100644 --- a/src/solver/NativeLinearEquationSolver.h +++ b/src/solver/NativeLinearEquationSolver.h @@ -38,7 +38,7 @@ namespace storm { virtual void solveEquationSystem(std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr) const override; - virtual void performMatrixVectorMultiplication(std::vector& x, std::vector* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; + virtual void performMatrixVectorMultiplication(std::vector& x, std::vector const* b, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; private: /*! diff --git a/src/solver/TopologicalNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalNondeterministicLinearEquationSolver.cpp index 343f36f1b..fda2998f2 100644 --- a/src/solver/TopologicalNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalNondeterministicLinearEquationSolver.cpp @@ -142,10 +142,7 @@ namespace storm { storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(this->A, fullSystem, false, false); - if (sccDecomposition.size() == 0) { - LOG4CPLUS_ERROR(logger, "Can not solve given Equation System as the SCC Decomposition returned no SCCs."); - throw storm::exceptions::IllegalArgumentException() << "Can not solve given Equation System as the SCC Decomposition returned no SCCs."; - } + STORM_LOG_THROW(sccDecomposition.size() > 0, storm::exceptions::IllegalArgumentException, "Can not solve given equation system as the SCC decomposition returned no SCCs."); storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = sccDecomposition.extractPartitionDependencyGraph(this->A); std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); diff --git a/src/utility/cli.h b/src/utility/cli.h index 07e520f68..402e96552 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -66,7 +66,6 @@ log4cplus::Logger printer; #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" -#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" // Headers for counterexample generation. diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 126864c31..76429ebdf 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -74,6 +74,11 @@ namespace storm { return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); } + std::unique_ptr getLpSolver(std::string const& name) { + std::unique_ptr factory(new LpSolverFactory()); + return factory->create(name); + } + template class LinearEquationSolverFactory; template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; diff --git a/src/utility/solver.h b/src/utility/solver.h index 137f4e210..d9f934c98 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -81,6 +81,8 @@ namespace storm { public: virtual std::unique_ptr create(std::string const& name) const override; }; + + std::unique_ptr getLpSolver(std::string const& name); } } } diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index ae366ae29..a4d4bd61f 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -4,7 +4,7 @@ #include "src/settings/SettingMemento.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/utility/solver.h" #include "src/parser/AutoParser.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { @@ -17,7 +17,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("observe0Greater1"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -55,7 +55,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); - storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver())); + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..c834ece2e --- /dev/null +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,159 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/settings/SettingsManager.h" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/utility/solver.h" +#include "src/parser/AutoParser.h" + +TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { + std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); + ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); + + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(6.172433512, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(6.1724344, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(GmxxMdpPrctlModelCheckerTest, Consensus) { + std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = abstractModel->as>(); + + ASSERT_EQ(63616ull, mdp->getNumberOfStates()); + ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); + + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxNondeterministicLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("finished"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("finished"); + auto labelFormula2 = std::make_shared("all_coins_equal_0"); + auto andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); + eventuallyFormula = std::make_shared(andFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.4374282832, quantitativeResult2[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("finished"); + labelFormula2 = std::make_shared("all_coins_equal_1"); + andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, labelFormula2); + eventuallyFormula = std::make_shared(andFormula); + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.5293286369, quantitativeResult3[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("finished"); + labelFormula2 = std::make_shared("agree"); + auto notFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, labelFormula2); + andFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::And, labelFormula, notFormula); + eventuallyFormula = std::make_shared(andFormula); + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.10414097, quantitativeResult4[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("finished"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 50); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + + result = checker.check(*minProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0, quantitativeResult5[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult6 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.0, quantitativeResult6[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("finished"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult7 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1725.593313, quantitativeResult7[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult8 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(2183.142422, quantitativeResult8[31168], storm::settings::nativeEquationSolverSettings().getPrecision()); +} diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..15038115a --- /dev/null +++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -0,0 +1,84 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/SettingMemento.h" +#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/utility/solver.h" +#include "src/parser/AutoParser.h" + +TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { + std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = abstractModel->as>(); + + ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); + ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); + + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("observe0Greater1"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.22968140721646868, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("observeIGreater1"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("observeOnlyTrueSender"); + eventuallyFormula = std::make_shared(labelFormula); + + result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.22742305378217331, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); +} + + +TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) { + std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); + + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = abstractModel->as>(); + + ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); + ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); + + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + + std::unique_ptr result = checker.check(*eventuallyFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); + + result = checker.check(*boundedUntilFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + + result = checker.check(*reachabilityRewardFormula); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(1.0252174454896057, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); +} diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp similarity index 95% rename from test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp rename to test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 1ef78c021..b2bbba7fa 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -4,7 +4,7 @@ #include "src/settings/SettingsManager.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "src/solver/NativeNondeterministicLinearEquationSolver.h" +#include "src/utility/solver.h" #include "src/parser/AutoParser.h" TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { @@ -17,7 +17,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); auto labelFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(labelFormula); @@ -79,7 +79,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) { ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); - storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); + storm::modelchecker::SparseMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeNondeterministicLinearEquationSolverFactory())); auto labelFormula = std::make_shared("finished"); auto eventuallyFormula = std::make_shared(labelFormula); diff --git a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index a66b47028..f73102617 100644 --- a/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -1,20 +1,20 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h" -#include "src/solver/NativeNondeterministicLinearEquationSolver.h" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/utility/solver.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/settings/SettingsManager.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { - std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as>(); + std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew")->as>(); ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); - storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); auto apFormula = std::make_shared("elected"); auto eventuallyFormula = std::make_shared(apFormula); @@ -81,12 +81,12 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) { // Increase the maximal number of iterations, because the solver does not converge otherwise. // This is done in the main cpp unit - std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as>(); + std::shared_ptr> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "")->as>(); ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); - storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::SparseMdpPrctlModelChecker mc(*mdp, std::unique_ptr>(new storm::utility::solver::TopologicalNondeterministicLinearEquationSolverFactory())); auto apFormula = std::make_shared("finished"); auto eventuallyFormula = std::make_shared(apFormula);