output of runtimes and other statistics

Former-commit-id: 3eaf89f5d5

examples/multi-objective/mdp/benchmarks_numerical.sh

@@ -3,10 +3,41 @@
 mkdir benchmarks_numerical
 
 
+executable=../../../build/src/Release/storm 
+options='--precision 0.000001 --multiObjective:precision 0.0001'
+modelcommand='-s'
+propertycommand='-prop'
+logfilepostfix='.storm.output'
+$executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_3_2$logfilepostfix 
+$executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_4_2$logfilepostfix 
+$executable $modelcommand consensus/consensus2_5_2.nm $propertycommand consensus/consensus2_5_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_5_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_3_2.nm $propertycommand consensus/consensus3_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_3_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_4_2.nm $propertycommand consensus/consensus3_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_4_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_5_2.nm $propertycommand consensus/consensus3_5_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_5_2$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf4.nm $propertycommand zeroconf/zeroconf4_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf4$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf6.nm $propertycommand zeroconf/zeroconf6_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf6$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf8.nm $propertycommand zeroconf/zeroconf8_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf8$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb2_14.nm $propertycommand zeroconf-tb/zeroconf-tb2_14_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb2_14$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb4_10.nm $propertycommand zeroconf-tb/zeroconf-tb4_10_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb4_10$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb4_14.nm $propertycommand zeroconf-tb/zeroconf-tb4_14_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb4_14$logfilepostfix 
+$executable $modelcommand team/team2obj_3.nm $propertycommand team/team2obj_3_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_3$logfilepostfix 
+$executable $modelcommand team/team3obj_3.nm $propertycommand team/team3obj_3_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_3$logfilepostfix 
+$executable $modelcommand team/team2obj_4.nm $propertycommand team/team2obj_4_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_4$logfilepostfix 
+$executable $modelcommand team/team3obj_4.nm $propertycommand team/team3obj_4_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_4$logfilepostfix 
+$executable $modelcommand team/team2obj_5.nm $propertycommand team/team2obj_5_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_5$logfilepostfix 
+$executable $modelcommand team/team3obj_5.nm $propertycommand team/team3obj_5_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_5$logfilepostfix 
+$executable $modelcommand scheduler/scheduler05.nm $propertycommand scheduler/scheduler05_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler05$logfilepostfix 
+$executable $modelcommand scheduler/scheduler25.nm $propertycommand scheduler/scheduler25_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler25$logfilepostfix 
+$executable $modelcommand scheduler/scheduler50.nm $propertycommand scheduler/scheduler50_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler50$logfilepostfix 
+$executable $modelcommand dpm/dpm100.nm $propertycommand dpm/dpm100_numerical.pctl $options | tee  benchmarks_numerical/7_dpm100$logfilepostfix 
+$executable $modelcommand dpm/dpm200.nm $propertycommand dpm/dpm200_numerical.pctl $options | tee  benchmarks_numerical/7_dpm200$logfilepostfix 
+$executable $modelcommand dpm/dpm300.nm $propertycommand dpm/dpm300_numerical.pctl $options | tee  benchmarks_numerical/7_dpm300$logfilepostfix 
+
+
 executable=../../../../prism/prism-4.3-src/bin/prism 
 options='-epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g'
-modelcommand=
-propertycommand=
+modelcommand=''
+propertycommand=''
 logfilepostfix='.prism.output'
 $executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_3_2$logfilepostfix 
 $executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_4_2$logfilepostfix 
@@ -35,8 +66,8 @@ $executable $modelcommand dpm/dpm300.nm $propertycommand dpm/dpm300_numerical.pc
 
 executable=../../../../prism/prism-4.3-src/bin/prism 
 options='-epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs'
-modelcommand=
-propertycommand=
+modelcommand=''
+propertycommand=''
 logfilepostfix='.prism-gs.output'
 $executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_3_2$logfilepostfix 
 $executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_4_2$logfilepostfix 

src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp

@@ -13,6 +13,8 @@
 #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h"
 #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h"
 
+#include "src/utility/Stopwatch.h"
+
 #include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
