From 24d9b8dfc6fbdcdfd806e7229ded1033196fee9f Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 15 Jan 2018 16:33:52 +0100
Subject: [PATCH] minor reformulation
---
.../SMTMinimalLabelSetGenerator.h | 18 +++++-------------
1 file changed, 5 insertions(+), 13 deletions(-)
diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
index 79bb2591f..854d92500 100644
--- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -1450,16 +1450,12 @@ namespace storm {
isBorderChoice = true;
}
}
-
+
if (isBorderChoice) {
boost::container::flat_set<uint_fast64_t> currentLabelSet;
- for (auto label : originalLabelSets.at(currentChoice)) {
- if (commandSet.find(label) == commandSet.end()) {
- currentLabelSet.insert(label);
- }
- }
+ std::set_difference(originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.begin()));
std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end()));
-
+
cutLabels.insert(currentLabelSet);
}
}
@@ -1559,13 +1555,9 @@ namespace storm {
for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) {
if (!std::includes(commandSet.begin(), commandSet.end(), originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end())) {
boost::container::flat_set<uint_fast64_t> currentLabelSet;
- for (auto label : originalLabelSets[currentChoice]) {
- if (commandSet.find(label) == commandSet.end()) {
- currentLabelSet.insert(label);
- }
- }
+ std::set_difference(originalLabelSets[currentChoice].begin(), originalLabelSets[currentChoice].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.begin()));
std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end()));
-
+
cutLabels.insert(currentLabelSet);
}
}