From fc0ae2ea4bf09be74ec542f8aafc995d89a2bfef Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 20 May 2021 23:41:11 +0200 Subject: [PATCH] removed SolveGoal in function computeLTLproabilities of SparseLTLHelper --- .../helper/ltl/SparseLTLHelper.cpp | 245 +++++++++++++----- .../modelchecker/helper/ltl/SparseLTLHelper.h | 21 +- .../prctl/SparseDtmcPrctlModelChecker.cpp | 11 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 12 +- .../prctl/helper/SparseMdpPrctlHelper.cpp | 111 -------- .../prctl/helper/SparseMdpPrctlHelper.h | 11 - 6 files changed, 222 insertions(+), 189 deletions(-) diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 8182289ce..86841f63f 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -7,6 +7,7 @@ #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" +#include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/DebugSettings.h" @@ -21,11 +22,143 @@ namespace storm { // Intentionally left empty. } - template - std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) { - STORM_LOG_THROW((!Nondeterministic) || goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP"); + // todo only for MDP and change name! + template + storm::storage::BitVector SparseLTLHelper::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()); + 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 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); + + 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_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_DEBUG("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_DEBUG("Checking against " << ~accSet); + if (!mec.containsAnyState(~accSet)) { + STORM_LOG_DEBUG(" -> not satisfied"); + accepting = false; + break; + } + } else { + STORM_LOG_DEBUG("Checking against " << accSet); + if (!mec.containsAnyState(accSet)) { + STORM_LOG_DEBUG(" -> 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) { + accMECs++; + STORM_LOG_DEBUG("MEC is accepting"); + for (auto const& stateChoicePair : mec) { + acceptingStates.set(stateChoicePair.first); + } + } + + } + } + + STORM_LOG_DEBUG("Accepting states: " << acceptingStates); + STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs)."); + + return acceptingStates; + } + + // todo only for dtmc and change name! + template + storm::storage::BitVector SparseLTLHelper::computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix) { + storm::storage::StronglyConnectedComponentDecomposition bottomSccs(transitionMatrix, storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs()); + //storm::storage::BitVector acceptingStates = storm::storage::BitVector(product->getProductModel().getNumberOfStates()); + storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false); + + std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0; + for (auto& scc : bottomSccs) { + checkedBSCCs++; + if (acceptance.isAccepting(scc)) { + acceptingBSCCs++; + for (auto& state : scc) { + acceptingStates.set(state); + acceptingBSCCStates++; + } + } + } + STORM_LOG_INFO("BSCC analysis: " << acceptingBSCCs << " of " << checkedBSCCs << " BSCCs were acceptingStates (" << acceptingBSCCStates << " states in acceptingStates BSCCs)."); + return acceptingStates; + } + template + std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) { const storm::automata::APSet& apSet = da.getAPSet(); std::vector apLabels; @@ -37,28 +170,25 @@ namespace storm { } storm::storage::BitVector statesOfInterest; - if (goal.hasRelevantValues()) { - statesOfInterest = goal.relevantValues(); + + if (this->hasRelevantStates()) { + statesOfInterest = this->getRelevantStates(); } else { // product from all model states statesOfInterest = storm::storage::BitVector(this->_numberOfStates, true); } + // todo change text STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states..."); storm::transformer::DAProductBuilder productBuilder(da, apLabels); auto product = productBuilder.build(this->_transitionMatrix, statesOfInterest); - STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC")) +" has " << product->getProductModel().getNumberOfStates() << " states and " + STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +" 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"); - // this->_model.writeDotToStream(modelDot); // TODO - modelDot.close(); - STORM_LOG_TRACE("Writing product model to product.dot"); std::ofstream productDot("product.dot"); product->getProductModel().writeDotToStream(productDot); @@ -70,75 +200,63 @@ namespace storm { STORM_LOG_TRACE(str.str()); } - // DTMC: BCC // MDP: computeSurelyAcceptingPmaxStates - storm::storage::BitVector accepting; + storm::storage::BitVector acceptingStates; if (Nondeterministic) { STORM_LOG_INFO("Computing accepting end components..."); - 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->_numberOfStates, storm::utility::zero()); - return numericResult; - } + // todo compute accepting states, same as below + acceptingStates = computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions()); + } else { STORM_LOG_INFO("Computing BSCCs and checking for acceptance..."); + // todo compute accepting states, (no btm) + acceptingStates = computeAcceptingComponentStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix()); - storm::storage::StronglyConnectedComponentDecomposition bottomSccs(product->getProductModel().getTransitionMatrix(), - storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs()); - accepting = storm::storage::BitVector(product->getProductModel().getNumberOfStates()); - std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0; - for (auto& scc : bottomSccs) { - checkedBSCCs++; - if (product->getAcceptance()->isAccepting(scc)) { - acceptingBSCCs++; - for (auto& state : scc) { - accepting.set(state); - acceptingBSCCStates++; - } - } - } - - STORM_LOG_INFO("BSCC analysis: " << acceptingBSCCs << " of " << checkedBSCCs << " BSCCs were accepting (" << acceptingBSCCStates << " states in accepting BSCCs)."); + } - if (acceptingBSCCs == 0) { - STORM_LOG_INFO("No accepting BSCCs, skipping probability computation."); - std::vector numericResult(this->_numberOfStates, storm::utility::zero()); - return numericResult; - } + if (acceptingStates.empty()) { + STORM_LOG_INFO("No acceptingStates states, skipping probability computation."); + std::vector numericResult(this->_numberOfStates, storm::utility::zero()); + return numericResult; } - STORM_LOG_INFO("Computing probabilities for reaching accepting components..."); + STORM_LOG_INFO("Computing probabilities for reaching acceptingStates components..."); storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); - - storm::solver::SolveGoal solveGoalProduct(goal); storm::storage::BitVector soiProduct(product->getStatesOfInterest()); - solveGoalProduct.setRelevantValues(std::move(soiProduct)); + + // Create goal for computeUntilProbabilities, compute maximizing probabilties for DA product with MDP + storm::solver::SolveGoal solveGoalProduct; + if (this->isValueThresholdSet()) { + solveGoalProduct = storm::solver::SolveGoal(OptimizationDirection::Maximize, this->getValueThresholdComparisonType(), this->getValueThresholdValue(), std::move(soiProduct)); + } else { + solveGoalProduct = storm::solver::SolveGoal(OptimizationDirection::Maximize); + solveGoalProduct.setRelevantValues(std::move(soiProduct)); + } std::vector prodNumericResult; if (Nondeterministic) { 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) + std::move(solveGoalProduct), + product->getProductModel().getTransitionMatrix(), + product->getProductModel().getBackwardTransitions(), + bvTrue, + acceptingStates, + qualitative, + false // no schedulers (at the moment) ).values); } else { prodNumericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, - std::move(solveGoalProduct), - product->getProductModel().getTransitionMatrix(), - product->getProductModel().getBackwardTransitions(), - bvTrue, - accepting, - qualitative); + std::move(solveGoalProduct), + product->getProductModel().getTransitionMatrix(), + product->getProductModel().getBackwardTransitions(), + bvTrue, + acceptingStates, + qualitative); } std::vector numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult); @@ -146,8 +264,12 @@ namespace storm { } + //todo remove goal? template - std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal&& goal, storm::logic::Formula const& ltlFormula, std::map& apSatSets) { + std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& ltlFormula, std::map& apSatSets) { + // TODO optDir: helper.getOptimizationDirection for MDP + // negate formula etc ~ap? + STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula); STORM_LOG_INFO(" in prefix format: " << ltlFormula.toPrefixString()); @@ -159,10 +281,11 @@ namespace storm { << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); - std::vector numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSatSets, this->isQualitativeSet()); + //todo remove goal here? send dir instead? + std::vector numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet()); - // TODO - /* + // TODO optDir: helper.getOptimizationDirection for MDP + /* //for any path formula ψ: pmin(s, ψ) = 1- pmax(s, ¬ψ) if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { // compute 1-Pmax[!ltl] for (auto& value : numericResult) { diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 42bf322cc..3e69b6f8d 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -35,19 +35,36 @@ namespace storm { /*! * todo + * Computes maximizing(!) probabilties for DA product with MDP * @return */ - std::vector computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative); + std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative); /*! * Computes the ltl probabilities ...todo * @return a value for each state */ - std::vector computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal&& goal, storm::logic::Formula const& f, std::map& apSatSets); //todo was brauchen wir hier aps und ..? + std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& f, std::map& apSatSets); //todo was brauchen wir hier aps und ..? private: + + /*! todo only relevant for MDP - enable_if_t ? + * 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); + + //todo only for dtmc, different to mdp: no backward tm + static storm::storage::BitVector computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix const& transitionMatrix); + + storm::storage::SparseMatrix const& _transitionMatrix; std::size_t _numberOfStates; diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 66b726bce..28009225c 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -162,7 +162,6 @@ namespace storm { STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula); std::map apSets; - // todo apSets = computeApSets(env, checkTask); for (auto& p : extracted) { STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); @@ -177,9 +176,17 @@ namespace storm { const SparseDtmcModelType& dtmc = this->getModel(); + // TODO + if (storm::settings::getModule().isTraceSet()) { + STORM_LOG_TRACE("Writing model to model.dot"); + std::ofstream modelDot("model.dot"); + this->getModel().writeDotToStream(modelDot); + modelDot.close(); + } + storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); - std::vector numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), *ltlFormula, apSets); + std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 6f0bc270a..85f89bf18 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -217,11 +217,19 @@ namespace storm { } const SparseMdpModelType& mdp = this->getModel(); - storm::solver::SolveGoal goal(mdp, subTask); + storm::solver::SolveGoal goal(mdp, subTask); //todo remove, infos now in helper, see below + + // TODO + if (storm::settings::getModule().isTraceSet()) { + STORM_LOG_TRACE("Writing model to model.dot"); + std::ofstream modelDot("model.dot"); + this->getModel().writeDotToStream(modelDot); + modelDot.close(); + } storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix(), this->getModel().getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, subTask, mdp); - std::vector numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal(this->getModel(), subTask), *ltlFormula, apSets); + std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); if(minimize) { // compute 1-Pmax[!ltl] diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 2e4cb8894..17bef0ff8 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -745,117 +745,6 @@ 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()); - 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 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_DEBUG("Handle conjunction " << i); - - for (auto const& literal : conjunction) { - STORM_LOG_DEBUG(" " << *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_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_DEBUG("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_DEBUG("Checking against " << ~accSet); - if (!mec.containsAnyState(~accSet)) { - STORM_LOG_DEBUG(" -> not satisfied"); - accepting = false; - break; - } - } else { - STORM_LOG_DEBUG("Checking against " << accSet); - if (!mec.containsAnyState(accSet)) { - STORM_LOG_DEBUG(" -> 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) { - accMECs++; - STORM_LOG_DEBUG("MEC is accepting"); - for (auto const& stateChoicePair : mec) { - acceptingStates.set(stateChoicePair.first); - } - } - - } - } - - STORM_LOG_DEBUG("Accepting states: " << acceptingStates); - STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs)."); - - return acceptingStates; - } template template diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index e70648186..ea38383f0 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -48,17 +48,6 @@ namespace storm { static MDPSparseModelCheckingHelperReturnType computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); 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);