@@ -35,20 +37,43 @@ namespace storm {
         template<typename SparseMdpModelType>
         std::unique_ptr<CheckResult> SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) {
             STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported.");
+            storm::utility::Stopwatch swModelChecking;
             std::unique_ptr<CheckResult> result;
             
 #ifdef STORM_HAVE_CARL
+            storm::utility::Stopwatch swPreprocessing;
             auto preprocessorData = helper::SparseMultiObjectivePreprocessor<SparseMdpModelType>::preprocess(checkTask.getFormula(), this->getModel());
+            swPreprocessing.pause();
             std::cout << std::endl;
-            std::cout << "Preprocessing done." << std::endl;
             preprocessorData.printToStream(std::cout);
+            STORM_LOG_DEBUG("Preprocessing done.");
+            
+            storm::utility::Stopwatch swHelper;
             auto resultData = helper::SparseMultiObjectiveHelper<SparseMdpModelType, storm::RationalNumber>::check(preprocessorData);
-            std::cout << "Modelchecking done." << std::endl;
+            swHelper.pause();
+            STORM_LOG_DEBUG("Modelchecking done.");
+            
+            storm::utility::Stopwatch swPostprocessing;
             result = helper::SparseMultiObjectivePostprocessor<SparseMdpModelType, storm::RationalNumber>::postprocess(preprocessorData, resultData);
-            std::cout << "Postprocessing done." << std::endl;
+            swPostprocessing.pause();
+            STORM_LOG_DEBUG("Postprocessing done.");
 #else
             STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi objective model checking requires carl.");
 #endif
+            std::cout << std::endl;
+            std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+            std::cout << "                                                 Multi-objective Model Checking Statistics:                                            " << std::endl;
+            std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+            std::cout << std::endl;
+            std::cout << "Runtimes (in seconds):" << std::endl;
+            std::cout << "\t Preprocessing:    " << std::setw(8) << swPreprocessing << std::endl;
+            std::cout << "\t Value Iterations: " << std::setw(8) << swHelper << std::endl;
+            std::cout << "\t Postprocessing:   " << std::setw(8) << swPostprocessing << std::endl;
+            std::cout << "\t Combined:         " << std::setw(8) << swModelChecking << std::endl;
+            std::cout << std::endl;
+            std::cout << "Performed Refinement Steps: " << resultData.refinementSteps().size() << std::endl;
+            std::cout << std::endl;
+            std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
             return result;
         }
         

src/storm.cpp

@@ -3,6 +3,7 @@
 #include "src/utility/macros.h"
 #include "src/cli/cli.h"
 #include "src/utility/initialize.h"
+#include "src/utility/Stopwatch.h"
 
 #include "src/settings/SettingsManager.h"
 
@@ -12,6 +13,8 @@
 int main(const int argc, const char** argv) {
 
     try {
+        storm::utility::Stopwatch stopwatch;
+        
         storm::utility::setUp();
         storm::cli::printHeader("SToRM", argc, argv);
         storm::settings::initializeAll("SToRM", "storm");
@@ -25,6 +28,10 @@ int main(const int argc, const char** argv) {
         
         // All operations have now been performed, so we clean up everything and terminate.
         storm::utility::cleanUp();
+        
+        storm::cli::printUsage();
+        std::cout << "OVERALL_TIME; " << stopwatch << std::endl;
+        
         return 0;
     } catch (storm::exceptions::BaseException const& exception) {
         STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what());

src/utility/Stopwatch.h

@@ -0,0 +1,68 @@
+#ifndef STORM_UTILITY_STOPWATCH_H_
+#define STORM_UTILITY_STOPWATCH_H_
+
+#include <chrono>
+#include <math.h>
+
+#include "src/utility/macros.h"
+
+namespace storm {
+    namespace utility {
+        // A class that provides convenience operations to display run times.
+        class Stopwatch {
+        public:
+            Stopwatch(double initialValueInSeconds = 0.0) : accumulatedSeconds(initialValueInSeconds), paused(false), startOfCurrentMeasurement(std::chrono::high_resolution_clock::now()) {
+                // Intentionally left empty
+            }
+            
+            ~Stopwatch() = default;
+            
+            double getAccumulatedSeconds() const {
+                if(paused) {
+                    return accumulatedSeconds;
+                } else {
+                    return accumulatedSeconds + std::chrono::duration<double>(std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement).count();
+                }
+            }
+            
+            void pause() {
+                if(paused) {
+                    STORM_LOG_WARN("Tried to pause a stopwatch that was already paused.");
+                } else {
+                    accumulatedSeconds = getAccumulatedSeconds();
+                    paused = true;
+                }
+            }
+        
+            void unpause() {
+                if(paused) {
+                    startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
+                    paused = false;
+                } else {
+                    STORM_LOG_WARN("Tried to unpause a stopwatch that was not paused.");
+                }
+            }
+            
+            // Note: Does NOT unpause if stopwatch is currently paused.
+            void reset() {
+                accumulatedSeconds = 0.0;
+                startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
+            }
+
+            friend std::ostream& operator<<(std::ostream& out, Stopwatch const& sw) {
+                out << (round(sw.getAccumulatedSeconds()*1000)/1000);
+                return out;
+            }
+            
+            
+        private:
+            double accumulatedSeconds;
+            bool paused;
+            std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;
+            
+            
+        };
+    }
+}
+
+#endif /* STORM_UTILITY_STOPWATCH_H_ */