From b80f41d5bc6f54d6b6357ec76da7b24ffa82008b Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 14 Sep 2016 11:33:06 +0000
Subject: [PATCH] ModelExplicit: refactor addUniqueLabel to ensure that already
 defined label names are avoided

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11814 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/ModelExplicit.java     | 36 ++++++++++++++---------
 prism/src/explicit/StateModelChecker.java |  2 +-
 2 files changed, 23 insertions(+), 15 deletions(-)

diff --git a/prism/src/explicit/ModelExplicit.java b/prism/src/explicit/ModelExplicit.java
index f44afb7a..f62db21e 100644
--- a/prism/src/explicit/ModelExplicit.java
+++ b/prism/src/explicit/ModelExplicit.java
@@ -208,30 +208,38 @@ public abstract class ModelExplicit implements Model
 	 * The label will be either "X" or "X_i" where X is the content of the {@code prefix} argument
 	 * and i is a non-negative integer.
 	 * <br>
-	 * Note that a stored label takes preference over the on-the-fly calculation
+	 * Optionally, a set of defined label names can be passed so that those labels
+	 * can be avoided. This can be obtained from the model checker via {@code getDefinedLabelNames()}.
+	 * <br>
+	 * Note that a stored label takes precedence over the on-the-fly calculation
 	 * of an ExpressionLabel, cf. {@link explicit.StateModelChecker#checkExpressionLabel}
 	 *
 	 * @param prefix the prefix for the unique label
 	 * @param labelStates the BitSet with the state set for the label
+	 * @param definedLabelNames set of names (optional, may be {@code null}) to check for existing labels
 	 * @return the generated unique label
 	 */
-	public String addUniqueLabel(String prefix, BitSet labelStates)
+	public String addUniqueLabel(String prefix, BitSet labelStates, Set<String> definedLabelNames)
 	{
 		String label;
-		if (!hasLabel(prefix)) {
-			label = prefix;
-		} else {
-			int i = 0;
-			while (true) {
-				if (!hasLabel(prefix+"_"+i)) {
-					label = prefix+"_"+i;
-					break;
-				}
-				if (i == Integer.MAX_VALUE)
-					throw new UnsupportedOperationException("Integer overflow trying to add unique label");
+		int i = 0;
+		label = prefix;  // first, try without appending _i
+		while (true) {
+			boolean labelOk = !hasLabel(label);  // not directly attached to model
+			if (definedLabelNames != null) {
+				labelOk &= !definedLabelNames.contains(label);  // not defined
+			}
 
-				i++;
+			if (labelOk) {
+				break;
 			}
+
+			// prepare next label to try
+			label = prefix+"_"+i;
+			if (i == Integer.MAX_VALUE)
+				throw new UnsupportedOperationException("Integer overflow trying to add unique label");
+
+			i++;
 		}
 
 		addLabel(label, labelStates);
diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 1242dbd0..1868914a 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/prism/src/explicit/StateModelChecker.java
@@ -1189,7 +1189,7 @@ public class StateModelChecker extends PrismComponent
 			String currentLabel = "L"+i;
 			// Attach satisfaction set for Li to the model, record necessary
 			// label renaming
-			String newLabel = model.addUniqueLabel("phi", labelBS.get(i));
+			String newLabel = model.addUniqueLabel("phi", labelBS.get(i), getDefinedLabelNames());
 			labelReplacements.put(currentLabel, newLabel);
 		}
 		// rename the labels