Add stopwatches

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;

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);
         }
 

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;
         }