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