From 1536aeab4712336b5bf391399f8fbdc2b8aa0c57 Mon Sep 17 00:00:00 2001
From: Jip Spel <jip.spel@cs.rwth-aachen.de>
Date: Fri, 17 Aug 2018 12:01:19 +0200
Subject: [PATCH] Add keep track of time

---
 src/storm-pars-cli/storm-pars.cpp | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index ab240471f..d700ef4cd 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -466,6 +466,7 @@ namespace storm {
 
             if (parSettings.isMonotonicityAnalysisSet()) {
                 std::cout << "Hello, Jip1" << std::endl;
+                storm::utility::Stopwatch simplifyingWatch(true);
                 auto consideredModel = (model->as<storm::models::sparse::Dtmc<ValueType>>());
                 // TODO: check if it is a Dtmc
                 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(*consideredModel);
@@ -477,6 +478,9 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
                 }
                 model = simplifier.getSimplifiedModel();
+                simplifyingWatch.stop();
+                STORM_PRINT(std::endl << "Time for model simplification: " << simplifyingWatch << "." << std::endl << std::endl);
+                model->printModelInformationToStream(std::cout);
                 std::cout << "Bye, Jip1" << std::endl;
             }
 
@@ -491,7 +495,7 @@ namespace storm {
             if (parSettings.isMonotonicityAnalysisSet()) {
                 // Do something more fancy.
                 std::cout << "Hello, Jip2" << std::endl;
-
+                storm::utility::Stopwatch latticeWatch(true);
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
 
@@ -508,9 +512,14 @@ namespace storm {
                 // Transform to LatticeLattice
                 storm::storage::SparseMatrix<ValueType> matrix = sparseModel.get()->getTransitionMatrix();
                 storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice<ValueType>(matrix, topStates, bottomStates);
+
+                latticeWatch.stop();
+                STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl);
                 lattice->toString(std::cout);
 
                 // Monotonicity?
+                storm::utility::Stopwatch monotonicityWatch(true);
+
                 bool monotoneInAll = true;
                 for (uint_fast64_t i = 0; i < sparseModel.get()->getNumberOfStates(); ++i) {
                     // go over all rows
@@ -539,6 +548,8 @@ namespace storm {
 
 
                 }
+                monotonicityWatch.stop();
+                STORM_PRINT(std::endl << "Time for monotonicity: " << monotonicityWatch << "." << std::endl << std::endl);
                 if (monotoneInAll) {
                     std::cout << "Monotone increasing in all parameters" << std::endl;
                 }