From 072b7d0e1aefcc7561aefd79e08fea3346ac817d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 2 Feb 2015 18:05:19 +0100
Subject: [PATCH 1/2] Added performance statistics for model building.
Former-commit-id: d7de4f93e376eab51412e80b5fb0d0ea4202d312
---
src/utility/cli.h | 25 ++++++++++++++++++++++++-
1 file changed, 24 insertions(+), 1 deletion(-)
diff --git a/src/utility/cli.h b/src/utility/cli.h
index e9297d5af..4ae261d0a 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -353,6 +353,8 @@ 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<storm::models::AbstractModel<double>> model;
if (settings.isExplicitSet()) {
model = buildExplicitModel<double>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
@@ -362,13 +364,34 @@ namespace storm {
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
-
+ std::chrono::high_resolution_clock::time_point buildingTimeEnd = std::chrono::high_resolution_clock::now();
+
// Now, we can do the preprocessing on the model, if it was requested.
+ 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<std::chrono::milliseconds>(totalTime);
+ std::chrono::high_resolution_clock::duration buildingTime = buildingTimeEnd - buildingTimeStart;
+ std::chrono::milliseconds buildingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(buildingTime);
+ std::chrono::high_resolution_clock::duration preprocessingTime = preprocessingTimeEnd - preprocessingTimeStart;
+ std::chrono::milliseconds preprocessingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(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);
+ }
+
// 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.");
From 8bc646ccb825c4f9d3ec4f21f4d8e1cc6bf4f2b0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 3 Feb 2015 05:31:52 +0100
Subject: [PATCH 2/2] Simplification of program when substituting constants.
Former-commit-id: d5ecb355f8c1a1ba45788873cbd3ee67c9c0fd4b
---
src/storage/prism/Command.cpp | 2 +-
src/storage/prism/Module.cpp | 5 ++++-
2 files changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index fec849628..a476e2fd9 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -41,7 +41,7 @@ namespace storm {
newUpdates.emplace_back(update.substitute(substitution));
}
- return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution), newUpdates, this->getFilename(), this->getLineNumber());
+ return Command(this->getGlobalIndex(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution).simplify(), newUpdates, this->getFilename(), this->getLineNumber());
}
bool Command::isLabeled() const {
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index bc40cbd78..e6adf07b1 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -161,7 +161,10 @@ namespace storm {
std::vector<Command> newCommands;
newCommands.reserve(this->getNumberOfCommands());
for (auto const& command : this->getCommands()) {
- newCommands.emplace_back(command.substitute(substitution));
+ Command newCommand = command.substitute(substitution);
+ if (!newCommand.getGuardExpression().isFalse()) {
+ newCommands.emplace_back(newCommand);
+ }
}
return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());