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(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 std::tuple LatticeExtender::toLattice(std::vector> 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 std::map>> MonotonicityChecker::checkMonotonicity(std::map>> map, storm::storage::SparseMatrix matrix) { + storm::utility::Stopwatch finalCheckWatch(true); + auto i = 0; std::map>> 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; }