diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index aaa601d15..b5606153f 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -140,6 +140,11 @@ namespace storm { if (wallclockMilliseconds != 0) { std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << " seconds" << std::endl; } + std::cout << "STATISTICS_OVERALL_HEADERS;" << "memory;CPU time;wallclock time;" << std::endl; + std::cout << "STATISTICS_OVERALL_DATA;" + << ru.ru_maxrss/1024/1024 << ";" + << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << ";" + << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << ";" << std::endl; #else HANDLE hProcess = GetCurrentProcess (); FILETIME ftCreation, ftExit, ftUser, ftKernel; diff --git a/src/storm/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp index b7ca7cbc4..0bb19e6c8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa.cpp @@ -1,3 +1,4 @@ +#include #include "storm/modelchecker/multiobjective/pcaa.h" #include "storm/utility/macros.h" @@ -11,9 +12,11 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" #include "storm/settings//SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/utility/Stopwatch.h" namespace storm { namespace modelchecker { @@ -22,17 +25,17 @@ namespace storm { template std::unique_ptr performPcaa(SparseModelType const& model, storm::logic::MultiObjectiveFormula const& formula) { STORM_LOG_ASSERT(model.getInitialStates().getNumberOfSetBits() == 1, "Multi-objective Model checking on model with multiple initial states is not supported."); - + storm::utility::Stopwatch swPcaa,swPrep; #ifdef STORM_HAVE_CARL - + // If we consider an MA, ensure that it is closed if(model.isOfType(storm::models::ModelType::MarkovAutomaton)) { STORM_LOG_THROW(dynamic_cast const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); } - + auto preprocessorResult = SparsePcaaPreprocessor::preprocess(model, formula); STORM_LOG_DEBUG("Preprocessing done. Result: " << preprocessorResult); - + auto preprocessedModelStates = preprocessorResult.preprocessedModel.getNumberOfStates(); std::unique_ptr> query; switch (preprocessorResult.queryType) { case SparsePcaaPreprocessorReturnType::QueryType::Achievability: @@ -48,12 +51,54 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unsupported multi-objective Query Type."); break; } - + swPrep.pause(); + storm::utility::Stopwatch swCheck; auto result = query->check(); - + swCheck.pause(); + swPcaa.pause(); + + std::cout << "STATISTICS_HEADERS;" + << "States;" + << "Transitions;" + << "Choices;" + << "Markovian states;" + << "Probabilistic states;" + << "Maximum exit rate E(s);" + << "Num of states after preprocessing;" + << "Query;" + << "Value iteration precision;" + << "Approximation precision;" + << "Time PCAA;" + << "Time Preprocessing;" + << "Time QueryCheck;" + << "Num of checked weight vectors;" + << "Vertices underApprox;" + << "Vertices overApprox;" + << "Max step bound;" + << std::endl; + + std::cout << "STATISTICS_DATA;" + << model.getNumberOfStates() << ";" + << model.getNumberOfTransitions() << ";" + << model.getNumberOfChoices() << ";" + << (model.isOfType(storm::models::ModelType::MarkovAutomaton) ? dynamic_cast const *>(&model)->getMarkovianStates().getNumberOfSetBits() : 0) << ";" + << (model.isOfType(storm::models::ModelType::MarkovAutomaton) ? ~(dynamic_cast const *>(&model)->getMarkovianStates()).getNumberOfSetBits() : model.getNumberOfStates()) << ";" + << (model.isOfType(storm::models::ModelType::MarkovAutomaton) ? dynamic_cast const *>(&model)->getMaximalExitRate() : 0) << ";" + << formula << ";" + << preprocessedModelStates << ";" + << settings::getModule().getPrecision() << ";" + << settings::getModule().getPrecision() << ";" + << swPcaa << ";" + << swPrep << ";" + << swCheck << ";"; + query->printInternalStatistics(); + std::cout << std::endl; + + if(settings::getModule().isExportPlotSet()) { query->exportPlotOfCurrentApproximation(storm::settings::getModule().getExportPlotDirectory()); } + return result; #else STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi-objective model checking requires carl."); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 1c4dd8420..50c6f6aaa 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -69,6 +69,7 @@ namespace storm { auto lowerTimeBoundIt = lowerTimeBounds.begin(); auto upperTimeBoundIt = upperTimeBounds.begin(); uint_fast64_t currentEpoch = std::max(lowerTimeBounds.empty() ? 0 : lowerTimeBoundIt->first, upperTimeBounds.empty() ? 0 : upperTimeBoundIt->first); + this->maxStepBound = std::max(this->maxStepBound, currentEpoch); while(true) { // Update the objectives that are considered at the current time epoch as well as the (weighted) reward vectors. updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, lowerTimeBoundIt, lowerTimeBounds, upperTimeBoundIt, upperTimeBounds); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index c0a891a13..cc9b33333 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -34,7 +34,16 @@ namespace storm { * This only works for 2 dimensional queries. */ void exportPlotOfCurrentApproximation(std::string const& destinationDir) const; - + + + void printInternalStatistics() const { + std::cout << refinementSteps.size() << ";" + << underApproximation->getVertices().size() << ";" + << overApproximation->getVertices().size() << ";" + << overApproximation->getVertices().size() << ";" + << weightVectorChecker->maxStepBound << ";"; + } + protected: /* diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 452f30189..4a60ba34c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -77,7 +77,8 @@ namespace storm { * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. */ storm::storage::TotalScheduler const& getScheduler() const; - + + uint_fast64_t maxStepBound = 0; protected: