From f098daf2f3fd0863311c51496c8c942db03a1a1e Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Mon, 8 Oct 2018 11:40:14 +0200
Subject: [PATCH] Add stopwatches

---
 src/storm-pars-cli/storm-pars.cpp               | 2 +-
 src/storm-pars/analysis/LatticeExtender.cpp     | 8 ++++++++
 src/storm-pars/analysis/MonotonicityChecker.cpp | 7 ++++++-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 0e4a61bf6..9e44097ee 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -531,7 +531,7 @@ namespace storm {
                 auto monotonicityChecker = storm::analysis::MonotonicityChecker<ValueType>(model, formulas, parSettings.isValidateAssumptionsSet());
                 monotonicityChecker.checkMonotonicity();
                 monotonicityWatch.stop();
-                STORM_PRINT(std::endl << "Time for monotonicity: " << monotonicityWatch << "." << std::endl
+                STORM_PRINT(std::endl << "Total time for monotonicity checking: " << monotonicityWatch << "." << std::endl
                                     << std::endl);
 
                 std::cout << "Bye, Jip2" << std::endl;
diff --git a/src/storm-pars/analysis/LatticeExtender.cpp b/src/storm-pars/analysis/LatticeExtender.cpp
index 324c8be8f..acb2a8952 100644
--- a/src/storm-pars/analysis/LatticeExtender.cpp
+++ b/src/storm-pars/analysis/LatticeExtender.cpp
@@ -22,6 +22,8 @@
 
 #include "storm/storage/BitVector.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/Stopwatch.h"
+
 
 namespace storm {
     namespace analysis {
@@ -46,6 +48,8 @@ namespace storm {
 
         template <typename ValueType>
         std::tuple<storm::analysis::Lattice*, uint_fast64_t, uint_fast64_t> LatticeExtender<ValueType>::toLattice(std::vector<std::shared_ptr<storm::logic::Formula const>> formulas) {
+            storm::utility::Stopwatch latticeWatch(true);
+
             STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
             STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula()
                             && ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()
@@ -92,6 +96,10 @@ namespace storm {
             for (auto state = initialMiddleStates.getNextSetIndex(0); state != numberOfStates; state = initialMiddleStates.getNextSetIndex(state + 1)) {
                 lattice->add(state);
             }
+
+
+            latticeWatch.stop();
+            STORM_PRINT(std::endl << "Time for initialization of lattice: " << latticeWatch << "." << std::endl << std::endl);
             return this->extendLattice(lattice);
         }
 
diff --git a/src/storm-pars/analysis/MonotonicityChecker.cpp b/src/storm-pars/analysis/MonotonicityChecker.cpp
index eb8d74bf2..2d99dcc45 100644
--- a/src/storm-pars/analysis/MonotonicityChecker.cpp
+++ b/src/storm-pars/analysis/MonotonicityChecker.cpp
@@ -49,6 +49,8 @@ namespace storm {
 
         template <typename ValueType>
         std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> MonotonicityChecker<ValueType>::checkMonotonicity(std::map<storm::analysis::Lattice*, std::vector<std::shared_ptr<storm::expressions::BinaryRelationExpression>>> map, storm::storage::SparseMatrix<ValueType> matrix) {
+            storm::utility::Stopwatch finalCheckWatch(true);
+
             auto i = 0;
             std::map<storm::analysis::Lattice*, std::map<carl::Variable, std::pair<bool, bool>>> result;
             for (auto itr = map.begin(); i < map.size() && itr != map.end(); ++itr) {
@@ -101,6 +103,9 @@ namespace storm {
                 }
                 ++i;
             }
+
+            finalCheckWatch.stop();
+            STORM_PRINT(std::endl << "Time for monotonicitycheck on lattice: " << finalCheckWatch << "." << std::endl << std::endl);
             return result;
         }
 
@@ -127,7 +132,7 @@ namespace storm {
             }
 
             latticeWatch.stop();
-            STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
+            STORM_PRINT(std::endl << "Total time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
             return result;
         }