From 5a06f212a5db7c411f19c48fbaf8bf125d3ed15a Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Wed, 14 Sep 2016 11:32:38 +0000
Subject: [PATCH] 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 | 40 +++++++++++++++++++++++
 prism/src/prism/StateModelChecker.java    | 35 +++++++++++++++++++-
 2 files changed, 74 insertions(+), 1 deletion(-)

diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java
index 7d0e92f8..1242dbd0 100644
--- a/prism/src/explicit/StateModelChecker.java
+++ b/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
 
 	/**
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index eebad789..652ba4ff 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/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