Browse Source

Merge branch 'master' into prism-parser-improvements

tempestpy_adaptions
TimQu 5 years ago
parent
commit
48e98119d5
  1. 4
      src/storm-cli-utilities/model-handling.h
  2. 3
      src/storm/models/sparse/Model.cpp

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

@ -824,6 +824,7 @@ namespace storm {
}, },
[&sparseModel,&ioSettings] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) { [&sparseModel,&ioSettings] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
if (ioSettings.isExportSchedulerSet()) { if (ioSettings.isExportSchedulerSet()) {
if (result->isExplicitQuantitativeCheckResult()) {
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 ... ") STORM_PRINT_AND_LOG("Exporting scheduler ... ")
@ -831,6 +832,9 @@ namespace storm {
} else { } else {
STORM_LOG_ERROR("Scheduler requested but could not be generated."); STORM_LOG_ERROR("Scheduler requested but could not be generated.");
} }
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
}
} }
}); });
} }

3
src/storm/models/sparse/Model.cpp

@ -350,8 +350,9 @@ namespace storm {
if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) { if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) {
outStream << "label = \"" << state; outStream << "label = \"" << state;
if (hasStateValuations()) { if (hasStateValuations()) {
std::string stateInfo = getStateValuations().getStateInfo(state);
std::vector<std::string> results; std::vector<std::string> results;
boost::split(results, getStateValuations().getStateInfo(state), [](char c) { return c == ',';});
boost::split(results, stateInfo, [](char c) { return c == ',';});
storm::utility::outputFixedWidth(outStream, results, maxWidthLabel); storm::utility::outputFixedWidth(outStream, results, maxWidthLabel);
} }
outStream << ": "; outStream << ": ";

Loading…
Cancel
Save