explicit/symbolic StateModelChecker: add methods getLabelList() and getDefinedLabelNames() to provide access to label namespace

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11813 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/StateModelChecker.java

@@ -36,6 +36,8 @@ import java.util.BitSet;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
+import java.util.TreeSet;
 import java.util.Vector;
 
 import parser.State;
@@ -370,6 +372,44 @@ public class StateModelChecker extends PrismComponent
 		return constantValues;
 	}
 
+	/**
+	 * Get the label list (from properties file and modules file, if they are attached).
+	 * @return the label list for the properties/modules file, or {@code null} if not available.
+	 */
+	public LabelList getLabelList()
+	{
+		if (propertiesFile != null) {
+			return propertiesFile.getCombinedLabelList(); // combined list from properties and modules file
+		} else if (modulesFile != null) {
+			return modulesFile.getLabelList();
+		} else {
+			return null;
+		}
+	}
+
+	/**
+	 * Return the set of label names that are defined
+	 * either by the model (from the model info or modules file)
+	 * or properties file (if attached to the model checker).
+	 */
+	public Set<String> getDefinedLabelNames()
+	{
+		TreeSet<String> definedLabelNames = new TreeSet<String>();
+
+		// labels from the label list
+		LabelList labelList = getLabelList();
+		if (labelList != null) {
+			definedLabelNames.addAll(labelList.getLabelNames());
+		}
+
+		// labels from the model info
+		if (modelInfo != null) {
+			definedLabelNames.addAll(modelInfo.getLabelNames());
+		}
+
+		return definedLabelNames;
+	}
+
 	// Other setters/getters
 
 	/**

prism/src/prism/StateModelChecker.java

@@ -29,6 +29,8 @@ package prism;
 import java.io.File;
 import java.io.FileNotFoundException;
 import java.util.List;
+import java.util.Set;
+import java.util.TreeSet;
 
 import mtbdd.PrismMTBDD;
 import dv.DoubleVector;
@@ -1418,7 +1420,38 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 	{
 		return constantValues;
 	}
-	
+
+	/**
+	 * Get the label list (combined list from properties file, if attached).
+	 * @return the label list for the properties/modules file, or {@code null} if not available.
+	 */
+	public LabelList getLabelList()
+	{
+		if (propertiesFile != null) {
+			return propertiesFile.getCombinedLabelList(); // combined list from properties and modules file
+		} else {
+			return null;
+		}
+	}
+
+	/**
+	 * Return the set of label names that are defined
+	 * either by the model (from the modules file)
+	 * or properties file (if attached to the model checker).
+	 */
+	public Set<String> getDefinedLabelNames()
+	{
+		TreeSet<String> definedLabelNames = new TreeSet<String>();
+
+		// labels from the label list
+		LabelList labelList = getLabelList();
+		if (labelList != null) {
+			definedLabelNames.addAll(labelList.getLabelNames());
+		}
+
+		return definedLabelNames;
+	}
+
 	/**
 	 * Export a set of labels and the states that satisfy them.
 	 * @param labelNames The name of each label