From 99f2344da94a78909eb8837a0a4e3997d4582b73 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 9 Mar 2020 14:00:33 +0100 Subject: [PATCH] Use acyclic solver in various Markov automata methods. --- .../helper/SparseMarkovAutomatonCslHelper.cpp | 104 +++++++++--------- 1 file changed, 50 insertions(+), 54 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index d188f7a35..38d62b1f3 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -32,6 +32,34 @@ namespace storm { namespace modelchecker { namespace helper { + template + std::unique_ptr> setUpProbabilisticStatesSolver(storm::Environment& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitions) { + std::unique_ptr> solver; + // The min-max system has no end components as we assume non-zeno MAs. + if (transitions.getNonzeroEntryCount() > 0) { + storm::solver::GeneralMinMaxLinearEquationSolverFactory factory; + bool isAcyclic = !storm::utility::graph::hasCycle(transitions); + if (isAcyclic) { + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Acyclic); + } + solver = factory.create(env, transitions); + solver->setHasUniqueSolution(true); // Assume non-zeno MA + solver->setHasNoEndComponents(true); // assume non-zeno MA + solver->setLowerBound(storm::utility::zero()); + solver->setUpperBound(storm::utility::one()); + solver->setCachingEnabled(true); + solver->setRequirementsChecked(true); + auto req = solver->getRequirements(env, dir); + req.clearBounds(); + req.clearUniqueSolution(); + if (isAcyclic) { + req.clearAcyclic(); + } + STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "The solver requirement " << req.getEnabledRequirementsAsString() << " has not been checked."); + } + return solver; + } + template class UnifPlusHelper { public: @@ -377,25 +405,6 @@ namespace storm { } } - std::unique_ptr> setUpProbabilisticStatesSolver(storm::Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitions) const { - std::unique_ptr> solver; - if (transitions.getNonzeroEntryCount() > 0) { - storm::solver::GeneralMinMaxLinearEquationSolverFactory factory; - solver = factory.create(env, transitions); - solver->setHasUniqueSolution(true); // Assume non-zeno MA - solver->setHasNoEndComponents(true); // assume non-zeno MA - solver->setLowerBound(storm::utility::zero()); - solver->setUpperBound(storm::utility::one()); - solver->setCachingEnabled(true); - solver->setRequirementsChecked(true); - auto req = solver->getRequirements(env, dir); - req.clearBounds(); - req.clearUniqueSolution(); - STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "The solver requirement " << req.getEnabledRequirementsAsString() << " has not been checked."); - } - return solver; - } - storm::storage::BitVector getProb0States(OptimizationDirection dir, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) const { if (dir == storm::solver::OptimizationDirection::Maximize) { return storm::utility::graph::performProb0A(transitionMatrix.transpose(true), phiStates, psiStates); @@ -492,20 +501,11 @@ namespace storm { } } - // Check for requirements of the solver. - // The min-max system has no end components as we assume non-zeno MAs. - storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir); - requirements.clearBounds(); - STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); - - std::unique_ptr> solver = minMaxLinearEquationSolverFactory.create(env, aProbabilistic); - solver->setHasUniqueSolution(); - solver->setHasNoEndComponents(); - solver->setBounds(storm::utility::zero(), storm::utility::one()); - solver->setRequirementsChecked(); - solver->setCachingEnabled(true); - + // Create a solver object (only if there are actually transitions between probabilistic states) + auto solverEnv = env; + solverEnv.solver().setForceExact(true); + auto solver = setUpProbabilisticStatesSolver(solverEnv, dir, aProbabilistic); + // Perform the actual value iteration // * loop until the step bound has been reached // * in the loop: @@ -520,7 +520,11 @@ namespace storm { storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); // Now perform the inner value iteration for probabilistic states. - solver->solveEquations(env, dir, probabilisticNonGoalValues, bProbabilistic); + if (solver) { + solver->solveEquations(solverEnv, dir, probabilisticNonGoalValues, bProbabilistic); + } else { + storm::utility::vector::reduceVectorMinOrMax(dir, bProbabilistic, probabilisticNonGoalValues, aProbabilistic.getRowGroupIndices()); + } // (Re-)compute bMarkovian = bMarkovianFixed + aMarkovianToProbabilistic * vProbabilistic. aMarkovianToProbabilistic.multiplyWithVector(probabilisticNonGoalValues, bMarkovian); @@ -543,7 +547,11 @@ namespace storm { // After the loop, perform one more step of the value iteration for PS states. aProbabilisticToMarkovian.multiplyWithVector(markovianNonGoalValues, bProbabilistic); storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); - solver->solveEquations(env, dir, probabilisticNonGoalValues, bProbabilistic); + if (solver) { + solver->solveEquations(solverEnv, dir, probabilisticNonGoalValues, bProbabilistic); + } else { + storm::utility::vector::reduceVectorMinOrMax(dir, bProbabilistic, probabilisticNonGoalValues, aProbabilistic.getRowGroupIndices()); + } } } @@ -1077,29 +1085,13 @@ namespace storm { if (env.solver().isForceSoundness()) { // To get correct results, the inner equation systems are solved exactly. // TODO investigate how an error would propagate - solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological); - solverEnv.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::PolicyIteration); - solverEnv.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological); - solverEnv.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen); - solverEnv.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); + solverEnv.solver().setForceExact(true); } x.resize(aProbabilistic.getRowGroupCount(), storm::utility::zero()); b = probabilisticChoiceRewards; - // Check for requirements of the solver. - // The solution is unique as we assume non-zeno MAs. - storm::solver::GeneralMinMaxLinearEquationSolverFactory minMaxLinearEquationSolverFactory; - storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(solverEnv, true, true, dir); - requirements.clearLowerBounds(); - STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked."); - - solver = minMaxLinearEquationSolverFactory.create(solverEnv, std::move(aProbabilistic)); - solver->setLowerBound(storm::utility::zero()); - solver->setHasUniqueSolution(true); - solver->setHasNoEndComponents(true); - solver->setRequirementsChecked(true); - solver->setCachingEnabled(true); + solver = setUpProbabilisticStatesSolver(solverEnv, dir, aProbabilistic); } uint64_t iter = 0; @@ -1111,7 +1103,11 @@ namespace storm { ++iter; // Compute the expected total rewards for the probabilistic states if (hasProbabilisticStates) { - solver->solveEquations(solverEnv, dir, x, b); + if (solver) { + solver->solveEquations(solverEnv, dir, x, b); + } else { + storm::utility::vector::reduceVectorMinOrMax(dir, b, x, aProbabilistic.getRowGroupIndices()); + } } // now compute the values for the markovian states. We also keep track of the maximal and minimal difference between two values (for convergence checking) auto vIt = v.begin();