Export of labels includes those in model if none in properties file.

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

prism/src/prism/Prism.java

@@ -1067,7 +1067,7 @@ public class Prism implements PrismSettingsListener
 	// export labels and satisfying states to a file
 	// file == null mean export to log
 	
-	public void exportLabelsToFile(Model model, PropertiesFile propertiesFile, int exportType, File file) throws FileNotFoundException, PrismException
+	public void exportLabelsToFile(Model model, ModulesFile modulesFile, PropertiesFile propertiesFile, int exportType, File file) throws FileNotFoundException, PrismException
 	{
 		int i, n;
 		LabelList ll;
@@ -1079,8 +1079,8 @@ public class Prism implements PrismSettingsListener
 		
 		// get label list and size
 		if (propertiesFile == null) {
-			ll = null;
-			n = 0;
+			ll = modulesFile.getLabelList();
+			n = ll.size();
 		} else {
 			ll = propertiesFile.getCombinedLabelList();
 			n = ll.size();
@@ -1094,7 +1094,7 @@ public class Prism implements PrismSettingsListener
 		if (n > 0) {
 			constantValues = new Values();
 			constantValues.addValues(model.getConstantValues());
-			constantValues.addValues(propertiesFile.getConstantValues());
+			if (propertiesFile != null) constantValues.addValues(propertiesFile.getConstantValues());
 			expr2mtbdd = new Expression2MTBDD(mainLog, techLog, model.getVarList(), model.getVarDDRowVars(), constantValues);
 			expr2mtbdd.setFilter(model.getReach());
 		}

prism/src/prism/PrismCL.java

@@ -267,7 +267,7 @@ public class PrismCL
 						propertiesFile.setUndefinedConstants(definedPFConstants);
 					}
 					File f = (exportLabelsFilename.equals("stdout")) ? null : new File(exportLabelsFilename);
-					prism.exportLabelsToFile(model, propertiesFile, exportType, f);
+					prism.exportLabelsToFile(model, modulesFile, propertiesFile, exportType, f);
 				}
 				// in case of error, report it and proceed
 				catch (FileNotFoundException e) {