From cb9cf68632c71f45a3f28e9d652aff764db54598 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 20 Jun 2016 14:13:36 +0200 Subject: [PATCH] output of runtime of mec decomposition Former-commit-id: 5238f9a7ad63d4f2d8202246d581ce5d23abd435 --- examples/multi-objective/mdp/benchmarks_numerical.sh | 2 +- .../helper/SparseMultiObjectivePreprocessor.cpp | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/examples/multi-objective/mdp/benchmarks_numerical.sh b/examples/multi-objective/mdp/benchmarks_numerical.sh index 165b615bd..d9b74740b 100755 --- a/examples/multi-objective/mdp/benchmarks_numerical.sh +++ b/examples/multi-objective/mdp/benchmarks_numerical.sh @@ -4,7 +4,7 @@ mkdir benchmarks_numerical executable=../../../build/src/Release/storm -options='--precision 0.000001 --multiobjective:precision 0.0001' +options='--precision 0.000001 --multiobjective:precision 0.0001 --debug' modelcommand='-s' propertycommand='-prop' logfilepostfix='.storm.output' diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 5972f5f0b..f1de554ea 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -10,6 +10,7 @@ #include "src/utility/macros.h" #include "src/utility/vector.h" #include "src/utility/graph.h" +#include "src/utility/Stopwatch.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/exceptions/UnexpectedException.h" @@ -362,8 +363,9 @@ namespace storm { template void SparseMultiObjectivePreprocessor::assertPositiveRewardFiniteness(PreprocessorData& data, storm::storage::BitVector const& actionsWithNegativeReward) { - + storm::utility::Stopwatch sw; auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getBackwardTransitions()); + STORM_LOG_DEBUG("Maximal end component decomposition for asserting positive reward finiteness took " << sw << " seconds."); if(mecDecomposition.empty()) { return; }