From 2ea911f86570090b0291dd4f8cb308ad415cd565 Mon Sep 17 00:00:00 2001
From: Timo Philipp Gros <timopgros@gmail.com>
Date: Sat, 6 Jan 2018 17:09:02 +0100
Subject: [PATCH] finished version of implementation

---
 .../csl/helper/SparseMarkovAutomatonCslHelper.cpp           | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index ad95dee20..6fee0321e 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -372,19 +372,19 @@ namespace storm {
                                                                             storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const &minMaxLinearEquationSolverFactory) {
                 STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities.");
 
-                bool cycleFree;
+
 
                 std::ofstream logfile("U+logfile.txt", std::ios::app);
                 //logfile << "Using U+\n";
                 ValueType maxNorm = storm::utility::zero<ValueType>();
-                ValueType oldDiff = -storm::utility::zero<ValueType>();
 
                 //bitvectors to identify different kind of states
                 storm::storage::BitVector markovianStates = markovStates;
                 storm::storage::BitVector allStates(markovianStates.size(), true);
                 storm::storage::BitVector probabilisticStates = ~markovianStates;
 
-
+                storm::storage::StronglyConnectedComponentDecomposition<double> sccList(transitionMatrix, probabilisticStates, true, false);
+                bool cycleFree = sccList.size() == 0;
                 //vectors to save calculation
                 std::vector<std::vector<std::vector<ValueType>>> unifVectors{};