From 8ba4f17a92484fe566188272d0ca24f98ce06312 Mon Sep 17 00:00:00 2001 From: hannah Date: Sun, 13 Jun 2021 18:53:46 +0200 Subject: [PATCH] ltl-mc with MAs --- .../SparseMarkovAutomatonCslModelChecker.cpp | 69 ++++++++++++++++++- .../SparseMarkovAutomatonCslModelChecker.h | 1 + 2 files changed, 68 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index e0844fbb8..cb8bf55ee 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -1,8 +1,9 @@ #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" - #include "storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h" + #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h" #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h" +#include "storm/modelchecker/helper/ltl/SparseLTLHelper.h" #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" @@ -13,16 +14,23 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/settings/modules/DebugSettings.h" + #include "storm/solver/SolveGoal.h" +#include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h" + #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/logic/FragmentSpecification.h" +#include "storm/logic/ExtractMaximalStateFormulasVisitor.h" #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/api/storm.h" + namespace storm { namespace modelchecker { template @@ -32,7 +40,7 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandleStatic(CheckTask const& checkTask, bool* requiresSingleInitialState) { - auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false); + auto singleObjectiveFragment = storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true).setRewardAccumulationAllowed(true).setInstantaneousFormulasAllowed(false).setNestedPathFormulasAllowed(true); //TODO (hannah) correct? auto multiObjectiveFragment = storm::logic::multiObjective().setTimeAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setRewardAccumulationAllowed(true); if (!storm::NumberTraits::SupportsExponential) { singleObjectiveFragment.setBoundedUntilFormulasAllowed(false).setCumulativeRewardFormulasAllowed(false); @@ -102,6 +110,63 @@ namespace storm { } return result; } + + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLTLProbabilities(Environment const& env, CheckTask const& checkTask) { + storm::logic::PathFormula const& pathFormula = checkTask.getFormula(); + + 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; + + // TODO correct? + 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..."); + + // TODO ? + 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(), this->getModel().getNumberOfStates()); + storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, embeddedMdp); + 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 + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index f18f4a374..360739171 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -29,6 +29,7 @@ namespace storm { virtual bool canHandle(CheckTask const& checkTask) const override; 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 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;