Export labels option now also includes default labels init/deadlock.

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

prism/src/prism/Prism.java

@@ -945,19 +945,17 @@ public class Prism
 		LabelList ll;
 		Expression expr;
 		Values constantValues;
-		Expression2MTBDD expr2mtbdd;
+		Expression2MTBDD expr2mtbdd = null;
 		JDDNode dd, labels[];
 		String labelNames[];
 		
-		if (propertiesFile == null) return;
-		
-		// get label list
+		// get label list and size
+		if (propertiesFile == null) {
+			ll = null;
+			n = 0;
+		} else {
 			ll = propertiesFile.getLabelList();
-		
-		// bail out if there are no labels
-		if (ll.size() == 0) {
-			mainLog.println("\nWarning: There were no labels to export.");
-			return;
+			n = ll.size();
 		}
 		
 		// print message
@@ -965,22 +963,27 @@ public class Prism
 		if (file != null) mainLog.println("to file \"" + file + "\"..."); else mainLog.println("below:");
 		
 		// convert labels to bdds
+		if (n > 0) {
 			constantValues = new Values();
 			constantValues.addValues(model.getConstantValues());
 			constantValues.addValues(propertiesFile.getConstantValues());
 			expr2mtbdd = new Expression2MTBDD(mainLog, techLog, model.getVarList(), model.getVarDDRowVars(), constantValues);
 			expr2mtbdd.setFilter(model.getReach());
-		n = ll.size();
-		labels = new JDDNode[n];
+		}
+		labels = new JDDNode[n+2];
+		labels[0] = model.getStart();
+		labels[1] = model.getFixedDeadlocks();
 		for (i = 0; i < n; i++) {
 			expr = ll.getLabel(i);
 			dd = expr2mtbdd.translateExpression(expr);
-			labels[i] = dd;
+			labels[i+2] = dd;
 		}
 		// put names for labels in an array
-		labelNames = new String[n];
+		labelNames = new String[n+2];
+		labelNames[0] = "init";
+		labelNames[1] = "deadlock";
 		for (i = 0; i < n; i++) {
-			labelNames[i] = ll.getLabelName(i);
+			labelNames[i+2] = ll.getLabelName(i);
 		}
 		
 		// export them to a file
@@ -988,7 +991,7 @@ public class Prism
 		
 		// deref dds
 		for (i = 0; i < n; i++) {
-			JDD.Deref(labels[i]);
+			JDD.Deref(labels[i+2]);
 		}
 	}
 

prism/src/prism/PrismCL.java

@@ -238,13 +238,11 @@ public class PrismCL
 			
 			// export labels/states
 			if (exportlabels) {
-				if (propertiesFile == null) {
-					mainLog.print("\nWarning: Labels have not been exported because there is no properties file");
-				}
-				else {
 				try {
+					if (propertiesFile != null) {
 						definedPFConstants = undefinedConstants.getPFConstantValues();
 						propertiesFile.setUndefinedConstants(definedPFConstants);
+					}
 					File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
 					prism.exportLabelsToFile(model, propertiesFile, exportType, f);
 				}
@@ -256,7 +254,6 @@ public class PrismCL
 					mainLog.println("\nError: " + e.getMessage() + ".");
 				}
 			}
-			}
 			
 			// work through list of properties to be checked
 			for (j = 0; j < numPropertiesToCheck; j++) {