From 086201ac4342868ae0db83dc66001b000d7570ec Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 10 Oct 2017 22:54:47 +0200 Subject: [PATCH] corrected some output and adapted requirements of symbolic minmax solver --- .../prctl/helper/HybridDtmcPrctlHelper.cpp | 3 ++- .../prctl/helper/SymbolicDtmcPrctlHelper.cpp | 3 ++- .../SymbolicQuantitativeCheckResult.cpp | 6 +++++ .../SymbolicMinMaxLinearEquationSolver.cpp | 27 ++++++++++++++----- 4 files changed, 30 insertions(+), 9 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index d7986e56d..39be2fbaa 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -28,10 +28,11 @@ namespace storm { std::unique_ptr HybridDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. + STORM_LOG_TRACE("Found " << phiStates.getNonZeroCount() << " phi states and " << psiStates.getNonZeroCount() << " psi states."); std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); - STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining)."); + STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining)."); // Check whether we need to compute exact probabilities for some states. if (qualitative) { diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index cf8019aea..86f624459 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -22,10 +22,11 @@ namespace storm { storm::dd::Add SymbolicDtmcPrctlHelper::computeUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, storm::solver::SymbolicLinearEquationSolverFactory const& linearEquationSolverFactory) { // We need to identify the states which have to be taken out of the matrix, i.e. all states that have // probability 0 and 1 of satisfying the until-formula. + STORM_LOG_TRACE("Found " << phiStates.getNonZeroCount() << " phi states and " << psiStates.getNonZeroCount() << " psi states."); std::pair, storm::dd::Bdd> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); storm::dd::Bdd maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); - STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 1, " << statesWithProbability01.second.getNonZeroCount() << " with probability 0 (" << maybeStates.getNonZeroCount() << " states remaining)."); + STORM_LOG_INFO("Preprocessing: " << statesWithProbability01.first.getNonZeroCount() << " states with probability 0, " << statesWithProbability01.second.getNonZeroCount() << " with probability 1 (" << maybeStates.getNonZeroCount() << " states remaining)."); // Check whether we need to compute exact probabilities for some states. if (qualitative) { diff --git a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index b73190bab..6f5597562 100644 --- a/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -28,7 +28,13 @@ namespace storm { if (comparisonType == storm::logic::ComparisonType::Less) { states &= values.less(bound); } else if (comparisonType == storm::logic::ComparisonType::LessEqual) { + std::cout << "states zero: " << (values.equals(values.getDdManager().template getAddZero()) && reachableStates).getNonZeroCount() << std::endl; + std::cout << "states one: " << (values.equals(values.getDdManager().template getAddOne()) && reachableStates).getNonZeroCount() << std::endl; + std::cout << "states before: " << states.getNonZeroCount() << std::endl; + values.exportToDot("vals.dot"); + std::cout << "total: " <<((values.equals(values.getDdManager().template getAddOne()) && states) || (values.lessOrEqual(bound) && states)).getNonZeroCount() << std::endl; states &= values.lessOrEqual(bound); + std::cout << "states after: " << states.getNonZeroCount() << std::endl; } else if (comparisonType == storm::logic::ComparisonType::Greater) { states &= values.greater(bound); } else if (comparisonType == storm::logic::ComparisonType::GreaterEqual) { diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index bee9c20c6..490f341e3 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -406,19 +406,32 @@ namespace storm { template MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver::getRequirements(EquationSystemType const& equationSystemType, boost::optional const& direction) const { MinMaxLinearEquationSolverRequirements requirements; - - if (equationSystemType == EquationSystemType::UntilProbabilities) { - if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { + + if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration) { + if (equationSystemType == EquationSystemType::UntilProbabilities) { if (!direction || direction.get() == OptimizationDirection::Maximize) { requirements.requireValidInitialScheduler(); } } - } else if (equationSystemType == EquationSystemType::ReachabilityRewards) { - if (!direction || direction.get() == OptimizationDirection::Minimize) { - requirements.requireValidInitialScheduler(); + if (equationSystemType == EquationSystemType::ReachabilityRewards) { + if (!direction || direction.get() == OptimizationDirection::Minimize) { + requirements.requireValidInitialScheduler(); + } + } + } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration) { + if (equationSystemType == EquationSystemType::ReachabilityRewards) { + if (!direction || direction.get() == OptimizationDirection::Minimize) { + requirements.requireValidInitialScheduler(); + } + } + } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings::SolutionMethod::RationalSearch) { + if (equationSystemType == EquationSystemType::ReachabilityRewards) { + if (!direction || direction.get() == OptimizationDirection::Minimize) { + requirements.requireNoEndComponents(); + } } } - + return requirements; }