From 615b2b53993ad59b9b541d7c0e1fae5fd596450f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:25:15 +0200 Subject: [PATCH] (MDP-LTL) SparseMdpPrctlHelper: computeSurelyAcceptingPmaxStates --- .../prctl/helper/SparseMdpPrctlHelper.cpp | 106 ++++++++++++++++++ .../prctl/helper/SparseMdpPrctlHelper.h | 13 +++ 2 files changed, 119 insertions(+) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 17bef0ff8..c79f6c9ae 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -745,6 +745,112 @@ namespace storm { return result; } } + + 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); + } else if (acceptance.getAcceptanceExpression()->isFALSE()) { + STORM_LOG_INFO(" FALSE -> all states rejecting"); + return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false); + } + + std::vector> dnf = acceptance.extractFromDNF(); + + storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false); + + 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); + + for (auto const& literal : conjunction) { + STORM_LOG_INFO(" " << *literal); + if (literal->isTRUE()) { + // skip + } else if (literal->isFALSE()) { + allowed.clear(); + break; + } else if (literal->isAtom()) { + const cpphoafparser::AtomAcceptance& atom = literal->getAtom(); + if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) { + // only deal with FIN, ignore INF here + const storm::storage::BitVector& accSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet()); + if (atom.isNegated()) { + // allowed = allowed \ ~accSet = allowed & accSet + allowed &= accSet; + } else { + // allowed = allowed \ accSet = allowed & ~accSet + allowed &= ~accSet; + } + } + } + } + + if (allowed.empty()) { + // skip + continue; + } + + STORM_LOG_INFO(" Allowed states: " << allowed); + + // compute MECs in the allowed fragment + storm::storage::MaximalEndComponentDecomposition mecs(transitionMatrix, backwardTransitions, allowed); + for (const auto& mec : mecs) { + STORM_LOG_INFO("Inspect MEC: " << mec); + + bool accepting = true; + for (auto const& literal : conjunction) { + if (literal->isTRUE()) { + // skip + } else if (literal->isFALSE()) { + accepting = false; + break; + } else if (literal->isAtom()) { + const cpphoafparser::AtomAcceptance& atom = literal->getAtom(); + 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); + if (!mec.containsAnyState(~accSet)) { + STORM_LOG_INFO(" -> not satisfied"); + accepting = false; + break; + } + } else { + STORM_LOG_INFO("Checking against " << accSet); + if (!mec.containsAnyState(accSet)) { + STORM_LOG_INFO(" -> not satisfied"); + accepting = false; + break; + } + } + } else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) { + // do only sanity checks here + STORM_LOG_ASSERT(atom.isNegated() ? !mec.containsAnyState(~accSet) : !mec.containsAnyState(accSet), "MEC contains Fin-states, which should have been removed"); + } + } + } + + if (accepting) { + STORM_LOG_INFO("MEC is accepting"); + for (auto const& stateChoicePair : mec) { + acceptingStates.set(stateChoicePair.first); + } + } + + } + } + + STORM_LOG_INFO("Accepting states: " << acceptingStates); + return acceptingStates; + } template template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 099533dab..e70648186 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -10,6 +10,8 @@ #include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h" #include "MDPModelCheckingHelperReturnType.h" +#include "storm/automata/AcceptanceCondition.h" + #include "storm/utility/solver.h" #include "storm/solver/SolveGoal.h" @@ -47,6 +49,17 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, bool useMecBasedTechnique = false); + /*! + * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance conditon. + * More precisely, let + * accEC be the set of states that are contained in end components that satisfy the acceptance condition + * and let + * P1acc be the set of states that satisfy Pmax=1[ F accEC ]. + * This function then computes a set that contains accEC and is contained by P1acc. + * However, if the acceptance condition consists of 'true', the whole state space can be returned. + */ + static storm::storage::BitVector computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions); + template static std::vector computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount);