From fba209b7f3a78d7e64ad2100220582fa1fdba99e Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 5 Jul 2016 12:16:26 +0000
Subject: [PATCH] New getIndexOfState method in prism.StateList (not tested
 yet).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11462 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/StateList.java      |  7 +++++
 prism/src/prism/StateListMTBDD.java | 46 +++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+)

diff --git a/prism/src/prism/StateList.java b/prism/src/prism/StateList.java
index a2e063ec..1fce06aa 100644
--- a/prism/src/prism/StateList.java
+++ b/prism/src/prism/StateList.java
@@ -29,6 +29,7 @@ package prism;
 import java.util.List;
 
 import jdd.*;
+import parser.State;
 import parser.Values;
 
 /**
@@ -94,6 +95,12 @@ public interface StateList
 	 */
 	Values getFirstAsValues() throws PrismException;
 	
+	/**
+	 * Get the index of a state in the list, specified as a State object.
+	 * Returns -1 if the state is not on the list or there is a problem with the lookup. 
+	 */
+	int getIndexOfState(State state);
+
 	/**
 	 * Free any memory associated with storing this list of states.
 	 */
diff --git a/prism/src/prism/StateListMTBDD.java b/prism/src/prism/StateListMTBDD.java
index a17a8ebf..57700087 100644
--- a/prism/src/prism/StateListMTBDD.java
+++ b/prism/src/prism/StateListMTBDD.java
@@ -30,6 +30,7 @@ import java.util.*;
 
 import jdd.*;
 import odd.*;
+import parser.State;
 import parser.Values;
 import parser.VarList;
 import parser.type.*;
@@ -372,6 +373,51 @@ public class StateListMTBDD implements StateList
 		return values;
 	}
 
+	@Override
+	public int getIndexOfState(State state)
+	{
+		// Traverse BDD/ODD, top to bottom, computing index
+		JDDNode ptr = states;
+		ODDNode o = odd;
+		int level = 0;
+		int index = 0;
+		// Iterate through variables
+		int n = varList.getNumVars();
+		for (int i = 0; i < n; i++) {
+			int valInt = -1;
+			try {
+				valInt = varList.encodeToInt(i, state.varValues[i]); 
+			} catch (PrismLangException e) {
+				// Problem looking up variable - bail out 
+				return -1;
+			}
+			// Iterate through bits for this variable
+			int n2 = varSizes[i];
+			for (int j = 0; j < n2; j++) {
+				// Traverse BDD (need to double check state is in the set)
+				if (ptr.equals(JDD.ZERO)) {
+					return -1;
+				} else if (ptr.getIndex() > vars.getVarIndex(level)) {
+					// ptr = ptr;
+				} else if ((valInt & (1 << (n2-1-j))) == 0) {
+					ptr = ptr.getElse();
+				} else {
+					ptr.getThen();					
+				}
+				level++;
+				// Traverse ODD (to get index)
+				if ((valInt & (1 << (n2-1-j))) == 0) {
+					o = o.getElse();
+				} else {
+					o.getThen();	
+					index += o.getEOff();
+				}
+				
+			}
+		}
+		return index;
+	}
+	
 	@Override
 	public void clear()
 	{