From 84485a2705f38306c6b7e8170a442e19aaae8aad Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 14 Nov 2013 23:57:57 +0000
Subject: [PATCH] Add areAllChoiceActionsUnique() for prism.NondetModel
 (symbolic) too.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7604 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/NondetModel.java | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java
index 484f8bb7..b36e7810 100644
--- a/prism/src/prism/NondetModel.java
+++ b/prism/src/prism/NondetModel.java
@@ -126,6 +126,35 @@ public class NondetModel extends ProbModel
 		return "S";
 	}
 
+	/**
+	 * Do all choices in in each state have a unique action label?
+	 */
+	public boolean areAllChoiceActionsUnique()
+	{
+		// Action labels
+		for (int i = 0; i < numSynchs; i++) {
+			JDD.Ref(transActions);
+			JDDNode tmp = JDD.Equals(transActions, i + 1);
+			tmp = JDD.SumAbstract(tmp, allDDNondetVars);
+			double max = JDD.FindMax(tmp);
+			JDD.Deref(tmp);
+			if (max > 1)
+				return false;
+		}
+		// Unlabelled choices
+		JDD.Ref(reach);
+		JDD.Ref(transActions);
+		JDD.Ref(nondetMask);
+		JDDNode tmp = JDD.And(reach, JDD.And(JDD.LessThanEquals(transActions, 0), JDD.Not(nondetMask)));
+		tmp = JDD.SumAbstract(tmp, allDDNondetVars);
+		double max = JDD.FindMax(tmp); 
+		JDD.Deref(tmp);
+		if (max > 1)
+			return false;
+		
+		return true;
+	}
+	
 	// set methods for things not set up in constructor
 
 	public void setTransInd(JDDNode transInd)