From b7791bf416247a958ae1501fba9ccca2a346316f Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 19 Jul 2017 12:28:34 +0000
Subject: [PATCH] prism.Model: move addUniqueLabelDD interface to Model

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12053 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/Model.java     | 19 +++++++++++++++++++
 prism/src/prism/ProbModel.java | 18 +-----------------
 2 files changed, 20 insertions(+), 17 deletions(-)

diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java
index 98b0fb00..aa38e161 100644
--- a/prism/src/prism/Model.java
+++ b/prism/src/prism/Model.java
@@ -78,6 +78,25 @@ public interface Model
 	 */
 	Set<String> getLabels();
 
+	/**
+	 * Add a label with corresponding state set, ensuring a unique, non-existing label.
+	 * 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>
+	 * 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}
+	 * <br>[ STORES: labelDD, deref on later call to clear() ]
+	 *
+	 * @param prefix the prefix for the unique label
+	 * @param labelDD the JDDNode 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 addUniqueLabelDD(String prefix, JDDNode labelDD, Set<String> definedLabelNames);
+
 	String globalToLocal(long x);
 	int globalToLocal(long x, int l);
 	State convertBddToState(JDDNode dd);
diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java
index 7843fb1e..6ba33322 100644
--- a/prism/src/prism/ProbModel.java
+++ b/prism/src/prism/ProbModel.java
@@ -481,23 +481,7 @@ public class ProbModel implements Model
 		if (old != null) JDD.Deref(old);
 	}
 
-	/**
-	 * Add a label with corresponding state set, ensuring a unique, non-existing label.
-	 * 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>
-	 * 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}
-	 * <br>[ STORES: labelDD, deref on later call to clear() ]
-	 *
-	 * @param prefix the prefix for the unique label
-	 * @param labelDD the JDDNode 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
-	 */
+	@Override
 	public String addUniqueLabelDD(String prefix, JDDNode labelDD, Set<String> definedLabelNames)
 	{
 		String label;