From baeeec96231050a4812360df4d0c306931cbf03c Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 4 Dec 2007 10:05:17 +0000
Subject: [PATCH] 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   | 8 ++++----
 prism/src/prism/PrismCL.java | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java
index 8576a362..bd7ab28c 100644
--- a/prism/src/prism/Prism.java
+++ b/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());
 		}
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index cde31054..d60ec123 100644
--- a/prism/src/prism/PrismCL.java
+++ b/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) {