diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp index c149a144f..f0c434ab2 100644 --- a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp +++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp @@ -7,11 +7,11 @@ namespace storm { namespace logic { - ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas, std::map& cachedFormulas) : extractedFormulas(extractedFormulas), cachedFormulas(cachedFormulas), nestingLevel(0) { + ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas) : extractedFormulas(extractedFormulas), nestingLevel(0) { } - std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, ApToFormulaMap& extractedFormulas, std::map& cachedFormulas) { - ExtractMaximalStateFormulasVisitor visitor(extractedFormulas, cachedFormulas); + std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, ApToFormulaMap& extractedFormulas) { + ExtractMaximalStateFormulasVisitor visitor(extractedFormulas); boost::any result = f.accept(visitor, boost::any()); return boost::any_cast>(result); } diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.h b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h index d1a188c3d..13c829dea 100644 --- a/src/storm/logic/ExtractMaximalStateFormulasVisitor.h +++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h @@ -6,12 +6,18 @@ namespace storm { namespace logic { - + class ExtractMaximalStateFormulasVisitor : public CloneVisitor { public: typedef std::map> ApToFormulaMap; - - static std::shared_ptr extract(PathFormula const& f, ApToFormulaMap& extractedFormulas, std::map& cachedFormulas); + + /*! + * Finds state subformulae in f and replaces them by atomic propositions. + * @param extractedFormulas will be the mapping of atomic propositions to the subformulae they replace + * @return the formula with replaced state subformulae + * @note identical subformulae will be replaced by the same atomic proposition + */ + static std::shared_ptr extract(PathFormula const& f, ApToFormulaMap& extractedFormulas); virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; @@ -28,7 +34,7 @@ namespace storm { virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; private: - ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas, std::map& cachedFormulas); + ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas); std::shared_ptr extract(std::shared_ptr f) const; void incrementNestingLevel() const; @@ -36,7 +42,7 @@ namespace storm { ApToFormulaMap& extractedFormulas; // A mapping from formula-strings to labels in order to use the same label for the equivalent formulas (as strings) - std::map& cachedFormulas; + mutable std::map cachedFormulas; std::size_t nestingLevel; }; diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index e83b692b7..baa780223 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -96,54 +96,35 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseCtmcCslModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); + + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); + storm::modelchecker::helper::SparseLTLHelper helper(probabilisticTransitions); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); + std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template 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); - storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted; - // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas - std::map cached; - std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); - - - const SparseCtmcModelType& ctmc = this->getModel(); - typedef typename storm::models::sparse::Dtmc SparseDtmcModelType; - - STORM_LOG_INFO("Computing 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 - storm::models::sparse::StateLabeling labeling(ctmc.getStateLabeling()); - - // 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"); - embeddedDtmc.writeDotToStream(modelDot); - modelDot.close(); - } - - storm::modelchecker::helper::SparseLTLHelper helper(embeddedDtmc.getTransitionMatrix()); - 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); + auto probabilisticTransitions = this->getModel().computeProbabilityMatrix(); + storm::modelchecker::helper::SparseLTLHelper helper(probabilisticTransitions); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); - // 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))); } - - + template std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index 48de3aa16..40b487eff 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -30,6 +30,8 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 5ebc3f8de..56a567359 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -111,57 +111,45 @@ namespace storm { return result; } + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); + + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); + std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(this->getModel()))); + } + return result; + } + template 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); - storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted; - // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas - std::map cached; - std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); - - const SparseMarkovAutomatonModelType& ma = this->getModel(); - typedef typename storm::models::sparse::Mdp SparseMdpModelType; - - STORM_LOG_INFO("Computing embedded MDP..."); - storm::storage::SparseMatrix probabilityMatrix = ma.getTransitionMatrix(); - // Copy of the state labelings of the MDP - storm::models::sparse::StateLabeling labeling(ma.getStateLabeling()); - // The embedded MDP, used for building the product and computing the probabilities in the product - SparseMdpModelType embeddedMdp(std::move(probabilityMatrix), std::move(labeling)); - - storm::solver::SolveGoal goal(embeddedMdp, checkTask); - - STORM_LOG_INFO("Performing ltl probability computations in embedded MDP..."); - - if (storm::settings::getModule().isTraceSet()) { - STORM_LOG_TRACE("Writing model to model.dot"); - std::ofstream modelDot("model.dot"); - embeddedMdp.writeDotToStream(modelDot); - modelDot.close(); - } - - storm::modelchecker::helper::SparseLTLHelper helper(embeddedMdp.getTransitionMatrix()); - 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); + 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 numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets); + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); if (checkTask.isProduceSchedulersSet()) { - result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(embeddedMdp))); + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(this->getModel()))); } - // We can directly return the numericResult vector as the state space of the CTMC and the embedded MDP are exactly the same return result; } - - + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 360739171..81f94bd7e 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -30,6 +30,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 8215aa4b3..6795e81b8 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -1,10 +1,14 @@ #include "SparseLTLHelper.h" #include "storm/automata/LTL2DeterministicAutomaton.h" +#include "storm/automata/DeterministicAutomaton.h" #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" +#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" +#include "storm/solver/SolveGoal.h" + #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/storage/memorystructure/MemoryStructure.h" @@ -108,18 +112,29 @@ namespace storm { } template - std::map SparseLTLHelper::computeApSets(std::map> 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::vector SparseLTLHelper::computeLTLProbabilities(Environment const &env, storm::logic::PathFormula const& formula, CheckFormulaCallback const& formulaChecker) { + // Replace state-subformulae by atomic propositions (APs) + storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(formula, extracted); + STORM_LOG_ASSERT(ltlFormula->isPathFormula(), "Unexpected formula type."); - std::unique_ptr subResultPointer = formulaChecker(p.second); - ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - auto sat = subResult.getTruthValuesVector(); + // Compute Satisfaction sets for the APs (which represent the state-subformulae + auto apSets = computeApSets(extracted, formulaChecker); + + STORM_LOG_INFO("Computing LTL probabilities for formula with " << apSets.size() << " atomic proposition(s)."); + + // Compute the resulting LTL probabilities + return computeLTLProbabilities(env, ltlFormula->asPathFormula(), apSets); - apSets[p.first] = std::move(sat); - STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << apSets[p.first].getNumberOfSetBits() << " states."); + } + + template + std::map SparseLTLHelper::computeApSets(std::map> const& extracted, CheckFormulaCallback const& formulaChecker) { + std::map apSets; + for (auto& p: extracted) { + STORM_LOG_DEBUG(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "..."); + apSets[p.first] = formulaChecker(*p.second); } return apSets; } @@ -579,7 +594,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::PathFormula 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) { diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 82d81c598..5a46b4bc9 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -1,16 +1,24 @@ #include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/automata/DeterministicAutomaton.h" + #include "storm/storage/SparseMatrix.h" -#include "storm/solver/SolveGoal.h" +#include "storm/storage/Scheduler.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" -#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" #include "storm/transformer/DAProductBuilder.h" namespace storm { + class Environment; + + namespace logic { + class Formula; + class PathFormula; + } + namespace automata { + class DeterministicAutomaton; + } + namespace modelchecker { namespace helper { @@ -24,6 +32,8 @@ namespace storm { public: + typedef std::function CheckFormulaCallback; + /*! * The type of the product automaton (DTMC or MDP) that is used during the computation. */ @@ -44,13 +54,22 @@ namespace storm { */ storm::storage::Scheduler extractScheduler(storm::models::sparse::Model const& model); + /*! + * Computes the LTL probabilities + * @param the LTL formula (allowing PCTL* like nesting) + * @param formulaChecker lambda that evaluates sub-formulas checks the provided formula and returns the set of states in which the formula holds + * @param the atomic propositions occuring in the formula together with the satisfaction sets + * @return a value for each state + */ + std::vector computeLTLProbabilities(Environment const &env, storm::logic::PathFormula const& formula, CheckFormulaCallback const& formulaChecker); + /*! * Computes the states that are satisfying the AP. - * @param mapping from Ap to formula - * @param lambda that checks the provided formula + * @param extracted mapping from Ap to formula + * @param formulaChecker lambda that checks the provided formula and returns the set of states in which the formula holds * @return mapping from AP to satisfaction sets */ - static std::map computeApSets(std::map> const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker); + static std::map computeApSets(std::map> const& extracted, CheckFormulaCallback const& formulaChecker); /*! * Computes the (maximizing) probabilities for the constructed DA product @@ -63,11 +82,11 @@ namespace storm { /*! * Computes the LTL probabilities - * @param the LTL formula - * @param the atomic propositions and satisfaction sets + * @param formula the LTL formula (without PCTL*-like nesting) + * @param apSatSets a mapping from all atomic propositions occuring in the formula to the corresponding satisfaction set * @return a value for each state */ - std::vector computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map& apSatSets); + std::vector computeLTLProbabilities(Environment const &env, storm::logic::PathFormula const& formula, std::map& apSatSets); private: /*! diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 5ee8fe1ce..4fb9802de 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -123,24 +123,14 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); - STORM_LOG_INFO("Obtaining HOA automaton..."); - storm::automata::DeterministicAutomaton::ptr da = pathFormula.readAutomaton(); - - STORM_LOG_INFO("Deterministic automaton from HOA file has " - << da->getNumberOfStates() << " states, " - << da->getAPSet().size() << " atomic propositions and " - << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); - - const SparseDtmcModelType& dtmc = this->getModel(); - storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix()); - storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc); - - // Compute Satisfaction sets for APs - storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted = pathFormula.getAPMapping(); - auto formulaChecker = [&] (std::shared_ptr const& formula) {return this->check(*formula); }; - std::map apSets = helper.computeApSets(extracted, formulaChecker); - - std::vector numericResult = helper.computeDAProductProbabilities(env, *da, apSets); + + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); + std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } @@ -148,30 +138,12 @@ 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); - storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted; - // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas - std::map cached; - std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); - - const SparseDtmcModelType& dtmc = this->getModel(); - - // TODO ? - if (storm::settings::getModule().isTraceSet()) { - STORM_LOG_TRACE("Writing model to model.dot"); - std::ofstream modelDot("model.dot"); - dtmc.writeDotToStream(modelDot); - modelDot.close(); - } - - storm::modelchecker::helper::SparseLTLHelper helper(dtmc.getTransitionMatrix()); - 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); + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, 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 2b8750c7d..874bb1c84 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -14,8 +14,6 @@ #include "storm/logic/FragmentSpecification.h" -#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" - #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" @@ -167,44 +165,45 @@ namespace storm { return result; } + template + std::unique_ptr SparseMdpPrctlModelChecker::computeHOAPathProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula(); + + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker); + std::vector numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets); + + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + if (checkTask.isProduceSchedulersSet()) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(this->getModel()))); + } + + return 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."); - STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula); - storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted; - // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas - std::map cached; - std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); - - const SparseMdpModelType& mdp = this->getModel(); - 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()); - 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); + storm::modelchecker::helper::SparseLTLHelper helper(this->getModel().getTransitionMatrix()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, this->getModel()); + + auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); }; + std::vector numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(numericResult))); if (checkTask.isProduceSchedulersSet()) { - result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(mdp))); + result->asExplicitQuantitativeCheckResult().setScheduler(std::make_unique>(helper.extractScheduler(this->getModel()))); } return result; } - + 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 2a56528ba..74358d334 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -41,6 +41,7 @@ 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 computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) override; + virtual std::unique_ptr computeHOAPathProbabilities(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;