From ddff929cbd3db17a4e5f0fc1ecd83baa08941be9 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 29 Oct 2019 21:17:24 +0100
Subject: [PATCH 1/2] Scheduler extraction is only supported for quantitative
checks
---
src/storm-cli-utilities/model-handling.h | 14 +++++++++-----
1 file changed, 9 insertions(+), 5 deletions(-)
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 1dc8a2370..6ea904594 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -824,12 +824,16 @@ namespace storm {
},
[&sparseModel,&ioSettings] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
if (ioSettings.isExportSchedulerSet()) {
- if (result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()) {
- auto const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
- STORM_PRINT_AND_LOG("Exporting scheduler ... ")
- storm::api::exportScheduler(sparseModel, scheduler, ioSettings.getExportSchedulerFilename());
+ if (result->isExplicitQuantitativeCheckResult()) {
+ if (result->template asExplicitQuantitativeCheckResult<ValueType>().hasScheduler()) {
+ auto const& scheduler = result->template asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
+ STORM_PRINT_AND_LOG("Exporting scheduler ... ")
+ storm::api::exportScheduler(sparseModel, scheduler, ioSettings.getExportSchedulerFilename());
+ } else {
+ STORM_LOG_ERROR("Scheduler requested but could not be generated.");
+ }
} else {
- STORM_LOG_ERROR("Scheduler requested but could not be generated.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
}
}
});
From 013695a6cec15c82e6cac848e2f82f8250968675 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 29 Oct 2019 23:09:20 +0100
Subject: [PATCH 2/2] Fixed compile issue: boost::split seems to need an lvalue
for the input string.
---
src/storm/models/sparse/Model.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp
index 1fe875ab9..6e087822f 100644
--- a/src/storm/models/sparse/Model.cpp
+++ b/src/storm/models/sparse/Model.cpp
@@ -350,8 +350,9 @@ namespace storm {
if (includeLabeling || firstValue != nullptr || secondValue != nullptr || hasStateValuations()) {
outStream << "label = \"" << state;
if (hasStateValuations()) {
+ std::string stateInfo = getStateValuations().getStateInfo(state);
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);
}
outStream << ": ";