From 75ddf49f2bc0a0518707e13fc838b70d86e64d62 Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 17 Jun 2021 13:23:38 +0200 Subject: [PATCH] compute SatSets via LTLHelper --- .../csl/SparseCtmcCslModelChecker.cpp | 32 ++++------- .../SparseMarkovAutomatonCslModelChecker.cpp | 23 ++------ .../helper/ltl/SparseLTLHelper.cpp | 21 ++++++- .../modelchecker/helper/ltl/SparseLTLHelper.h | 14 ++++- .../prctl/SparseDtmcPrctlModelChecker.cpp | 22 +++----- .../prctl/SparseMdpPrctlModelChecker.cpp | 56 +++---------------- 6 files changed, 66 insertions(+), 102 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index b36663dc9..995c06856 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -100,40 +100,27 @@ namespace storm { std::unique_ptr SparseCtmcCslModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula); 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; - // TODO simplify APs - 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); - } const SparseCtmcModelType& ctmc = this->getModel(); typedef typename storm::models::sparse::Dtmc SparseDtmcModelType; STORM_LOG_INFO("Computing embedded DTMC..."); - // compute probability matrix (embedded DTMC) + // Compute probability matrix (embedded DTMC) storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(ctmc.getTransitionMatrix(), ctmc.getExitRateVector()); - // copy of the state labelings of the CTMC + // Copy of the state labelings of the CTMC storm::models::sparse::StateLabeling labeling(ctmc.getStateLabeling()); - // the embedded DTMC, used for building the product and computing the probabilities in the product + // The embedded DTMC, used for building the product and computing the probabilities in the product SparseDtmcModelType embeddedDtmc(std::move(probabilityMatrix), std::move(labeling)); storm::solver::SolveGoal goal(embeddedDtmc, checkTask); STORM_LOG_INFO("Performing ltl probability computations in embedded DTMC..."); + // TODO ? if (storm::settings::getModule().isTraceSet()) { STORM_LOG_TRACE("Writing model to model.dot"); std::ofstream modelDot("model.dot"); @@ -141,11 +128,16 @@ namespace storm { modelDot.close(); } - storm::modelchecker::helper::SparseLTLHelper helper(embeddedDtmc.getTransitionMatrix(), this->getModel().getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(embeddedDtmc.getTransitionMatrix(), embeddedDtmc.getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, embeddedDtmc); + + // Compute Satisfaction sets for APs + auto formulaChecker = [&] (std::shared_ptr const& formula) { return this->check(env, *formula); }; + std::map apSets = helper.computeApSets(extracted, formulaChecker); + std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); - // we can directly return the numericResult vector as the state space of the CTMC and the embedded DTMC are exactly the same + // We can directly return the numericResult vector as the state space of the CTMC and the embedded DTMC are exactly the same return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 1a9c9fe55..90c13cf61 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -116,26 +116,10 @@ namespace storm { std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula); 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; - - // TODO simplify APs - 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); - } - const SparseMarkovAutomatonModelType& ma = this->getModel(); typedef typename storm::models::sparse::Mdp SparseMdpModelType; @@ -161,6 +145,11 @@ namespace storm { storm::modelchecker::helper::SparseLTLHelper helper(embeddedMdp.getTransitionMatrix(), this->getModel().getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, embeddedMdp); + + // Compute Satisfaction sets for APs + auto formulaChecker = [&] (std::shared_ptr const& formula) { return this->check(env, *formula); }; + std::map apSets = helper.computeApSets(extracted, formulaChecker); + std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); // We can directly return the numericResult vector as the state space of the CTMC and the embedded MDP are exactly the same diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 080e6bc0a..925f0ec3b 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -1,3 +1,5 @@ +#include +#include #include "SparseLTLHelper.h" #include "storm/transformer/DAProductBuilder.h" @@ -259,7 +261,7 @@ namespace storm { template - std::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets) { + std::vector SparseLTLHelper::computeLTLProbabilities(Environment const& env, storm::logic::Formula const& formula, std::map& apSatSets) { std::shared_ptr ltlFormula; STORM_LOG_THROW((!Nondeterministic) || this->isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); if (Nondeterministic && this->getOptimizationDirection() == OptimizationDirection::Minimize) { @@ -294,6 +296,23 @@ namespace storm { return numericResult; } + template + std::map SparseLTLHelper::computeApSets(std::vector const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker){ + std::map apSets; + for (auto& p : extracted) { + STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); + + std::unique_ptr subResultPointer = formulaChecker(p.second); + + ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); + auto sat = subResult.getTruthValuesVector(); + + apSets[p.first] = std::move(sat); + STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); + } + return apSets; + } + template class SparseLTLHelper; template class SparseLTLHelper; diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 7774daf01..44e618644 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -4,6 +4,7 @@ #include "storm/solver/SolveGoal.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" namespace storm { @@ -27,6 +28,7 @@ namespace storm { using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::type; + /*! * Initializes the helper for a discrete time model (i.e. DTMC, MDP) * @param the transition matrix of the model @@ -43,6 +45,16 @@ namespace storm { */ std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); + /*! + * todo computes Sat sets of AP + * @param + * @param + * @return + */ + std::map computeApSets(std::vector const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker); + + + private: /*! * Computes the (maximizing) probabilities for the constructed DA product * @param the DA to build the product with @@ -53,8 +65,6 @@ namespace storm { std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets); - private: - /*! * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF). * More precisely, let diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index fedbb5895..70f7cd475 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -146,6 +146,7 @@ namespace storm { const SparseDtmcModelType& dtmc = this->getModel(); storm::solver::SolveGoal goal(dtmc, checkTask); + // TODO HOA call LTL helper std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -154,24 +155,10 @@ namespace storm { std::unique_ptr SparseDtmcPrctlModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula); 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); - // TODO simplify APs - 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); - } - const SparseDtmcModelType& dtmc = this->getModel(); // TODO ? @@ -184,6 +171,11 @@ namespace storm { storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); + + // Compute Satisfaction sets for APs + auto formulaChecker = [&] (std::shared_ptr const& formula) { return this->check(env, *formula); }; + std::map apSets = helper.computeApSets(extracted, formulaChecker); + 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 cc63d179a..500e893ea 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -184,56 +184,13 @@ namespace storm { STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula); 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; - std::map substitution; - - // TODO Maintain a mapping from APsets to labels in order to use the same label for the same formulas - std::map labels; - - 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."); - - - auto occ = labels.find(sat); - if(occ != labels.end()){ - // Reuse AP - STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is equivalent to " << occ->second << ", substituting..."); - substitution[p.first] = occ->second; - continue; - } - /*// equivalent to !pi - occ = labels.find(~sat); - if(occ != labels.end()){ - // Reuse negated AP - STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is equivalent to !" << occ->second << ", substituting..."); - substitution[p.first] = todo: ! occ->second; - continue; - } - */ - - labels[sat] = p.first; - apSets[p.first] = std::move(sat); - STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states."); - } - - ltlFormula = ltlFormula->substitute(substitution); - const SparseMdpModelType& mdp = this->getModel(); - - // TODO + // TODO ? if (storm::settings::getModule().isTraceSet()) { STORM_LOG_TRACE("Writing model to model.dot"); std::ofstream modelDot("model.dot"); @@ -241,8 +198,13 @@ namespace storm { modelDot.close(); } - storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix(), this->getModel().getNumberOfStates()); + storm::modelchecker::helper::SparseLTLHelper helper(mdp.getTransitionMatrix(), mdp.getNumberOfStates()); storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, mdp); + + // Compute Satisfaction sets for APs + auto formulaChecker = [&] (std::shared_ptr const& formula) { return this->check(env, *formula); }; + std::map apSets = helper.computeApSets(extracted, formulaChecker); + std::vector numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult)));