From 78058b515297fb46e67732150f694523ffde466b Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Sun, 13 Jun 2021 18:47:33 +0200
Subject: [PATCH] ltl-mc with ctmcs

 Conflicts:
	src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
---
 .../csl/SparseCtmcCslModelChecker.cpp         | 33 +++++++++++--------
 1 file changed, 20 insertions(+), 13 deletions(-)

diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
index 5b296a5a2..4d3dab7ec 100644
--- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
+++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
@@ -16,7 +16,10 @@
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "storm/modelchecker/helper/ltl/SparseLTLHelper.h"
+
 #include "storm/logic/FragmentSpecification.h"
+#include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 
@@ -24,6 +27,10 @@
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/NotImplementedException.h"
 
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
+
 namespace storm {
     namespace modelchecker {
         template <typename SparseCtmcModelType>
@@ -99,7 +106,7 @@ namespace storm {
             STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula);
 
             std::map<std::string, storm::storage::BitVector> apSets;
-
+            // TODO simplify APs
             for (auto& p : extracted) {
                 STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
 
@@ -112,16 +119,6 @@ namespace storm {
                 apSets[p.first] = std::move(sat);
             }
 
-            STORM_LOG_INFO("Resulting LTL path formula: " << *ltlFormula);
-            STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString());
-
-            std::shared_ptr<storm::automata::DeterministicAutomaton> da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula, false);
-
-            STORM_LOG_INFO("Deterministic automaton for LTL formula has "
-                    << da->getNumberOfStates() << " states, "
-                    << da->getAPSet().size() << " atomic propositions and "
-                    << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
-
             const SparseCtmcModelType& ctmc = this->getModel();
             typedef typename storm::models::sparse::Dtmc<typename SparseCtmcModelType::ValueType> SparseDtmcModelType;
 
@@ -135,9 +132,19 @@ namespace storm {
             SparseDtmcModelType embeddedDtmc(std::move(probabilityMatrix), std::move(labeling));
             storm::solver::SolveGoal<ValueType> goal(embeddedDtmc, checkTask);
 
+            STORM_LOG_INFO("Performing ltl probability computations in embedded DTMC...");
+
+            if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
+                STORM_LOG_TRACE("Writing model to model.dot");
+                std::ofstream modelDot("model.dot");
+                embeddedDtmc.writeDotToStream(modelDot);
+                modelDot.close();
+            }
+
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(embeddedDtmc.getTransitionMatrix(), this->getModel().getNumberOfStates());
+            storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, embeddedDtmc);
+            std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
-            STORM_LOG_INFO("Performing DA product and probability computations in embedded DTMC...");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeDAProductProbabilities(env, embeddedDtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet());
             // 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<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }