Browse Source

Cleaner output when exporting schedulers

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
a47945a931
  1. 2
      src/storm-cli-utilities/model-handling.h

2
src/storm-cli-utilities/model-handling.h

@ -773,7 +773,7 @@ namespace storm {
if (ioSettings.isExportSchedulerSet()) { if (ioSettings.isExportSchedulerSet()) {
if (result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()) { if (result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()) {
auto const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler(); auto const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
STORM_PRINT_AND_LOG("Exporting scheduler to '" << ioSettings.getExportSchedulerFilename())
STORM_PRINT_AND_LOG("Exporting scheduler ... ")
storm::api::exportScheduler(sparseModel, scheduler, ioSettings.getExportSchedulerFilename()); storm::api::exportScheduler(sparseModel, scheduler, ioSettings.getExportSchedulerFilename());
} else { } else {
STORM_LOG_ERROR("Scheduler requested but could not be generated."); STORM_LOG_ERROR("Scheduler requested but could not be generated.");

Loading…
Cancel
Save