State lists and vectors display Boolean variables properly (true/false, not 1/0).

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

prism/src/prism/StateListMTBDD.java

@@ -22,10 +22,10 @@
 
 package prism;
 
-import parser.VarList;
 import jdd.*;
 import odd.*;
 import parser.Values;
+import parser.VarList;
 import parser.Expression;
 
 // list of states (mtbdd)
@@ -154,7 +154,7 @@ public class StateListMTBDD implements StateList
 	
 	private void printRec(JDDNode dd, int level, ODDNode o, long n)
 	{
-		int i;
+		int i, j;
 		JDDNode e, t;
 		
 		// if we've printed enough states, stop
@@ -167,11 +167,18 @@ public class StateListMTBDD implements StateList
 		if (level == numVars) {
 			
 			if (!matlab) outputLog.print(n + ":(");
-			for (i = 0; i < varList.getNumVars()-1; i++) {
-				outputLog.print((varValues[i]+varList.getLow(i)) + ",");
+			j = varList.getNumVars();
+			for (i = 0; i < j; i++) {
+				// integer variable
+				if (varList.getType(i) == Expression.INT) {
+					outputLog.print(varValues[i]+varList.getLow(i));
+				}
+				// boolean variable
+				else {
+					outputLog.print(varValues[i] == 1);
+				}
+				if (i < j-1) outputLog.print(",");
 			}
-			i = varList.getNumVars()-1;
-			outputLog.print((varValues[i]+varList.getLow(i)));
 			if (!matlab) outputLog.print(")");
 			outputLog.println();
 			count++;

prism/src/prism/StateProbsDV.java

@@ -26,6 +26,7 @@ import dv.*;
 import jdd.*;
 import odd.*;
 import parser.VarList;
+import parser.Expression;
 
 // state probability vector (double vector)
 
@@ -234,7 +235,7 @@ public class StateProbsDV implements StateProbs
 	
 	private void printRec(int level, ODDNode o, int n)
 	{
-		int i;
+		int i, j;
 		double d;
 		
 		// base case - at bottom
@@ -242,11 +243,18 @@ public class StateProbsDV implements StateProbs
 			d = probs.getElement(n);
 			if (d != 0) {
 				outputLog.print(n + ":(");
-				for (i = 0; i < varList.getNumVars()-1; i++) {
-					outputLog.print((varValues[i]+varList.getLow(i)) + ",");
+				j = varList.getNumVars();
+				for (i = 0; i < j; i++) {
+					// integer variable
+					if (varList.getType(i) == Expression.INT) {
+						outputLog.print(varValues[i]+varList.getLow(i));
+					}
+					// boolean variable
+					else {
+						outputLog.print(varValues[i] == 1);
+					}
+					if (i < j-1) outputLog.print(",");
 				}
-				i = varList.getNumVars()-1;
-				outputLog.print((varValues[i]+varList.getLow(i)));
 				outputLog.print(")=" + d + " ");
 				outputLog.println();
 				return;

prism/src/prism/StateProbsMTBDD.java

@@ -25,6 +25,7 @@ package prism;
 import jdd.*;
 import odd.*;
 import parser.VarList;
+import parser.Expression;
 
 // state probability vector (mtbdd)
 
@@ -330,7 +331,7 @@ public class StateProbsMTBDD implements StateProbs
 	
 	private void printRec(JDDNode dd, int level, ODDNode o, long n)
 	{
-		int i;
+		int i, j;
 		JDDNode e, t;
 
 		// zero constant - bottom out of recursion
@@ -340,11 +341,18 @@ public class StateProbsMTBDD implements StateProbs
 		if (level == numVars) {
 		
 			outputLog.print(n + ":(");
-			for (i = 0; i < varList.getNumVars()-1; i++) {
-				outputLog.print((varValues[i]+varList.getLow(i)) + ",");
+			j = varList.getNumVars();
+			for (i = 0; i < j; i++) {
+				// integer variable
+				if (varList.getType(i) == Expression.INT) {
+					outputLog.print(varValues[i]+varList.getLow(i));
+				}
+				// boolean variable
+				else {
+					outputLog.print(varValues[i] == 1);
+				}
+				if (i < j-1) outputLog.print(",");
 			}
-			i = varList.getNumVars()-1;
-			outputLog.print((varValues[i]+varList.getLow(i)));
 			outputLog.print(")=" + dd.getValue() + " ");
 			outputLog.println();
 			return;