From 40e148d9a4b661719b1f1a0c3edd5172339c5447 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 3 Feb 2015 06:25:55 +0100 Subject: [PATCH 1/2] Added overall performance measurements. Former-commit-id: bbe44611670d0da54b2b6e2caa5f4b1bde2c5dec --- src/utility/cli.h | 43 ++++++++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 19 deletions(-) diff --git a/src/utility/cli.h b/src/utility/cli.h index 4ae261d0a..9463560d8 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -331,6 +331,7 @@ namespace storm { } void processOptions() { + std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); // If we have to build the model from a symbolic representation, we need to parse the representation first. @@ -353,7 +354,6 @@ namespace storm { } // Now we are ready to actually build the model. - std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point buildingTimeStart = std::chrono::high_resolution_clock::now(); std::shared_ptr> model; if (settings.isExplicitSet()) { @@ -370,28 +370,11 @@ namespace storm { std::chrono::high_resolution_clock::time_point preprocessingTimeStart = std::chrono::high_resolution_clock::now(); model = preprocessModel(model, formula); std::chrono::high_resolution_clock::time_point preprocessingTimeEnd = std::chrono::high_resolution_clock::now(); - std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); // Print some information about the model. model->printModelInformationToStream(std::cout); - if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; - std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); - std::chrono::high_resolution_clock::duration buildingTime = buildingTimeEnd - buildingTimeStart; - std::chrono::milliseconds buildingTimeInMilliseconds = std::chrono::duration_cast(buildingTime); - std::chrono::high_resolution_clock::duration preprocessingTime = preprocessingTimeEnd - preprocessingTimeStart; - std::chrono::milliseconds preprocessingTimeInMilliseconds = std::chrono::duration_cast(preprocessingTime); - - STORM_PRINT_AND_LOG(std::endl); - STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); - STORM_PRINT_AND_LOG(" * time for building: " << buildingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(" * time for preprocessing: " << preprocessingTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); - STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); - STORM_PRINT_AND_LOG(std::endl); - } - + std::chrono::high_resolution_clock::time_point checkingTimeStart = std::chrono::high_resolution_clock::now(); // If we were requested to generate a counterexample, we now do so. if (settings.isCounterexampleSet()) { STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property."); @@ -419,6 +402,28 @@ namespace storm { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } } + std::chrono::high_resolution_clock::time_point checkingTimeEnd = std::chrono::high_resolution_clock::now(); + std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); + + if (storm::settings::generalSettings().isShowStatisticsSet()) { + std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart; + std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast(totalTime); + std::chrono::high_resolution_clock::duration buildingTime = buildingTimeEnd - buildingTimeStart; + std::chrono::milliseconds buildingTimeInMilliseconds = std::chrono::duration_cast(buildingTime); + std::chrono::high_resolution_clock::duration preprocessingTime = preprocessingTimeEnd - preprocessingTimeStart; + std::chrono::milliseconds preprocessingTimeInMilliseconds = std::chrono::duration_cast(preprocessingTime); + std::chrono::high_resolution_clock::duration checkingTime = checkingTimeEnd - checkingTimeStart; + std::chrono::milliseconds checkingTimeInMilliseconds = std::chrono::duration_cast(checkingTime); + + STORM_PRINT_AND_LOG(std::endl); + STORM_PRINT_AND_LOG("Time breakdown:" << std::endl); + STORM_PRINT_AND_LOG(" * time for building: " << buildingTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(" * time for preprocessing: " << preprocessingTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(" * time for checking: " << checkingTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG("------------------------------------------" << std::endl); + STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl); + STORM_PRINT_AND_LOG(std::endl); + } } } } From 0a59f7a7ef9d5b745250e9143dabd26c4de6d61b Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 3 Feb 2015 13:03:29 +0100 Subject: [PATCH 2/2] Fixed a bug that sometimes prevented transition rewards from being built. Former-commit-id: afd56375abe84620508972511786ef9eafec2ed8 --- src/builder/ExplicitPrismModelBuilder.cpp | 2 +- src/storage/DeterministicModelBisimulationDecomposition.cpp | 2 +- src/storage/prism/TransitionReward.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 01d06cd11..48d21ba6e 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -220,7 +220,7 @@ namespace storm { int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); - STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) == assignedValue, "Writing to the bit vector bucket failed."); + STORM_LOG_ASSERT(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed."); } // Check that we processed all assignments. diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 08c11a2f2..81d4feec8 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -642,7 +642,7 @@ namespace storm { measureDrivenInitialPartition = true; } } else if (newFormula->isReachabilityRewardFormula()) { - rightSubformula = newFormula->asEventuallyFormula().getSubformula().asSharedPointer(); + rightSubformula = newFormula->asReachabilityRewardFormula().getSubformula().asSharedPointer(); if (rightSubformula->isPropositionalFormula()) { measureDrivenInitialPartition = true; } diff --git a/src/storage/prism/TransitionReward.cpp b/src/storage/prism/TransitionReward.cpp index 2fee8dabc..182fe43a1 100644 --- a/src/storage/prism/TransitionReward.cpp +++ b/src/storage/prism/TransitionReward.cpp @@ -2,7 +2,7 @@ namespace storm { namespace prism { - TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), labeled(actionName != ""), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { + TransitionReward::TransitionReward(uint_fast64_t actionIndex, std::string const& actionName, storm::expressions::Expression const& statePredicateExpression, storm::expressions::Expression const& rewardValueExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionIndex(actionIndex), actionName(actionName), labeled(actionName != ""), statePredicateExpression(statePredicateExpression), rewardValueExpression(rewardValueExpression) { // Nothing to do here. }