From 04a8bec83f51bd8a370343baec3b7b4a0a2a298f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:25:16 +0200 Subject: [PATCH] (MDP-LTL) SparseMdpPrctlModelChecker: handle LTL Conflicts: src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp --- .../prctl/SparseMdpPrctlModelChecker.cpp | 155 +++++++++++++++++- .../prctl/SparseMdpPrctlModelChecker.h | 5 + .../prctl/helper/SparseMdpPrctlHelper.cpp | 27 +-- 3 files changed, 174 insertions(+), 13 deletions(-) diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index a56a8b3ef..31b3a5c1d 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -1,5 +1,7 @@ #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include + #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -12,6 +14,10 @@ #include "storm/logic/FragmentSpecification.h" +#include "storm/transformer/DAProductBuilder.h" +#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" +#include "storm/automata/LTL2DeterministicAutomaton.h" + #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" @@ -23,12 +29,14 @@ #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" #include "storm/solver/SolveGoal.h" - #include "storm/storage/BitVector.h" #include "storm/shields/ShieldHandling.h" +#include "storm/settings/SettingsManager.h" + #include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/DebugSettings.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -48,7 +56,7 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { + if (formula.isInFragment(storm::logic::prctlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) { return true; } else if (checkTask.isOnlyInitialStatesRelevantSet()) { auto multiObjectiveFragment = storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setRewardAccumulationAllowed(true); @@ -169,6 +177,149 @@ namespace storm { return std::make_unique>(result); } + template + std::unique_ptr SparseMdpPrctlModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + + std::vector extracted; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted); + + STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula); + + std::map apSets; + + for (auto& p : extracted) { + STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); + + std::unique_ptr subResultPointer = this->check(env, *p.second); + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto sat = subResult.getTruthValuesVector(); + + STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); + + apSets[p.first] = std::move(sat); + } + + bool minimize = false; + CheckTask subTask(checkTask); + + if (checkTask.getOptimizationDirection() == OptimizationDirection::Minimize) { + minimize = true; + // negate + ltlFormula = std::make_shared(storm::logic::UnaryBooleanOperatorType::Not, ltlFormula); + STORM_LOG_INFO("Computing Pmin, proceeding with negated LTL formula."); + + subTask = checkTask.negate().substituteFormula(*ltlFormula); + } else { + subTask = checkTask.substituteFormula(*ltlFormula); + } + + STORM_LOG_INFO("Resulting LTL path formula: " << *ltlFormula); + STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString()); + + std::shared_ptr da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula); + + STORM_LOG_INFO("Deterministic automaton for LTL formula has " + << da->getNumberOfStates() << " states, " + << da->getAPSet().size() << " atomic propositions and " + << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); + + const SparseMdpModelType& mdp = this->getModel(); + storm::solver::SolveGoal goal(mdp, subTask); + + std::vector numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); + + if (minimize) { + // compute 1-Pmax[!ltl] + for (auto& value : numericResult) { + value = storm::utility::one() - value; + } + } + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + + + template + std::vector::ValueType> SparseMdpPrctlModelChecker::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal::ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) const { + STORM_LOG_THROW(goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP"); + + const storm::automata::APSet& apSet = da.getAPSet(); + + std::vector apLabels; + for (const std::string& ap : apSet.getAPs()) { + auto it = apSatSets.find(ap); + STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula"); + + apLabels.push_back(std::move(it->second)); + } + + const SparseMdpModelType& mdp = this->getModel(); + + storm::storage::BitVector statesOfInterest; + if (goal.hasRelevantValues()) { + statesOfInterest = goal.relevantValues(); + } else { + // product from all model states + statesOfInterest = storm::storage::BitVector(mdp.getNumberOfStates(), true); + } + + STORM_LOG_INFO("Building MDP-DA product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); + storm::transformer::DAProductBuilder productBuilder(da, apLabels); + auto product = productBuilder.build(mdp, statesOfInterest); + STORM_LOG_INFO("Product MDP has " << product->getProductModel().getNumberOfStates() << " states and " + << product->getProductModel().getNumberOfTransitions() << " transitions."); + + if (storm::settings::getModule().isTraceSet()) { + STORM_LOG_TRACE("Writing model to model.dot"); + std::ofstream modelDot("model.dot"); + mdp.writeDotToStream(modelDot); + modelDot.close(); + + STORM_LOG_TRACE("Writing product model to product.dot"); + std::ofstream productDot("product.dot"); + product->getProductModel().writeDotToStream(productDot); + productDot.close(); + + STORM_LOG_TRACE("Product model mapping:"); + std::stringstream str; + product->printMapping(str); + STORM_LOG_TRACE(str.str()); + } + + STORM_LOG_INFO("Computing accepting end components..."); + storm::storage::BitVector accepting = storm::modelchecker::helper::SparseMdpPrctlHelper::computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); + if (accepting.empty()) { + STORM_LOG_INFO("No accepting states, skipping probability computation."); + std::vector numericResult(this->getModel().getNumberOfStates(), storm::utility::zero()); + return numericResult; + } + + STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs..."); + + storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); + + storm::solver::SolveGoal solveGoalProduct(goal); + storm::storage::BitVector soiProduct(product->getStatesOfInterest()); + solveGoalProduct.setRelevantValues(std::move(soiProduct)); + + std::vector prodNumericResult + = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, + std::move(solveGoalProduct), + product->getProductModel().getTransitionMatrix(), + product->getProductModel().getBackwardTransitions(), + bvTrue, + accepting, + qualitative, + false // no schedulers (at the moment) + ).values); + + std::vector numericResult = product->projectToOriginalModel(this->getModel(), prodNumericResult); + return numericResult; + } + + template std::unique_ptr SparseMdpPrctlModelChecker::computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index ad164df32..73e706596 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -4,6 +4,8 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/models/sparse/Mdp.h" #include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/solver/SolveGoal.h" + namespace storm { @@ -39,9 +41,12 @@ namespace storm { virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeStateFormulaProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkMultiObjectiveFormula(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr checkQuantileFormula(Environment const& env, CheckTask const& checkTask) override; + private: + std::vector computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) const; }; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index c79f6c9ae..2e4cb8894 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -749,7 +749,6 @@ namespace storm { template storm::storage::BitVector SparseMdpPrctlHelper::computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions) { STORM_LOG_INFO("Computing accepting states for acceptance condition " << *acceptance.getAcceptanceExpression()); - std::cout << transitionMatrix.getRowGroupCount() << std::endl; if (acceptance.getAcceptanceExpression()->isTRUE()) { STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)"); return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); @@ -762,16 +761,18 @@ namespace storm { storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false); + std::size_t accMECs = 0; + std::size_t allMECs = 0; std::size_t i = 0; for (auto const& conjunction : dnf) { // determine the set of states of the subMDP that can satisfy the condition // => remove all states that would violate Fins in the conjunction storm::storage::BitVector allowed(transitionMatrix.getRowGroupCount(), true); - STORM_LOG_INFO("Handle conjunction " << i); + STORM_LOG_DEBUG("Handle conjunction " << i); for (auto const& literal : conjunction) { - STORM_LOG_INFO(" " << *literal); + STORM_LOG_DEBUG(" " << *literal); if (literal->isTRUE()) { // skip } else if (literal->isFALSE()) { @@ -798,12 +799,13 @@ namespace storm { continue; } - STORM_LOG_INFO(" Allowed states: " << allowed); + STORM_LOG_DEBUG(" Allowed states: " << allowed); // compute MECs in the allowed fragment storm::storage::MaximalEndComponentDecomposition mecs(transitionMatrix, backwardTransitions, allowed); + allMECs += mecs.size(); for (const auto& mec : mecs) { - STORM_LOG_INFO("Inspect MEC: " << mec); + STORM_LOG_DEBUG("Inspect MEC: " << mec); bool accepting = true; for (auto const& literal : conjunction) { @@ -817,16 +819,16 @@ namespace storm { const storm::storage::BitVector& accSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet()); if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_INF) { if (atom.isNegated()) { - STORM_LOG_INFO("Checking against " << ~accSet); + STORM_LOG_DEBUG("Checking against " << ~accSet); if (!mec.containsAnyState(~accSet)) { - STORM_LOG_INFO(" -> not satisfied"); + STORM_LOG_DEBUG(" -> not satisfied"); accepting = false; break; } } else { - STORM_LOG_INFO("Checking against " << accSet); + STORM_LOG_DEBUG("Checking against " << accSet); if (!mec.containsAnyState(accSet)) { - STORM_LOG_INFO(" -> not satisfied"); + STORM_LOG_DEBUG(" -> not satisfied"); accepting = false; break; } @@ -839,7 +841,8 @@ namespace storm { } if (accepting) { - STORM_LOG_INFO("MEC is accepting"); + accMECs++; + STORM_LOG_DEBUG("MEC is accepting"); for (auto const& stateChoicePair : mec) { acceptingStates.set(stateChoicePair.first); } @@ -848,7 +851,9 @@ namespace storm { } } - STORM_LOG_INFO("Accepting states: " << acceptingStates); + STORM_LOG_DEBUG("Accepting states: " << acceptingStates); + STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs)."); + return acceptingStates; }