sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merged master into parametricSystems. 

Former-commit-id: d6bd414859
tempestpy_adaptions
dehnert 10 years ago
parent
6585e56768 0a59f7a7ef
commit
36e632c43c
2 changed files with 25 additions and 20 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storage/prism/TransitionReward.cpp
  2. 43
      src/utility/cli.h

2
src/storage/prism/TransitionReward.cpp
View File

@ -2,7 +2,7 @@
namespace storm { namespace storm {
namespace prism { 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. // Nothing to do here.
} }

43
src/utility/cli.h
View File

@ -339,6 +339,7 @@ namespace storm {
initializeFileLogging(); initializeFileLogging();
} }
std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings(); storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
// If we have to build the model from a symbolic representation, we need to parse the representation first. // If we have to build the model from a symbolic representation, we need to parse the representation first.
@ -361,7 +362,6 @@ namespace storm {
} }
// Now we are ready to actually build the model. // 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::chrono::high_resolution_clock::time_point buildingTimeStart = std::chrono::high_resolution_clock::now();
std::shared_ptr<storm::models::AbstractModel<double>> model; std::shared_ptr<storm::models::AbstractModel<double>> model;
if (settings.isExplicitSet()) { if (settings.isExplicitSet()) {
@ -378,28 +378,11 @@ namespace storm {
std::chrono::high_resolution_clock::time_point preprocessingTimeStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point preprocessingTimeStart = std::chrono::high_resolution_clock::now();
model = preprocessModel(model, formula); 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 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. // Print some information about the model.
model->printModelInformationToStream(std::cout); 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);
}
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 we were requested to generate a counterexample, we now do so.
if (settings.isCounterexampleSet()) { if (settings.isCounterexampleSet()) {
STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property."); STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
@ -427,6 +410,28 @@ namespace storm {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; 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<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);
std::chrono::high_resolution_clock::duration checkingTime = checkingTimeEnd - checkingTimeStart;
std::chrono::milliseconds checkingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(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);
}
} }
} }
} }

Write Preview
Loading…
Cancel
Save