Code tidy + comments.

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

prism/src/explicit/StateStorage.java

@@ -2,9 +2,8 @@
 //	
 //	Copyright (c) 2002-
 //	Authors:
-//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford)
 //	* Mateusz Ujma <mateusz.ujma@cs.ox.ac.uk> (University of Oxford)
-
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -31,8 +30,8 @@ package explicit;
 import java.util.*;
 
 /**
- * Interface for storing an set of objects of type T.
- * Typically used for storing state space during reachability.
+ * Interface for storing a set of objects of type T.
+ * Typically used for storing states during reachability.
  */
 public interface StateStorage<T>
 {
@@ -90,5 +89,4 @@ public interface StateStorage<T>
 	 * to new indices under the sorting order.
 	 */
 	public int[] buildSortingPermutation();
-	
 }

prism/src/parser/State.java

@@ -115,7 +115,7 @@ public class State implements Comparable<State>
 	}
 
 	/**
-	 * 
+	 * Set the {@code i}th value to {@code val}.
 	 */
 	public void setValue(int i, Object val)
 	{
@@ -160,40 +160,49 @@ public class State implements Comparable<State>
 		return true;
 	}
 
+	@Override
 	public int compareTo(State s)
 	{
 		return compareTo(s, 0);
 	}
 	
-	public int compareTo(State s, int variableIndex)
+	/**
+	 * Compare this state to another state {@code s} (in the style of {@link #compareTo(State)},
+	 * first comparing variables with index greater than or equal to {@code j},
+	 * and then comparing variables with index less than {@code j}.
+	 */
+	public int compareTo(State s, int j)
 	{
-		int i, j, n;
+		int i, c, n;
 		Object svv[], o1, o2;
+		
 		// Can't compare to null
 		if (s == null)
 			throw new NullPointerException();
+		
 		// States of different size are incomparable 
 		svv = s.varValues;
 		n = varValues.length;
 		if (n != svv.length)
 			throw new ClassCastException("States are different sizes");
 		
-		if (variableIndex > n-1)
+		if (j > n-1)
 			throw new ClassCastException("Variable index is incorrect");
-		// Go through array
-		for (i = variableIndex; i < n; i++) {
+		
+		// Go through variables j...n-1
+		for (i = j; i < n; i++) {
 			o1 = varValues[i];
 			o2 = svv[i];
 			if (o1 instanceof Integer && o2 instanceof Integer) {
-				j = ((Integer) o1).compareTo((Integer) o2);
-				if (j != 0)
-					return j;
+				c = ((Integer) o1).compareTo((Integer) o2);
+				if (c != 0)
+					return c;
 				else
 					continue;
 			} else if (o1 instanceof Boolean && o2 instanceof Boolean) {
-				j = ((Boolean) o1).compareTo((Boolean) o2);
-				if (j != 0)
-					return j;
+				c = ((Boolean) o1).compareTo((Boolean) o2);
+				if (c != 0)
+					return c;
 				else
 					continue;
 			} else {
@@ -201,25 +210,27 @@ public class State implements Comparable<State>
 			}
 		}
 		
-		for (i = 0; i < variableIndex; i++) {
+		// Go through variables 0...j
+		for (i = 0; i < j; i++) {
 			o1 = varValues[i];
 			o2 = svv[i];
 			if (o1 instanceof Integer && o2 instanceof Integer) {
-				j = ((Integer) o1).compareTo((Integer) o2);
-				if (j != 0)
-					return j;
+				c = ((Integer) o1).compareTo((Integer) o2);
+				if (c != 0)
+					return c;
 				else
 					continue;
 			} else if (o1 instanceof Boolean && o2 instanceof Boolean) {
-				j = ((Boolean) o1).compareTo((Boolean) o2);
-				if (j != 0)
-					return j;
+				c = ((Boolean) o1).compareTo((Boolean) o2);
+				if (c != 0)
+					return c;
 				else
 					continue;
 			} else {
 				throw new ClassCastException("Can't compare " + o1.getClass() + " and " + o2.getClass());
 			}
 		}
+		
 		return 0;
 	}
 

prism/src/pta/DBMList.java

@@ -121,22 +121,22 @@ public class DBMList extends NCZone
 			addDBM(dbm);
 	}
 
-	// Methods required for Zone interface
-
 	/**
-	 * Get parent PTA
+	 * Get the {@code i}th DBM in the list.
 	 */
-	public PTA getPTA()
+	public DBM getDBM(int i) 
 	{
-		return pta;
+		return list.get(i);
 	}
 
+	// Methods required for Zone interface
+
 	/**
-	 * Get DBM
+	 * Get parent PTA
 	 */
-	public DBM getDBM(int i) 
+	public PTA getPTA()
 	{
-		return list.get(i);
+		return pta;
 	}
 	
 	// Zone operations (modify the zone)