Merge lp:~danilovesky/workcraft/trunk-stg-conformation into lp:workcraft

[Danil Sokolov]

[lp:~danilovesky/workcraft/trunk-stg-conformation]

575. By Danil Sokolov on 2014-11-30

Polishing the Reach expression for conformation check.

[Danil Sokolov (danilovesky)]

review: Needs Resubmitting

[Danil Sokolov (danilovesky)]

review: Approve

=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java	2014-11-24 15:37:13 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java	2014-11-30 23:14:46 +0000
@@ -1,6 +1,13 @@
 package org.workcraft.plugins.circuit.tasks;
 
+import java.io.BufferedReader;
+import java.io.ByteArrayInputStream;
 import java.io.File;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.InputStreamReader;
+import java.util.HashSet;
+import java.util.Set;
 
 import org.workcraft.Framework;
 import org.workcraft.interop.Exporter;
@@ -14,10 +21,11 @@
 import org.workcraft.plugins.mpsat.tasks.MpsatChainTask;
 import org.workcraft.plugins.mpsat.tasks.MpsatTask;
 import org.workcraft.plugins.mpsat.tasks.PunfTask;
-import org.workcraft.plugins.pcomp.PCompOutputMode;
 import org.workcraft.plugins.pcomp.tasks.PcompTask;
+import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.plugins.stg.STG;
+import org.workcraft.plugins.stg.SignalTransition.Type;
 import org.workcraft.serialisation.Format;
 import org.workcraft.tasks.ProgressMonitor;
 import org.workcraft.tasks.Result;
@@ -62,6 +70,7 @@
 	
 	@Override
 	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
+		File workingDirectory = null;
 		try {
 			// Common variables
 			monitor.progressUpdate(0.05);
@@ -70,79 +79,76 @@
 				title = title.substring(0, title.length() - 5);
 			}
 			VisualCircuit visualCircuit = (VisualCircuit)we.getModelEntry().getVisualModel();
-			STG circuitStg = (STG)STGGenerator.generate(visualCircuit).getMathModel();
-			Exporter stgExporter = Export.chooseBestExporter(framework.getPluginManager(), circuitStg, Format.STG);
-			if (stgExporter == null) {
-				throw new RuntimeException ("Exporter not available: model class " + circuitStg.getClass().getName() + " to format STG.");
+			File envFile = visualCircuit.getEnvironmentFile(); 
+			boolean hasEnvironment = ((envFile != null) && envFile.exists()); 
+
+			workingDirectory = FileUtils.createTempDirectory(title + "-");
+
+			STG devStg = (STG)STGGenerator.generate(visualCircuit).getMathModel();
+			Exporter devStgExporter = Export.chooseBestExporter(framework.getPluginManager(), devStg, Format.STG);
+			if (devStgExporter == null) {
+				throw new RuntimeException ("Exporter not available: model class " + devStg.getClass().getName() + " to format STG.");
 			}
 			SubtaskMonitor<Object> subtaskMonitor = new SubtaskMonitor<Object>(monitor);
 			monitor.progressUpdate(0.10);
 
 			// Generating .g for the circuit
-			String circuitFilePrefix = title + "-circuit-";
-			File circuitStgFile = File.createTempFile(circuitFilePrefix.replaceAll("\\s",""), stgExporter.getExtenstion());
-			ExportTask circuitExportTask = new ExportTask(stgExporter, circuitStg, circuitStgFile.getCanonicalPath());
-			Result<? extends Object> circuitExportResult = framework.getTaskManager().execute(
-					circuitExportTask, "Exporting circuit .g", subtaskMonitor);
+			String devStgName = (hasEnvironment ? "dev.g" : "system.g");
+			File devStgFile =  new File(workingDirectory, devStgName);
+			ExportTask devExportTask = new ExportTask(devStgExporter, devStg, devStgFile.getCanonicalPath());
+			Result<? extends Object> devExportResult = framework.getTaskManager().execute(
+					devExportTask, "Exporting circuit .g", subtaskMonitor);
 			
-			if (circuitExportResult.getOutcome() != Outcome.FINISHED) {
-				circuitStgFile.delete();
-				if (circuitExportResult.getOutcome() == Outcome.CANCELLED) {
+			if (devExportResult.getOutcome() != Outcome.FINISHED) {
+				if (devExportResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(circuitExportResult, null, null, null, toolchainPreparationSettings));
+						new MpsatChainResult(devExportResult, null, null, null, toolchainPreparationSettings));
 			}
 			monitor.progressUpdate(0.20);
 			
 			// Generating .g for the environment
-			File stgFile;
 			STG stg;
+			File stgFile = null;
 			Result<? extends ExternalProcessResult>  pcompResult = null;
-			File environmentFile = visualCircuit.getEnvironmentFile(); 
-			boolean hasEnvironment = ((environmentFile != null) && environmentFile.exists()); 
 			if ( !hasEnvironment ) {
-				 // No environment to compose with
-				 stgFile = circuitStgFile;
-				 stg = circuitStg;
+				 stgFile = devStgFile;
+				 stg = devStg;
 			} else {
-				// Compose circuit with its environment
-				File environmentStgFile;
-				if (environmentFile.getName().endsWith(".g")) {
-					environmentStgFile = environmentFile;
+				File envStgFile = null;
+				if (envFile.getName().endsWith(".g")) {
+					envStgFile = envFile;
 				} else {
-					STG environementStg = (STG)framework.loadFile(environmentFile).getMathModel();
-					String environmentFilePrefix = title + "-environment-";
-					environmentStgFile = File.createTempFile(environmentFilePrefix.replaceAll("\\s",""), stgExporter.getExtenstion());
-					ExportTask environmentExportTask = new ExportTask(stgExporter, environementStg, environmentStgFile.getCanonicalPath());
-					Result<? extends Object> environmentExportResult = framework.getTaskManager().execute(
-							environmentExportTask, "Exporting environment .g", subtaskMonitor);
+					STG envStg = (STG)framework.loadFile(envFile).getMathModel();
+					Exporter envStgExporter = Export.chooseBestExporter(framework.getPluginManager(), envStg, Format.STG);
+					envStgFile = new File(workingDirectory, "env.g");
+					ExportTask envExportTask = new ExportTask(envStgExporter, envStg, envStgFile.getCanonicalPath());
+					Result<? extends Object> envExportResult = framework.getTaskManager().execute(
+							envExportTask, "Exporting environment .g", subtaskMonitor);
 					
-					if (environmentExportResult.getOutcome() != Outcome.FINISHED) {
-						environmentStgFile.delete();
-						if (environmentExportResult.getOutcome() == Outcome.CANCELLED) {
+					if (envExportResult.getOutcome() != Outcome.FINISHED) {
+						if (envExportResult.getOutcome() == Outcome.CANCELLED) {
 							return new Result<MpsatChainResult>(Outcome.CANCELLED);
 						}
 						return new Result<MpsatChainResult>(Outcome.FAILED, 
-								new MpsatChainResult(environmentExportResult, null, null, null, toolchainPreparationSettings));
+								new MpsatChainResult(envExportResult, null, null, null, toolchainPreparationSettings));
 					}
 				}
 				monitor.progressUpdate(0.25);
 
 				// Generating .g for the whole system (circuit and environment)
-				String systemFilePrefix = title + "-system-";
-				stgFile = File.createTempFile(systemFilePrefix.replaceAll("\\s",""), stgExporter.getExtenstion());
-				PcompTask pcompTask = new PcompTask(new File[]{circuitStgFile, environmentStgFile}, PCompOutputMode.OUTPUT, true, false);
+				stgFile = new File(workingDirectory, "system.g");
+				PcompTask pcompTask = new PcompTask(new File[]{devStgFile, envStgFile}, ConversionMode.OUTPUT, true, false, workingDirectory);
 				pcompResult = framework.getTaskManager().execute(
 						pcompTask, "Running pcomp", subtaskMonitor);
 				
 				if (pcompResult.getOutcome() != Outcome.FINISHED) {
-					circuitStgFile.delete();
 					if (pcompResult.getOutcome() == Outcome.CANCELLED) {
 						return new Result<MpsatChainResult>(Outcome.CANCELLED);
 					}
 					return new Result<MpsatChainResult>(Outcome.FAILED, 
-							new MpsatChainResult(circuitExportResult, pcompResult, null, null, toolchainPreparationSettings));
+							new MpsatChainResult(devExportResult, pcompResult, null, null, toolchainPreparationSettings));
 				}
 				FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput()));
 				WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true);
@@ -151,26 +157,26 @@
 			monitor.progressUpdate(0.30);
 
 			// Generate unfolding
-			String unfoldingFilePrefix = title + "-unfolding-";
-			File unfoldingFile = File.createTempFile(unfoldingFilePrefix.replaceAll("\\s",""), MpsatUtilitySettings.getUnfoldingExtension());
+			File unfoldingFile = new File(workingDirectory, "system" + MpsatUtilitySettings.getUnfoldingExtension());
 			PunfTask punfTask = new PunfTask(stgFile.getCanonicalPath(), unfoldingFile.getCanonicalPath());
 			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
 					punfTask, "Unfolding .g", subtaskMonitor);
 			
-			stgFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				unfoldingFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainPreparationSettings));
+						new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainPreparationSettings));
 			}
 			monitor.progressUpdate(0.40);
 			
 			// Check for interface conformation (only if the environment is specified) 
 			if (hasEnvironment && checkConformation) {
-				String reachConformation = MpsatSettings.genReachConformation(stg, circuitStg);
+				Set<String> devOutputNames = devStg.getSignalFlatNames(Type.OUTPUT);
+				Set<String> devPlaceNames = parsePlaceNames(pcompResult.getReturnValue().getOutputFile("places.list"), 0);
+//				String reachConformation = MpsatSettings.genReachConformation(devOutputNames, devPlaceNames);
+				String reachConformation = MpsatSettings.genReachConformationDetail(stg, devOutputNames, devPlaceNames);
 				if (MpsatUtilitySettings.getDebugReach()) {
 					System.out.println("\nReach expression for the interface conformation property:");
 					System.out.println(reachConformation);
@@ -179,7 +185,8 @@
 						MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), 
 						MpsatUtilitySettings.getSolutionCount(), reachConformation);
 				
-				MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath());
+				MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), 
+						unfoldingFile.getCanonicalPath(), workingDirectory);
 				Result<? extends ExternalProcessResult>  mpsatConformationResult = framework.getTaskManager().execute(
 						mpsatConformationTask, "Running conformation check [MPSat]", subtaskMonitor);
 
@@ -188,15 +195,14 @@
 						return new Result<MpsatChainResult>(Outcome.CANCELLED);
 					}
 					return new Result<MpsatChainResult>(Outcome.FAILED, 
-							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings));
+							new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings));
 				}
 				monitor.progressUpdate(0.50);
 
 				MpsatResultParser mpsatConformationParser = new MpsatResultParser(mpsatConformationResult.getReturnValue());
 				if (!mpsatConformationParser.getSolutions().isEmpty()) {
-					unfoldingFile.delete();
 					return new Result<MpsatChainResult>(Outcome.FINISHED, 
-							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, 
+							new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, 
 									"Circuit does not conform to the environment after the following trace:"));
 				}
 			}
@@ -204,7 +210,8 @@
 			
 			// Check for deadlock
 			if (checkDeadlock) {
-				MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath());
+				MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(), 
+						unfoldingFile.getCanonicalPath(), workingDirectory);
 				Result<? extends ExternalProcessResult> mpsatDeadlockResult = framework.getTaskManager().execute(
 						mpsatDeadlockTask, "Running deadlock check [MPSat]", subtaskMonitor);
 			
@@ -213,15 +220,14 @@
 						return new Result<MpsatChainResult>(Outcome.CANCELLED);
 					}
 					return new Result<MpsatChainResult>(Outcome.FAILED, 
-							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings));
+							new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings));
 				}
 				monitor.progressUpdate(0.70);
 			
 				MpsatResultParser mpsatDeadlockParser = new MpsatResultParser(mpsatDeadlockResult.getReturnValue());
 				if (!mpsatDeadlockParser.getSolutions().isEmpty()) {
-					unfoldingFile.delete();
 					return new Result<MpsatChainResult>(Outcome.FINISHED, 
-							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings, 
+							new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings, 
 									"Circuit has a deadlock after the following trace:"));
 				}
 			}
@@ -229,7 +235,8 @@
 			
 			// Check for hazards
 			if (checkHazard) {
-				MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath());
+				MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(), 
+						unfoldingFile.getCanonicalPath(), workingDirectory);
 				if (MpsatUtilitySettings.getDebugReach()) {
 					System.out.println("\nReach expression for the hazard property:");
 					System.out.println(hazardSettings.getReach());
@@ -242,44 +249,72 @@
 						return new Result<MpsatChainResult>(Outcome.CANCELLED);
 					}
 					return new Result<MpsatChainResult>(Outcome.FAILED, 
-							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings));
+							new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings));
 				}
 				monitor.progressUpdate(0.90);
 
 				MpsatResultParser mpsatHazardParser = new MpsatResultParser(mpsatHazardResult.getReturnValue());
 				if (!mpsatHazardParser.getSolutions().isEmpty()) {
-					unfoldingFile.delete();
 					return new Result<MpsatChainResult>(Outcome.FINISHED, 
-							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings, 
+							new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings, 
 									"Circuit has a hazard  after the following trace:"));
 				}
 			}
 			monitor.progressUpdate(1.0);
 
 			// Success
-			unfoldingFile.delete();
-			String message = "";
-			if (hasEnvironment) {
-				message = "Under the given environment (" + environmentFile.getName() + ")";
-			} else {
-				message = "Without environment restrictions";
-			}
-			message +=  " the circuit is:\n";
-			if (checkConformation) {
-				message += "  * conformant\n";
-			}
-			if (checkDeadlock) {
-				message += "  * deadlock-free\n";
-			}
-			if (checkHazard) {
-				message += "  * hazard-free\n";
-			}
+			String message = getSuccessMessage(envFile);
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message));
+					new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message));
 
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
-		}
+		} finally {
+			if ((workingDirectory != null) && !MpsatUtilitySettings.getDebugTemporaryFiles()) {
+				FileUtils.deleteDirectoryTree(workingDirectory);
+			}
+		}
+	}
+
+	private HashSet<String> parsePlaceNames(byte[] bufferedInput, int lineIndex) {
+		HashSet<String> result = new HashSet<String>();
+		InputStream is = new ByteArrayInputStream(bufferedInput);
+	    BufferedReader br = new BufferedReader(new InputStreamReader(is));
+		try {
+			String line = null;
+			while ((lineIndex >= 0) && ((line = br.readLine()) != null)) {
+				lineIndex--;
+			}
+			if (line != null) {
+				for (String name: line.trim().split("\\s")) {
+					result.add(name);
+				}
+			}
+		} catch (IOException e) {
+			e.printStackTrace();
+		}
+		return result;
+	}
+
+	private String getSuccessMessage(File environmentFile) {
+		String message = "";
+		boolean hasEnvironment = ((environmentFile != null) && environmentFile.exists()); 
+		if (hasEnvironment) {
+			message = "Under the given environment (" + environmentFile.getName() + ")";
+		} else {
+			message = "Without environment restrictions";
+		}
+		message +=  " the circuit is:\n";
+		if (checkConformation) {
+			message += "  * conformant\n";
+		}
+		if (checkDeadlock) {
+			message += "  * deadlock-free\n";
+		}
+		if (checkHazard) {
+			message += "  * hazard-free\n";
+		}
+		return message;
 	}
 
 }
 
=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java	2014-11-21 18:25:23 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java	2014-11-30 23:14:46 +0000
@@ -451,7 +451,7 @@
 		Node parent = contact.getParent();
 		if (parent instanceof VisualFunctionComponent) {
 			VisualFunctionComponent component = (VisualFunctionComponent)parent;
-			String componentName = NamespaceHelper.getFlatName(circuit.getMathName(component));
+			String componentName = NamespaceHelper.hierarchicalToFlatName(circuit.getMathName(component));
 			String contactName = circuit.getMathName(contact);
 			result = componentName + "_" + contactName;
 		}
@@ -470,7 +470,7 @@
 				result = circuit.getMathName(outputPort); 
 			} else {
 				// If the component has a single output, use the component name. Otherwise append the contact.
-				result = NamespaceHelper.getFlatName(circuit.getMathName(component));
+				result = NamespaceHelper.hierarchicalToFlatName(circuit.getMathName(component));
 				int output_cnt = 0;
 				for (Node node: component.getChildren()) {
 					if (node instanceof VisualContact) {
 
=== modified file 'CpogsPlugin/src/org/workcraft/plugins/cpog/serialisation/BooleanFormulaSerialiser.java'
--- CpogsPlugin/src/org/workcraft/plugins/cpog/serialisation/BooleanFormulaSerialiser.java	2014-07-11 09:35:42 +0000
+++ CpogsPlugin/src/org/workcraft/plugins/cpog/serialisation/BooleanFormulaSerialiser.java	2014-11-30 23:14:46 +0000
@@ -61,7 +61,7 @@
 				
 				String ref = internalReferences.getReference(node);
 				// use full path to a flattened name
-				String flat = NamespaceHelper.getFlatName(ref);
+				String flat = NamespaceHelper.hierarchicalToFlatName(ref);
 				
 				// old style naming, if number is used as an ID for a contact
 				if (Identifier.isNumber(ref)) {
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatCscResolutionResultHandler.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatCscResolutionResultHandler.java	2013-09-18 16:19:20 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatCscResolutionResultHandler.java	2014-11-30 23:14:46 +0000
@@ -28,12 +28,11 @@
 				this.result = result;
 	}
 	
-	public STGModel getResolvedStg()
-	{
+	public STGModel getResolvedStg() {
 		final byte[] output = result.getReturnValue().getMpsatResult().getReturnValue().getOutputFile("mpsat.g");
-		if(output == null)
+		if(output == null) {
 			return null;
-		
+		}
 		try {
 			return new DotGImporter().importSTG(new ByteArrayInputStream(output));
 		} catch (DeserialisationException e) {
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatModule.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatModule.java	2014-10-24 16:33:38 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatModule.java	2014-11-30 23:14:46 +0000
@@ -6,13 +6,13 @@
 import org.workcraft.Tool;
 import org.workcraft.gui.propertyeditor.Settings;
 import org.workcraft.plugins.mpsat.tools.CscResolutionTool;
-import org.workcraft.plugins.mpsat.tools.CustomPropertyMpsatChecker;
+import org.workcraft.plugins.mpsat.tools.MpsatConformationChecker;
 import org.workcraft.plugins.mpsat.tools.MpsatConsistencyChecker;
 import org.workcraft.plugins.mpsat.tools.MpsatCscChecker;
+import org.workcraft.plugins.mpsat.tools.MpsatCustomPropertyChecker;
 import org.workcraft.plugins.mpsat.tools.MpsatDeadlockChecker;
 import org.workcraft.plugins.mpsat.tools.MpsatNormalcyChecker;
 import org.workcraft.plugins.mpsat.tools.MpsatPersistencyChecker;
-import org.workcraft.plugins.mpsat.tools.MpsatSynthesis;
 import org.workcraft.plugins.mpsat.tools.MpsatSynthesisComplexGate;
 import org.workcraft.plugins.mpsat.tools.MpsatSynthesisGeneralisedCelement;
 import org.workcraft.plugins.mpsat.tools.MpsatSynthesisStandardCelement;
@@ -38,7 +38,8 @@
 		p.registerClass(Tool.class, MpsatNormalcyChecker.class, framework);
 		p.registerClass(Tool.class, MpsatCscChecker.class, framework);
 		p.registerClass(Tool.class, MpsatUscChecker.class, framework);
-		p.registerClass(Tool.class, CustomPropertyMpsatChecker.class, framework);
+		p.registerClass(Tool.class, MpsatConformationChecker.class, framework);
+		p.registerClass(Tool.class, MpsatCustomPropertyChecker.class, framework);
 		
 		p.registerClass(Settings.class, MpsatUtilitySettings.class);
 		p.registerClass(Settings.class, PunfUtilitySettings.class);
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java	2014-11-13 00:05:09 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java	2014-11-30 23:14:46 +0000
@@ -6,9 +6,10 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
-import java.util.HashSet;
+import java.util.Collection;
 import java.util.LinkedHashMap;
 import java.util.Map;
+import java.util.Set;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
@@ -16,7 +17,7 @@
 import org.workcraft.dom.hierarchy.NamespaceHelper;
 import org.workcraft.plugins.stg.STG;
 import org.workcraft.plugins.stg.SignalTransition;
-import org.workcraft.plugins.stg.SignalTransition.Type;
+import org.workcraft.plugins.stg.SignalTransition.Direction;
 import org.workcraft.util.FileUtils;
 
 public class MpsatSettings {
@@ -53,134 +54,158 @@
 	// Reach expression for checking signal consistency
 	public static final String reachConsistency = 
 		"exists s in SIGNALS \\ DUMMY {\n" +
-		"  let Es = ev s {\n" +
-		"    $s & exists e in Es s.t. is_plus e { @e }\n" +
-		"    |\n" +
-		"    ~$s & exists e in Es s.t. is_minus e { @e }\n" +
-		"  }\n" +
+		"    let Es = ev s {\n" +
+		"        $s & exists e in Es s.t. is_plus e { @e }\n" +
+		"        |\n" +
+		"        ~$s & exists e in Es s.t. is_minus e { @e }\n" +
+		"    }\n" +
 		"}\n";
 
 	// Reach expression for checking semimodularity (output persistency)
 	public static final String reachSemimodularity =
 		"card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n" +
-		"  exists t1 in tran EVENTS s.t. sig t1 in LOCAL {\n" +
-		"    @t1 &\n" +
-		"    exists t2 in tran EVENTS s.t. sig t2 != sig t1 & card (pre t1 * (pre t2 \\ post t2)) != 0 {\n" +
-		"      @t2 &\n" +
-		"      forall t3 in tran EVENTS * (tran sig t1 \\ {t1}) s.t. card (pre t3 * (pre t2 \\ post t2)) = 0 {\n" +
-		"        exists p in pre t3 \\ post t2 { ~$p }\n" +
-		"      }\n" +
-		"    }\n" +
-		"  }\n";
+		"    exists t1 in tran EVENTS s.t. sig t1 in LOCAL {\n" +
+		"        @t1 &\n" +
+		"        exists t2 in tran EVENTS s.t. sig t2 != sig t1 & card (pre t1 * (pre t2 \\ post t2)) != 0 {\n" +
+		"            @t2 &\n" +
+		"            forall t3 in tran EVENTS * (tran sig t1 \\ {t1}) s.t. card (pre t3 * (pre t2 \\ post t2)) = 0 {\n" +
+		"                exists p in pre t3 \\ post t2 { ~$p }\n" +
+		"            }\n" +
+		"        }\n" +
+		"    }\n";
 	
 	// Reach expression for checking conformation (this is a template, 
 	// the list of places needs to be updated for each circuit)
 	public static final String reachConformation =
-		"card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n" +
-		"  let CPnames = {\"in1_0\", \"in1_1\", \"in0_0\", \"in0_1\", \"out0_0\", \"out0_1\"},\n" +
-		"  CP=gather n in CPnames { P n } {\n" +
-		"    exists s in SIGNALS \\ DUMMY {\n" +
-		"      exists t in tran s {\n" +
-		"        forall p in pre t * CP { $p }\n" +
-		"      }\n" +
-		"      &\n" +
-		"      forall t in tran s {\n" +
-		"        exists p in pre t \\ CP { ~$p }\n" +
-		"      }\n" +
-		"    }\n" +
-		"  }\n";
-	
+//			"let devOutputs = gather signalName in { \"out0\" } { S signalName },\n" +
+//			"    devPlaces = gather placeName in { \"in1_0\", \"in1_1\", \"in0_1\", \"in0_0\", \"<out0+,out0->\", \"<out0-,out0+>\" } { P placeName } {\n" +
+			"    card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n" +
+			"    exists s in devOutputs {\n" +
+			"        exists t in tran s {\n" +
+			"            is_plus t & forall p in pre t * devPlaces { $ p }\n" +
+			"        }\n" +
+			"        &\n" +
+			"        forall t in tran s {\n" +
+			"            is_plus t & exists p in pre t \\ devPlaces { ~ $ p }\n" +
+			"        }\n" +
+			"        |\n" +
+			"        exists t in tran s {\n" +
+			"            is_minus t & forall p in pre t * devPlaces { $ p }\n" +
+			"        }\n" +
+			"        &\n" +
+			"        forall t in tran s {\n" +
+			"            is_minus t & exists p in pre t \\ devPlaces { ~ $ p }\n" +
+			"        }\n" +
+			"    }\n" +
+			"}\n";
+
 	// Note: New (PNML-based) version of Punf is required to check conformation property. 
 	// Old version of Punf does not support dead signals, transitions and places well 
 	// (e.g. a dead transition may disappear from unfolding), therefore the conformation 
 	// property cannot be checked reliably.
-	public static String genReachConformation(STG stg, STG circuitStg) {
-		// Form a set of system STG places which came from the circuitStg 
-		HashSet<Node> circuitPlaces = new HashSet<Node>();
-		for (Type type: Type.values()) {
-			for (String s : circuitStg.getSignalReferences(type)) {
-				Node p0 = stg.getNodeByReference(s + "_0");
-				if (p0 == null) {
-					p0 = stg.getNodeByReference("<" + s + "-," + s + "+>");
-				}
-				if (p0 != null) {
-					circuitPlaces.add(p0);
-				}
-				Node p1 = stg.getNodeByReference(s + "_1");
-				if (p1 == null) {
-					p1 = stg.getNodeByReference("<" + s + "+," + s + "->");
-				}
-				if (p1 != null) {
-					circuitPlaces.add(p1);
-				}
+	public static String genReachConformation(Set<String> devOutputNames, Set<String> devPlaceNames) {
+		String devOutputList = genNameList(devOutputNames);
+		String devPlaceList = genNameList(devPlaceNames);
+		return "let devOutputs = gather signalName in { " + devOutputList + " } { S signalName },\n" + 
+			   "    devPlaces = gather placeName in { " + devPlaceList + " } { P placeName } {\n" +
+			   reachConformation;
+	}
+	
+	private static String genNameList(Collection<String> names) {
+		String result = "";
+		for (String name: names) {
+			if ( !result.isEmpty() ) {
+				result += ", ";
 			}
+			result += "\"" + name + "\"";
 		}
-		// Generate Reach expression
+		return result;
+	}
+	
+	public static String genReachConformationDetail(STG stg, Set<String> devOutputNames, Set<String> devPlaceNames) {
 		String result = "";
-		for (String s : circuitStg.getSignalReferences(Type.OUTPUT)) {
-			String circuitPredicate = "";
-			String environmentPredicate = "";
-			for (SignalTransition t: stg.getSignalTransitions()) {
-				if (!t.getSignalType().equals(Type.OUTPUT) || !t.getSignalName().equals(s)) continue;
-				String circuitPreset = "";
-				String environmentPreset = "";
+		for (String signalFlatName: devOutputNames) {
+			String riseDevPredicate = "";
+			String fallDevPredicate = "";
+			String riseEnvPredicate = "";
+			String fallEnvPredicate = "";
+
+			String signalRef = NamespaceHelper.flatToHierarchicalName(signalFlatName);
+			for (SignalTransition t: stg.getSignalTransitions(signalRef)) {
+				String devPreset = "";
+				String envPreset = "";
 				for (Node p: stg.getPreset(t)) {
-					String name = stg.getNodeReference(p);
-					if (circuitPlaces.contains(p)) {
-						if (circuitPreset.isEmpty()) {
-							circuitPreset += "{";
-						} else {
-							circuitPreset += ", ";
-						}
-						circuitPreset += "\"" + name + "\"";
+					String placeRef = stg.getNodeReference(p);
+					String placeFlatName = NamespaceHelper.hierarchicalToFlatName(placeRef);
+					if (devPlaceNames.contains(placeFlatName)) {
+						devPreset += (devPreset.isEmpty() ? "{" : ", ");
+						devPreset += "\"" + placeFlatName + "\"";
+					}
+					envPreset += (envPreset.isEmpty() ? "{" : ", ");
+					envPreset += "\"" + placeFlatName + "\"";
+				}
+				
+				if ( !devPreset.isEmpty() && !envPreset.isEmpty() ) {
+					devPreset += "}";
+					envPreset += "}";
+					String devPredicate = "";
+					devPredicate += "        forall p in " + devPreset  + " {\n";
+					devPredicate += "            $ P p\n";
+					devPredicate += "        }\n";
+					String envPredicate = "";
+					envPredicate += "        exists p in " + envPreset  + " {\n";
+					envPredicate += "          ~$ P p\n";
+					envPredicate += "        }\n";
+					if (t.getDirection() == Direction.PLUS) {
+						if ( !riseDevPredicate.isEmpty() ) {
+							riseDevPredicate += "        |\n";
+						}
+						riseDevPredicate += devPredicate;
+						if ( !riseEnvPredicate.isEmpty() ) {
+							riseEnvPredicate += "        &\n";
+						}
+						riseEnvPredicate += envPredicate;
 					} else {
-						if (environmentPreset.isEmpty()) {
-							environmentPreset += "{";
-						} else {
-							environmentPreset += ", ";
-						}
-						environmentPreset += "\"" + name + "\"";
+						if ( !fallDevPredicate.isEmpty() ) {
+							fallDevPredicate += "        |\n";
+						}
+						fallDevPredicate += devPredicate;
+						if ( !fallEnvPredicate.isEmpty() ) {
+							fallEnvPredicate += "        &\n";
+						}
+						fallEnvPredicate += envPredicate;
 					}
 				}
-				circuitPreset += "}";
-				environmentPreset += "}";
-
-				if (circuitPredicate.isEmpty()) {
-					circuitPredicate += "   (\n";
-				} else {
-					circuitPredicate += "      |\n";
-				}
-				circuitPredicate += "      forall p in " + circuitPreset  + " {\n";
-				circuitPredicate += "         $ P p\n";
-				circuitPredicate += "      }\n";
-
-				if (environmentPredicate.isEmpty()) {
-					environmentPredicate += "   (\n";
-				} else {
-					environmentPredicate += "      &\n";
-				}
-				environmentPredicate += "      exists p in " + environmentPreset  + " {\n";
-				environmentPredicate += "         ~$ P p\n";
-				environmentPredicate += "      }\n";
-			}
-			circuitPredicate += "   )\n";
-			environmentPredicate += "   )\n";
-			if (result.isEmpty()) {
-				result = "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n";
-			} else {
-				result += "|\n";
-			}
-			result += "/* Conformation check for signal " + s + " */\n";
-			result += "(\n";
-			result += circuitPredicate;
-			result += "   &\n";
-			result += environmentPredicate;
-			result += ")\n";
+			}
+			
+			if ( !riseDevPredicate.isEmpty() || !fallDevPredicate.isEmpty() ) {
+				if (result.isEmpty()) {
+					result = "card DUMMY != 0 ? fail \"This property can be checked only on STGs without dummies\" :\n";
+				} else {
+					result += "|\n";
+				}
+				result += "(  /* Conformation check for signal \"" + signalFlatName + "\" */\n";
+				result += "    (\n";
+				result +=          riseDevPredicate;
+				result += "    )\n";
+				result += "    &\n";
+				result += "    (\n";
+				result +=          riseEnvPredicate;
+				result += "    )\n";
+				result += "    |\n";
+				result += "    (\n";
+				result +=          fallDevPredicate;
+				result += "    )\n";
+				result += "    &\n";
+				result += "    (\n";
+				result +=          fallEnvPredicate;
+				result += "    )\n";
+				result += ")\n";
+			}
 		}
 		return result;
 	}
 
-	
 	public MpsatSettings(String name, MpsatMode mode, int verbosity, SolutionMode solutionMode, int solutionNumberLimit, String reach) {
 		super();
 		this.name = name;
@@ -212,7 +237,7 @@
 		Matcher matcher = nodeNamePattern.matcher(reach);
 		while (matcher.find()) {
 			String reference = matcher.group(1);
-			String flatName = NamespaceHelper.getFlatName(reference);
+			String flatName = NamespaceHelper.hierarchicalToFlatName(reference);
 			matcher.appendReplacement(sb, "\"" + flatName + "\"");
 		}
 		matcher.appendTail(sb);
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java	2014-09-05 16:36:36 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java	2014-11-30 23:14:46 +0000
@@ -38,18 +38,21 @@
 	private static final String keyExtraArgs = prefix + ".args";
 	private static final String keyUsePnmlUnfolding = prefix + ".usePnmlUnfolding";
 	private static final String keyDebugReach = prefix + ".debugReach";
+	private static final String keyDebugTemporaryFiles = prefix + ".debugTemporaryFiles";
 	
 	private static final String defaultCommand = "mpsat";
 	private static final SolutionMode defaultSolutionMode = SolutionMode.MINIMUM_COST;
 	private static final String defaultExtraArgs = "";
 	private static final Boolean defaultUsePnmlUnfolding = false;
 	private static final Boolean defaultDebugReach = false;
+	private static final Boolean defaultDebugTemporaryFiles = true;
 
 	private static String command = defaultCommand;
 	private static SolutionMode solutionMode = defaultSolutionMode;
 	private static String extraArgs = defaultExtraArgs;
 	private static Boolean usePnmlUnfolding = defaultUsePnmlUnfolding;
 	private static Boolean debugReach = defaultDebugReach;
+	private static Boolean debigTemporaryFiles = defaultDebugTemporaryFiles;
 
 	public MpsatUtilitySettings() {
 		properties.add(new PropertyDeclaration<MpsatUtilitySettings, String>(
@@ -93,7 +96,7 @@
 		});
 
 		properties.add(new PropertyDeclaration<MpsatUtilitySettings, Boolean>(
-				this, "Debug Reach expressions", Boolean.class) {
+				this, "Print out Reach expressions (debug)", Boolean.class) {
 			protected void setter(MpsatUtilitySettings object, Boolean value) {
 				MpsatUtilitySettings.setDebugReach(value);
 			}
@@ -101,6 +104,16 @@
 				return MpsatUtilitySettings.getDebugReach();
 			}
 		});
+
+		properties.add(new PropertyDeclaration<MpsatUtilitySettings, Boolean>(
+				this, "Keep temporary files (debug)", Boolean.class) {
+			protected void setter(MpsatUtilitySettings object, Boolean value) {
+				MpsatUtilitySettings.setDebugTemporaryFiles(value);
+			}
+			protected Boolean getter(MpsatUtilitySettings object) {
+				return MpsatUtilitySettings.getDebugTemporaryFiles();
+			}
+		});
 	}
 	
 	@Override
@@ -115,6 +128,7 @@
 		setExtraArgs(config.getString(keyExtraArgs, defaultExtraArgs));
 		setUsePnmlUnfolding(config.getBoolean(keyUsePnmlUnfolding, defaultUsePnmlUnfolding));
 		setDebugReach(config.getBoolean(keyDebugReach, defaultDebugReach));
+		setDebugTemporaryFiles(config.getBoolean(keyDebugTemporaryFiles, defaultDebugTemporaryFiles));
 	}
 
 	@Override
@@ -124,6 +138,8 @@
 		config.set(keyExtraArgs, getExtraArgs());
 		config.setBoolean(keyUsePnmlUnfolding, getUsePnmlUnfolding());
 		config.setBoolean(keyDebugReach, getDebugReach());
+		config.setBoolean(keyDebugTemporaryFiles, getDebugTemporaryFiles());
+		
 	}
 	
 	@Override
@@ -171,7 +187,7 @@
 	public static void setUsePnmlUnfolding(Boolean value) {
 		usePnmlUnfolding = value;
 	}
-
+	
 	public static Boolean getDebugReach() {
 		return debugReach;
 	}
@@ -180,6 +196,14 @@
 		debugReach = value;
 	}
 	
+	public static Boolean getDebugTemporaryFiles() {
+		return debigTemporaryFiles;
+	}
+
+	public static void setDebugTemporaryFiles(Boolean value) {
+		debigTemporaryFiles = value;
+	}
+	
 	public static String getUnfoldingExtension() {
 		return (getUsePnmlUnfolding() ? ".pnml" : ".mci");
 	}
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java	2014-09-05 16:36:36 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java	2014-11-30 23:14:46 +0000
@@ -11,44 +11,41 @@
 import org.workcraft.serialisation.Format;
 import org.workcraft.tasks.ProgressMonitor;
 import org.workcraft.tasks.Result;
+import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.tasks.SubtaskMonitor;
 import org.workcraft.tasks.Task;
-import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.util.Export;
+import org.workcraft.util.Export.ExportTask;
 import org.workcraft.util.WorkspaceUtils;
-import org.workcraft.util.Export.ExportTask;
 import org.workcraft.workspace.WorkspaceEntry;
 
 public class MpsatChainTask implements Task<MpsatChainResult> {
 	private final WorkspaceEntry we;
 	private final MpsatSettings settings;
 	private final Framework framework;
-	private PetriNetModel model;
 
 	public MpsatChainTask(WorkspaceEntry we, MpsatSettings settings, Framework framework) {
 		this.we = we;
 		this.settings = settings;
 		this.framework = framework;
-		this.model = null;
 	}
 	
 	@Override
 	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
+		File netFile = null;
+		File unfoldingFile = null;
 		try {
-			if(model == null) {
-				model = WorkspaceUtils.getAs(getWorkspaceEntry(), PetriNetModel.class);
-			}
+			PetriNetModel model = WorkspaceUtils.getAs(we, PetriNetModel.class);
 			Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG);
 			if (exporter == null) {
 				throw new RuntimeException ("Exporter not available: model class " + model.getClass().getName() + " to format STG.");
 			}
-			File netFile = File.createTempFile("net", exporter.getExtenstion());
+			netFile = File.createTempFile("net", exporter.getExtenstion());
 			ExportTask exportTask;
 			exportTask = new ExportTask(exporter, model, netFile.getCanonicalPath());
 			SubtaskMonitor<Object> mon = new SubtaskMonitor<Object>(monitor);
 			Result<? extends Object> exportResult = framework.getTaskManager().execute(exportTask, "Exporting .g", mon);
 			if (exportResult.getOutcome() != Outcome.FINISHED) {
-				netFile.delete();
 				if (exportResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
@@ -56,13 +53,11 @@
 			}
 			monitor.progressUpdate(0.33);
 			
-			File unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension());
+			unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension());
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), unfoldingFile.getCanonicalPath());
 			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
-			netFile.delete();
 			
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				unfoldingFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
@@ -71,9 +66,8 @@
 
 			monitor.progressUpdate(0.66);
 
-			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), unfoldingFile.getCanonicalPath());
+			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), unfoldingFile.getCanonicalPath(), null);
 			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running mpsat model-checking", mon);
-			unfoldingFile.delete();
 			
 			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
 				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
@@ -88,6 +82,15 @@
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
 		}
+		// Clean up
+		finally {
+			if ((netFile != null) && !MpsatUtilitySettings.getDebugTemporaryFiles() ) {
+				netFile.delete();
+			}
+			if ((unfoldingFile != null) && !MpsatUtilitySettings.getDebugTemporaryFiles() ) {
+				unfoldingFile.delete();
+			}
+		}
 	}
 	
 	public MpsatSettings getSettings() {
 
=== added file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java	1970-01-01 00:00:00 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java	2014-11-30 23:14:46 +0000
@@ -0,0 +1,215 @@
+package org.workcraft.plugins.mpsat.tasks;
+
+import java.io.BufferedReader;
+import java.io.ByteArrayInputStream;
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.InputStreamReader;
+import java.util.HashSet;
+import java.util.Set;
+
+import org.workcraft.Framework;
+import org.workcraft.interop.Exporter;
+import org.workcraft.plugins.mpsat.MpsatMode;
+import org.workcraft.plugins.mpsat.MpsatResultParser;
+import org.workcraft.plugins.mpsat.MpsatSettings;
+import org.workcraft.plugins.mpsat.MpsatUtilitySettings;
+import org.workcraft.plugins.pcomp.tasks.PcompTask;
+import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode;
+import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
+import org.workcraft.plugins.stg.STG;
+import org.workcraft.plugins.stg.SignalTransition.Type;
+import org.workcraft.serialisation.Format;
+import org.workcraft.tasks.ProgressMonitor;
+import org.workcraft.tasks.Result;
+import org.workcraft.tasks.Result.Outcome;
+import org.workcraft.tasks.SubtaskMonitor;
+import org.workcraft.util.Export;
+import org.workcraft.util.Export.ExportTask;
+import org.workcraft.util.FileUtils;
+import org.workcraft.workspace.WorkspaceEntry;
+
+
+public class MpsatConformationTask extends MpsatChainTask {
+	private final MpsatSettings toolchainPreparationSettings = new MpsatSettings("Toolchain preparation of data", 
+			MpsatMode.UNDEFINED, 0, null, 0, null);
+
+	private final MpsatSettings toolchainCompletionSettings = new MpsatSettings("Toolchain completion", 
+			MpsatMode.UNDEFINED, 0, null, 0, null);
+	
+	private final WorkspaceEntry we;
+	private final Framework framework;
+	private File envFile;
+	
+	public MpsatConformationTask(WorkspaceEntry we, Framework framework, File envFile) {
+		super (we, null, framework);
+		this.we = we;
+		this.framework = framework;
+		this.envFile = envFile;
+	}
+	
+	@Override
+	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
+		File workingDirectory = null;
+		try {
+			// Common variables
+			monitor.progressUpdate(0.10);
+			String title = we.getWorkspacePath().getNode();
+			if (title.endsWith(".work")) {
+				title = title.substring(0, title.length() - 5);
+			}
+			workingDirectory = FileUtils.createTempDirectory(title + "-");
+
+			STG devStg = (STG)we.getModelEntry().getVisualModel().getMathModel();
+			Exporter devStgExporter = Export.chooseBestExporter(framework.getPluginManager(), devStg, Format.STG);
+			if (devStgExporter == null) {
+				throw new RuntimeException ("Exporter not available: model class " + devStg.getClass().getName() + " to format STG.");
+			}
+			SubtaskMonitor<Object> subtaskMonitor = new SubtaskMonitor<Object>(monitor);
+			monitor.progressUpdate(0.20);
+
+			// Generating .g for the model
+			File devStgFile =  new File(workingDirectory, "dev.g");
+			ExportTask devExportTask = new ExportTask(devStgExporter, devStg, devStgFile.getCanonicalPath());
+			Result<? extends Object> devExportResult = framework.getTaskManager().execute(
+					devExportTask, "Exporting circuit .g", subtaskMonitor);
+			
+			if (devExportResult.getOutcome() != Outcome.FINISHED) {
+				if (devExportResult.getOutcome() == Outcome.CANCELLED) {
+					return new Result<MpsatChainResult>(Outcome.CANCELLED);
+				}
+				return new Result<MpsatChainResult>(Outcome.FAILED, 
+						new MpsatChainResult(devExportResult, null, null, null, toolchainPreparationSettings));
+			}
+			monitor.progressUpdate(0.30);
+			
+			// Generating .g for the environment
+			Result<? extends ExternalProcessResult>  pcompResult = null;
+			File envStgFile = null;
+			if (envFile.getName().endsWith(".g")) {
+				envStgFile = envFile;
+			} else {
+				STG envStg = (STG)framework.loadFile(envFile).getMathModel();
+				Exporter envStgExporter = Export.chooseBestExporter(framework.getPluginManager(), envStg, Format.STG);
+				envStgFile = new File(workingDirectory, "env.g");
+				ExportTask envExportTask = new ExportTask(envStgExporter, envStg, envStgFile.getCanonicalPath());
+				Result<? extends Object> envExportResult = framework.getTaskManager().execute(
+						envExportTask, "Exporting environment .g", subtaskMonitor);
+				
+				if (envExportResult.getOutcome() != Outcome.FINISHED) {
+					if (envExportResult.getOutcome() == Outcome.CANCELLED) {
+						return new Result<MpsatChainResult>(Outcome.CANCELLED);
+					}
+					return new Result<MpsatChainResult>(Outcome.FAILED, 
+							new MpsatChainResult(envExportResult, null, null, null, toolchainPreparationSettings));
+				}
+			}
+			monitor.progressUpdate(0.40);
+
+			// Generating .g for the whole system (model and environment)
+			File stgFile = new File(workingDirectory, "system.g");
+			PcompTask pcompTask = new PcompTask(new File[]{devStgFile, envStgFile}, ConversionMode.OUTPUT, true, false, workingDirectory);
+			pcompResult = framework.getTaskManager().execute(
+					pcompTask, "Running pcomp", subtaskMonitor);
+			
+			if (pcompResult.getOutcome() != Outcome.FINISHED) {
+				if (pcompResult.getOutcome() == Outcome.CANCELLED) {
+					return new Result<MpsatChainResult>(Outcome.CANCELLED);
+				}
+				return new Result<MpsatChainResult>(Outcome.FAILED, 
+						new MpsatChainResult(devExportResult, pcompResult, null, null, toolchainPreparationSettings));
+			}
+			FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput()));
+			WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true);
+			STG stg = (STG)stgWorkspaceEntry.getModelEntry().getMathModel();
+			monitor.progressUpdate(0.50);
+			
+			// Generate unfolding
+			File unfoldingFile = new File(workingDirectory, "system" + MpsatUtilitySettings.getUnfoldingExtension());
+			PunfTask punfTask = new PunfTask(stgFile.getCanonicalPath(), unfoldingFile.getCanonicalPath());
+			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
+					punfTask, "Unfolding .g", subtaskMonitor);
+			
+			if (punfResult.getOutcome() != Outcome.FINISHED) {
+				if (punfResult.getOutcome() == Outcome.CANCELLED) {
+					return new Result<MpsatChainResult>(Outcome.CANCELLED);
+				}
+				return new Result<MpsatChainResult>(Outcome.FAILED, 
+						new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainPreparationSettings));
+			}
+			monitor.progressUpdate(0.60);
+			
+			// Check for interface conformation
+			Set<String> devOutputNames = devStg.getSignalFlatNames(Type.OUTPUT);
+			Set<String> devPlaceNames = parsePlaceNames(pcompResult.getReturnValue().getOutputFile("places.list"), 0);
+//			String reachConformation = MpsatSettings.genReachConformation(devOutputNames, devPlaceNames);
+			String reachConformation = MpsatSettings.genReachConformationDetail(stg, devOutputNames, devPlaceNames);
+			if (MpsatUtilitySettings.getDebugReach()) {
+				System.out.println("\nReach expression for the interface conformation property:");
+				System.out.println(reachConformation);
+			}
+			MpsatSettings conformationSettings = new MpsatSettings("Interface conformation", 
+					MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), 
+					MpsatUtilitySettings.getSolutionCount(), reachConformation);
+			
+			MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), 
+					unfoldingFile.getCanonicalPath(), workingDirectory);
+			Result<? extends ExternalProcessResult>  mpsatConformationResult = framework.getTaskManager().execute(
+					mpsatConformationTask, "Running conformation check [MPSat]", subtaskMonitor);
+
+			if (mpsatConformationResult.getOutcome() != Outcome.FINISHED) {
+				if (mpsatConformationResult.getOutcome() == Outcome.CANCELLED) {
+					return new Result<MpsatChainResult>(Outcome.CANCELLED);
+				}
+				return new Result<MpsatChainResult>(Outcome.FAILED, 
+						new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings));
+			}
+			monitor.progressUpdate(0.80);
+
+			MpsatResultParser mpsatConformationParser = new MpsatResultParser(mpsatConformationResult.getReturnValue());
+			if (!mpsatConformationParser.getSolutions().isEmpty()) {
+				return new Result<MpsatChainResult>(Outcome.FINISHED, 
+						new MpsatChainResult(devExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, 
+								"This model does not conform to the environment after the following trace:"));
+			}
+			monitor.progressUpdate(1.0);
+
+			// Success
+			unfoldingFile.delete();
+			String message = "The model conforms to its environment (" + envFile.getName() + ").";
+			return new Result<MpsatChainResult>(Outcome.FINISHED, 
+					new MpsatChainResult(devExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message));
+
+		} catch (Throwable e) {
+			return new Result<MpsatChainResult>(e);
+		} finally {
+			if ((workingDirectory != null) && !MpsatUtilitySettings.getDebugTemporaryFiles()) {
+				FileUtils.deleteDirectoryTree(workingDirectory);
+			}
+		}
+	}
+	
+
+	private HashSet<String> parsePlaceNames(byte[] bufferedInput, int lineIndex) {
+		HashSet<String> result = new HashSet<String>();
+		InputStream is = new ByteArrayInputStream(bufferedInput);
+	    BufferedReader br = new BufferedReader(new InputStreamReader(is));
+		try {
+			String line = null;
+			while ((lineIndex >= 0) && ((line = br.readLine()) != null)) {
+				lineIndex--;
+			}
+			if (line != null) {
+				for (String name: line.trim().split("\\s")) {
+					result.add(name);
+				}
+			}
+		} catch (IOException e) {
+			e.printStackTrace();
+		}
+		return result;
+	}
+
+
+}
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java	2014-11-13 00:05:09 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatTask.java	2014-11-30 23:14:46 +0000
@@ -16,12 +16,21 @@
 import org.workcraft.util.FileUtils;
 
 public class MpsatTask implements Task<ExternalProcessResult> {
-	private String[] args;
-	private String inputFileName;
-			
+	private final String[] args;
+	private final String inputFileName;
+	private final File workingDirectory;
+	
 	public MpsatTask(String[] args, String inputFileName) {
+		this(args, inputFileName, null);
+	}
+
+	public MpsatTask(String[] args, String inputFileName, File workingDirectory) {
 		this.args = args;
 		this.inputFileName = inputFileName;
+		if (workingDirectory == null) {
+			workingDirectory = FileUtils.createTempDirectory("mpsat_");
+		}
+		this.workingDirectory = workingDirectory;
 	}
 	
 	@Override
@@ -43,23 +52,20 @@
 		// Input file argument
 		command.add(inputFileName);
 
-		File workingDir = FileUtils.createTempDirectory("mpsat_");
-		ExternalProcessTask externalProcessTask = new ExternalProcessTask(command, workingDir);
-		
+		ExternalProcessTask externalProcessTask = new ExternalProcessTask(command, workingDirectory);
 		Result<? extends ExternalProcessResult> res = externalProcessTask.run(monitor);
-		
-		if(res.getOutcome() == Outcome.CANCELLED)
+		if(res.getOutcome() == Outcome.CANCELLED) {
 			return res;
+		}
 		
 		Map<String, byte[]> outputFiles = new HashMap<String, byte[]>();
-		
 		try {
 			String unfoldingFileName = "mpsat" + MpsatUtilitySettings.getUnfoldingExtension();
-			File unfoldingFile = new File(workingDir, unfoldingFileName);
+			File unfoldingFile = new File(workingDirectory, unfoldingFileName);
 			if(unfoldingFile.exists()) {
 				outputFiles.put(unfoldingFileName, FileUtils.readAllBytes(unfoldingFile));
 			}
-			File g = new File(workingDir, "mpsat.g");
+			File g = new File(workingDirectory, "mpsat.g");
 			if(g.exists()) {
 				outputFiles.put("mpsat.g", FileUtils.readAllBytes(g));
 			}
@@ -69,10 +75,11 @@
 		
 		ExternalProcessResult retVal = res.getReturnValue();
 		ExternalProcessResult result = new ExternalProcessResult(retVal.getReturnCode(), retVal.getOutput(), retVal.getErrors(), outputFiles);
-		
-		if (retVal.getReturnCode() < 2)
+		if (retVal.getReturnCode() < 2) {
 			return Result.finished(result);
-		else
+		} else {
 			return Result.failed(result);
+		}
 	}
-}
 \ No newline at end of file
+	
+}
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/AbstractMpsatChecker.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/AbstractMpsatChecker.java	2014-06-20 21:35:25 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/AbstractMpsatChecker.java	2014-11-30 23:14:46 +0000
@@ -22,15 +22,19 @@
 	
 	@Override
 	public final void run(WorkspaceEntry we) {
+		final MpsatSettings settings = getSettings();
+		final MpsatChainTask mpsatTask = new MpsatChainTask(we, settings, framework);
+	
 		String description = "MPSat tool chain";
 		String title = we.getModelEntry().getModel().getTitle();
 		if (!title.isEmpty()) {
 			description += "(" + title +")";
 		}
-		final MpsatChainTask mpsatTask = new MpsatChainTask(we, getSettings(), framework);
-		framework.getTaskManager().queue(mpsatTask, description, new MpsatChainResultHandler(mpsatTask));
+		MpsatChainResultHandler monitor = new MpsatChainResultHandler(mpsatTask);
+	
+		framework.getTaskManager().queue(mpsatTask, description, monitor);
 	}
-
+	
 	@Override
 	public abstract String getDisplayName();
 
 
=== added file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatConformationChecker.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatConformationChecker.java	1970-01-01 00:00:00 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatConformationChecker.java	2014-11-30 23:14:46 +0000
@@ -0,0 +1,56 @@
+package org.workcraft.plugins.mpsat.tools;
+
+import java.io.File;
+
+import javax.swing.JFileChooser;
+
+import org.workcraft.Framework;
+import org.workcraft.Tool;
+import org.workcraft.plugins.mpsat.MpsatChainResultHandler;
+import org.workcraft.plugins.mpsat.tasks.MpsatConformationTask;
+import org.workcraft.plugins.stg.STGModel;
+import org.workcraft.util.WorkspaceUtils;
+import org.workcraft.workspace.WorkspaceEntry;
+
+public class MpsatConformationChecker implements Tool {
+	private final Framework framework;
+	
+	public MpsatConformationChecker(Framework framework) {
+		this.framework = framework;
+	}
+
+	@Override
+	public String getSection() {
+		return "Verification";
+	}
+
+	@Override
+	public String getDisplayName() {
+		return "Check for conformation (without dummies) [MPSat]...";
+	}
+
+	@Override
+	public boolean isApplicableTo(WorkspaceEntry we) {
+		return WorkspaceUtils.canHas(we, STGModel.class);
+	}
+	
+	@Override
+	public final void run(WorkspaceEntry we) {
+		JFileChooser fc = framework.getMainWindow().createOpenDialog("Open environment file", false, null);
+		if (fc.showDialog(null, "Open") == JFileChooser.APPROVE_OPTION) {
+			File file = fc.getSelectedFile();
+			if (framework.checkFile(file)) {
+				final MpsatConformationTask mpsatTask = new MpsatConformationTask(we, framework, file);
+
+				String description = "MPSat tool chain";
+				String title = we.getModelEntry().getModel().getTitle();
+				if (!title.isEmpty()) {
+					description += "(" + title +")";
+				}
+				MpsatChainResultHandler monitor = new MpsatChainResultHandler(mpsatTask);
+
+				framework.getTaskManager().queue(mpsatTask, description, monitor);
+			}
+		}
+	}
+}
 
=== renamed file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/CustomPropertyMpsatChecker.java' => 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatCustomPropertyChecker.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/CustomPropertyMpsatChecker.java	2014-04-16 21:55:15 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tools/MpsatCustomPropertyChecker.java	2014-11-30 23:14:46 +0000
@@ -15,9 +15,9 @@
 import org.workcraft.util.WorkspaceUtils;
 import org.workcraft.workspace.WorkspaceEntry;
 
-public class CustomPropertyMpsatChecker implements Tool {
+public class MpsatCustomPropertyChecker implements Tool {
 
-	public CustomPropertyMpsatChecker(Framework framework) {
+	public MpsatCustomPropertyChecker(Framework framework) {
 		this.framework = framework;
 	}
 	
 
=== removed file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/PCompOutputMode.java'
--- MpsatPlugin/src/org/workcraft/plugins/pcomp/PCompOutputMode.java	2010-10-06 15:51:01 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/pcomp/PCompOutputMode.java	1970-01-01 00:00:00 +0000
@@ -1,7 +0,0 @@
-package org.workcraft.plugins.pcomp;
-
-public enum PCompOutputMode {
-	DUMMY, 
-	INTERNAL, 
-	OUTPUT
-}
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java'
--- MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java	2014-09-05 15:06:01 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/pcomp/gui/PcompDialog.java	2014-11-30 23:14:46 +0000
@@ -22,7 +22,7 @@
 import org.workcraft.gui.trees.TreeWindow;
 import org.workcraft.gui.workspace.Path;
 import org.workcraft.gui.workspace.WorkspaceChooser;
-import org.workcraft.plugins.pcomp.PCompOutputMode;
+import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode;
 import org.workcraft.plugins.stg.STGWorkspaceFilter;
 
 @SuppressWarnings("serial")
@@ -62,14 +62,13 @@
 		return improvedPcomp.isSelected();
 	}
 	
-	public PCompOutputMode getMode()
-	{
+	public ConversionMode getMode() {
 		if (leaveOutputs.isSelected())
-			return PCompOutputMode.OUTPUT;
+			return ConversionMode.OUTPUT;
 		if (internalize.isSelected())
-			return PCompOutputMode.INTERNAL;
+			return ConversionMode.INTERNAL;
 		if (dummify.isSelected())
-			return PCompOutputMode.DUMMY;
+			return ConversionMode.DUMMY;
 		throw new NotSupportedException("No button is selected. Cannot proceed.");
 	}
 	
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java	2014-09-05 15:06:01 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java	2014-11-30 23:14:46 +0000
@@ -3,28 +3,38 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.Map;
 
-import org.workcraft.plugins.pcomp.PCompOutputMode;
 import org.workcraft.plugins.pcomp.PcompUtilitySettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.plugins.shared.tasks.ExternalProcessTask;
 import org.workcraft.tasks.ProgressMonitor;
 import org.workcraft.tasks.Result;
+import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.tasks.Task;
-import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.util.FileUtils;
 
 public class PcompTask implements Task<ExternalProcessResult> {
-	private File[] inputs;
-	private final PCompOutputMode mode;
-	private final boolean sharedOutputs;
-	private final boolean improved;
-	
-	public PcompTask(File[] inputs, PCompOutputMode mode, boolean sharedOutputs, boolean improved) {
-		this.inputs = inputs;
-		this.mode = mode;
-		this.sharedOutputs = sharedOutputs;
-		this.improved = improved;
+	
+	public enum ConversionMode {
+		DUMMY, 
+		INTERNAL, 
+		OUTPUT
+	}
+
+	private final File[] inputFiles;
+	private final ConversionMode conversionMode;
+	private final boolean useSharedOutputs;
+	private final boolean useImprovedComposition;
+	private final File workingDirectory;
+	
+	public PcompTask(File[] inputFiles, ConversionMode conversionMode, boolean useSharedOutputs, boolean useImprovedComposition, File workingDirectory) {
+		this.inputFiles = inputFiles;
+		this.conversionMode = conversionMode;
+		this.useSharedOutputs = useSharedOutputs;
+		this.useImprovedComposition = useImprovedComposition;
+		this.workingDirectory = workingDirectory;
 	}
 	
 	@Override
@@ -38,60 +48,58 @@
 			}
 		}
 		
-		if (mode == PCompOutputMode.DUMMY) {
+		if (conversionMode == ConversionMode.DUMMY) {
 			command.add("-d");
 			command.add("-r");
-		}
-
-		if (mode == PCompOutputMode.INTERNAL) {
+		} else if (conversionMode == ConversionMode.INTERNAL) {
 			command.add("-i");
 		}
 		
-		if (sharedOutputs) {
+		if (useSharedOutputs) {
 			command.add("-o");
 		}
 
-		if (improved) {
+		if (useImprovedComposition) {
 			command.add("-p");
 		}
 		
-		File listFile;
-		
+		File listFile = null;
 		try {
-			listFile = File.createTempFile("pcomp_", ".list");
+			if (workingDirectory == null) {
+				listFile = File.createTempFile("places_", ".list");
+			} else {
+				listFile = new File(workingDirectory, "places.list");
+			}
 		} catch (IOException e) {
 			return Result.exception(e);
 		}
+		command.add("-l" + listFile.getAbsolutePath());
+
+		for (File inputFile: inputFiles) {
+			command.add(inputFile.getAbsolutePath());
+		}
 		
-		try
-		{
-			StringBuilder fileList = new StringBuilder();
-			for (File f : inputs)
-			{
-				fileList.append(f.getAbsolutePath());
-				fileList.append('\n');
-			}
-				
-			try {
-				FileUtils.writeAllText(listFile, fileList.toString());
-			} catch (IOException e) {
-				return Result.exception(e);
-			}
-
-			command.add("@"+listFile.getAbsolutePath());
-			
-			Result<? extends ExternalProcessResult> res = new ExternalProcessTask(command, new File(".")).run(monitor);
-			if (res.getOutcome() != Outcome.FINISHED)
-				return res;
-			
-			ExternalProcessResult retVal = res.getReturnValue();
-			if (retVal.getReturnCode() < 2)
-				return Result.finished(retVal);
-			else
-				return Result.failed(retVal);
-		}
-		finally {
-			listFile.delete();
-		}
+		Result<? extends ExternalProcessResult> res = new ExternalProcessTask(command, new File(".")).run(monitor);
+		if (res.getOutcome() != Outcome.FINISHED) {
+			return res;
+		}
+			
+		Map<String, byte[]> outputFiles = new HashMap<String, byte[]>();
+		try {
+			if(listFile.exists()) {
+				outputFiles.put("places.list", FileUtils.readAllBytes(listFile));
+			}
+		} catch (IOException e) {
+			return new Result<ExternalProcessResult>(e);
+		}
+
+		ExternalProcessResult retVal = res.getReturnValue();
+		ExternalProcessResult result = new ExternalProcessResult(retVal.getReturnCode(), retVal.getOutput(), retVal.getErrors(), outputFiles);
+		if (retVal.getReturnCode() < 2) {
+			return Result.finished(result);
+		} else {
+			return Result.failed(result);
+		}
+
 	}
 }
 \ No newline at end of file
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java'
--- MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java	2014-09-05 15:06:01 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java	2014-11-30 23:14:46 +0000
@@ -46,7 +46,7 @@
 			}
 			
 			PcompTask pcompTask = new PcompTask(inputs.toArray(new File[0]), dialog.getMode(), 
-					dialog.isSharedOutputsChecked(), dialog.isImprovedPcompChecked());
+					dialog.isSharedOutputsChecked(), dialog.isImprovedPcompChecked(), null);
 			
 			PcompResultHandler pcompResult = new PcompResultHandler(framework, dialog.showInEditor());
 			
 
=== modified file 'STGPlugin/src/org/workcraft/plugins/stg/STG.java'
--- STGPlugin/src/org/workcraft/plugins/stg/STG.java	2014-11-03 18:11:53 +0000
+++ STGPlugin/src/org/workcraft/plugins/stg/STG.java	2014-11-30 23:14:46 +0000
@@ -213,6 +213,16 @@
 					}
 				});
 	}
+	
+	public Set<String> getSignalFlatNames(Type type) {
+		Set<String> result = new HashSet<String>();
+		for (SignalTransition st : getSignalTransitions(type)) {
+			String ref = getSignalReference(st);
+			String flatName = NamespaceHelper.hierarchicalToFlatName(ref);
+			result.add(flatName);
+		}
+		return result;
+	}
 
 	@Override
 	public Set<String> getSignalReferences(Type type) {
@@ -359,8 +369,8 @@
 					throw new RuntimeException("An implicit place cannot have more that one transition in its preset or postset.");
 				}
 				
-				return "<" + NamespaceHelper.getFlatName(referenceManager.getNodeReference(null, preset.iterator().next())) 
-						+ "," + NamespaceHelper.getFlatName(referenceManager.getNodeReference(null, postset.iterator().next())) + ">";
+				return "<" + NamespaceHelper.hierarchicalToFlatName(referenceManager.getNodeReference(null, preset.iterator().next())) 
+						+ "," + NamespaceHelper.hierarchicalToFlatName(referenceManager.getNodeReference(null, postset.iterator().next())) + ">";
 			}
 		}
 		return super.getNodeReference(provider, node);
@@ -369,27 +379,27 @@
 	@Override
 	public Node getNodeByReference(NamespaceProvider provider, String reference) {
 		Pair<String, String> implicitPlaceTransitions = LabelParser.parseImplicitPlaceReference(reference);
-		
 		if (implicitPlaceTransitions != null) {
 			Node t1 = referenceManager.getNodeByReference(provider, 
 					NamespaceHelper.flatToHierarchicalName(implicitPlaceTransitions.getFirst())	);
+			
 			Node t2 = referenceManager.getNodeByReference(provider, 
 					NamespaceHelper.flatToHierarchicalName(implicitPlaceTransitions.getSecond()) );
-
-			Set<Node> implicitPlaceCandidates = SetUtils.intersection(getPreset(t2), getPostset(t1));
-
-			for (Node node : implicitPlaceCandidates) {
-				if ((node instanceof STGPlace) && ((STGPlace)node).isImplicit()) {
-					return node;
+			if ((t1 != null) && (t2 != null)) {
+				Set<Node> implicitPlaceCandidates = SetUtils.intersection(getPreset(t2), getPostset(t1));
+
+				for (Node node : implicitPlaceCandidates) {
+					if ((node instanceof STGPlace) && ((STGPlace)node).isImplicit()) {
+						return node;
+					}
 				}
 			}
-
 			throw new NotFoundException("Implicit place between "
 					+ implicitPlaceTransitions.getFirst() + " and "
 					+ implicitPlaceTransitions.getSecond() + " does not exist.");
-		} else
-		
+		} else {
 			return super.getNodeByReference(provider, reference); 			
+		}
 	}
 
 	public void makeExplicit(STGPlace implicitPlace) {
 
=== modified file 'STGPlugin/src/org/workcraft/plugins/stg/serialisation/DotGSerialiser.java'
--- STGPlugin/src/org/workcraft/plugins/stg/serialisation/DotGSerialiser.java	2014-07-28 13:32:42 +0000
+++ STGPlugin/src/org/workcraft/plugins/stg/serialisation/DotGSerialiser.java	2014-11-30 23:14:46 +0000
@@ -66,7 +66,7 @@
 		
 		for (String s : sortedNames) {
 			out.print(" ");
-			out.print(NamespaceHelper.getFlatName(s));
+			out.print(NamespaceHelper.hierarchicalToFlatName(s));
 		}
 		
 		out.print("\n");
@@ -90,7 +90,7 @@
 				return;
 		
 		if (model.getPostset(node).size()>0) {
-			out.write(NamespaceHelper.getFlatName(model.getNodeReference(node)));
+			out.write(NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(node)));
 
 			for (Node n : sortNodes (model.getPostset(node), model)  ) {
 				if (n instanceof STGPlace) {
@@ -98,11 +98,11 @@
 						Collection<Node> postset = model.getPostset(n);
 						if (postset.size() > 1)
 							throw new FormatException("Implicit place cannot have more than one node in postset");
-						out.write(" " + NamespaceHelper.getFlatName(model.getNodeReference(postset.iterator().next())));						
+						out.write(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(postset.iterator().next())));						
 					} else
-						out.write(" " + NamespaceHelper.getFlatName(model.getNodeReference(n)));	
+						out.write(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(n)));	
 				} else {
-					out.write(" " + NamespaceHelper.getFlatName(model.getNodeReference(n)));
+					out.write(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(n)));
 				}
 			}
 			
@@ -165,12 +165,12 @@
 			
 			if (p instanceof STGPlace) {
 				if ( ((STGPlace)p).isImplicit() ) {
-					reference = "<" + NamespaceHelper.getFlatName(model.getNodeReference(model.getPreset(p).iterator().next())) + "," +
-							NamespaceHelper.getFlatName(model.getNodeReference(model.getPostset(p).iterator().next())) + ">";
+					reference = "<" + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(model.getPreset(p).iterator().next())) + "," +
+							NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(model.getPostset(p).iterator().next())) + ">";
 				} else
-					reference = NamespaceHelper.getFlatName(model.getNodeReference(p));
+					reference = NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(p));
 			} else {
-				reference = NamespaceHelper.getFlatName(model.getNodeReference(p));
+				reference = NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(p));
 			}
 			
 			if (tokens == 1)
@@ -201,7 +201,7 @@
 		for (Place p : places) {
 			if (p instanceof STGPlace)
 				if (((STGPlace)p).getCapacity() != 1)
-				capacity.append(" " + NamespaceHelper.getFlatName(model.getNodeReference(p)) + "=" + ((STGPlace)p).getCapacity());
+				capacity.append(" " + NamespaceHelper.hierarchicalToFlatName(model.getNodeReference(p)) + "=" + ((STGPlace)p).getCapacity());
 		}
 		
 		if (capacity.length() > 0)
@@ -212,7 +212,7 @@
 		LinkedList<String> transitions = new LinkedList<String>(); 
 		
 		for (Transition t : net.getTransitions())
-			transitions.add(NamespaceHelper.getFlatName(net.getNodeReference(t)));
+			transitions.add(NamespaceHelper.hierarchicalToFlatName(net.getNodeReference(t)));
 		
 		writeSignalsHeader(out, transitions, ".dummy");
 		
 
=== modified file 'Tests/src/org/workcraft/testing/dom/hierarchy/HierarchicalUniqueNameReferenceManagerTest.java'
--- Tests/src/org/workcraft/testing/dom/hierarchy/HierarchicalUniqueNameReferenceManagerTest.java	2014-07-11 09:35:42 +0000
+++ Tests/src/org/workcraft/testing/dom/hierarchy/HierarchicalUniqueNameReferenceManagerTest.java	2014-11-30 23:14:46 +0000
@@ -68,7 +68,7 @@
 			String hName = en.getKey();
 			String fName = en.getValue();
 			
-			String answer = NamespaceHelper.getFlatName(hName); 
+			String answer = NamespaceHelper.hierarchicalToFlatName(hName); 
 			assertTrue(answer.equals(fName));
 			
 			hName = hName.replaceAll("'", "");
 
=== modified file 'WorkcraftCore/src/org/workcraft/Info.java'
--- WorkcraftCore/src/org/workcraft/Info.java	2014-11-24 15:37:13 +0000
+++ WorkcraftCore/src/org/workcraft/Info.java	2014-11-30 23:14:46 +0000
@@ -13,7 +13,7 @@
 	private static final int majorVersion = 3;
 	private static final int minorVersion = 0;
 	private static final int revisionVersion = 3;
-	private static final String statusVersion = "alpha";
+	private static final String statusVersion = "beta";
 
 	private static final int startYear = 2006;
 	private static final int currentYear = Calendar.getInstance().get(Calendar.YEAR);
 
=== modified file 'WorkcraftCore/src/org/workcraft/dom/hierarchy/NamespaceHelper.java'
--- WorkcraftCore/src/org/workcraft/dom/hierarchy/NamespaceHelper.java	2014-11-12 18:06:50 +0000
+++ WorkcraftCore/src/org/workcraft/dom/hierarchy/NamespaceHelper.java	2014-11-30 23:14:46 +0000
@@ -23,20 +23,20 @@
 	// TODO: make it work with the embedded ' characters
 	private static Pattern hPattern = Pattern.compile("(/)?(((\\'([^\\']+)\\')|([_A-Za-z][_A-Za-z0-9]*))([\\+\\-\\~])?(/[0-9]+)?)(.*)");
 	
-	public static String getFlatName(String reference) {
-		return getFlatName(reference, flatNameSeparator, true);
+	public static String hierarchicalToFlatName(String reference) {
+		return hierarchicalToFlatName(reference, flatNameSeparator, true);
 	}
 	
-	private static String getFlatName(String reference, String flatSeparator, boolean isFirst) {
+	private static String hierarchicalToFlatName(String reference, String flatSeparator, boolean suppressLeadingSeparator) {
 		if (flatSeparator==null) flatSeparator=flatNameSeparator;
 		
-		// do not work with implicit places(?)
+		// Do not work with implicit places(?)
 		if (reference.startsWith("<")) { 
 			return reference;
 		}
 		String ret = "";
-		// in this version the first separator is not shown
-		if (!isFirst && reference.startsWith(hierarchySeparator)) {
+		// In this version the first separator is suppressed
+		if (!suppressLeadingSeparator && reference.startsWith(hierarchySeparator)) {
 			ret=flatSeparator;
 		}
 		
@@ -45,11 +45,11 @@
 		if (tail.equals("")) { 
 			return ret+head;
 		}
-		return ret+head+getFlatName(tail, flatSeparator, false);
+		return ret + head + hierarchicalToFlatName(tail, flatSeparator, false);
 	}
 	
-	public static String flatToHierarchicalName(String reference) {
-		return flatToHierarchicalName(reference, flatNameSeparator);
+	public static String flatToHierarchicalName(String flatName) {
+		return flatToHierarchicalName(flatName, flatNameSeparator);
 	}
 	
 	private static String flatToHierarchicalName(String reference, String flatSeparator) {
 
=== modified file 'WorkcraftCore/src/org/workcraft/gui/MainWindow.java'
--- WorkcraftCore/src/org/workcraft/gui/MainWindow.java	2014-11-24 17:04:15 +0000
+++ WorkcraftCore/src/org/workcraft/gui/MainWindow.java	2014-11-30 23:14:46 +0000
@@ -833,7 +833,7 @@
 		}
 	}
 
-	private JFileChooser createOpenDialog(String title, boolean multiSelection, Importer[] importers) {
+	public JFileChooser createOpenDialog(String title, boolean multiSelection, Importer[] importers) {
 		JFileChooser fc = new JFileChooser();
 		fc.setDialogType(JFileChooser.OPEN_DIALOG);
 		fc.setMultiSelectionEnabled(multiSelection);
@@ -856,7 +856,7 @@
 		return fc;
 	}
 	
-	private JFileChooser createSaveDialog(String title, File file, Exporter exporter) {
+	public JFileChooser createSaveDialog(String title, File file, Exporter exporter) {
 		JFileChooser fc = new JFileChooser();
 		fc.setDialogType(JFileChooser.SAVE_DIALOG);
 		fc.setDialogTitle(title);
 
=== modified file 'WorkcraftCore/src/org/workcraft/util/FileUtils.java'
--- WorkcraftCore/src/org/workcraft/util/FileUtils.java	2014-01-15 17:13:30 +0000
+++ WorkcraftCore/src/org/workcraft/util/FileUtils.java	2014-11-30 23:14:46 +0000
@@ -31,8 +31,6 @@
 import java.io.InputStream;
 import java.io.InputStreamReader;
 import java.io.OutputStream;
-import java.net.URI;
-import java.net.URISyntaxException;
 import java.nio.channels.Channels;
 import java.nio.channels.FileChannel;
 import java.nio.channels.WritableByteChannel;
 
=== modified file 'build_distr_linux.sh'
--- build_distr_linux.sh	2014-11-24 15:37:13 +0000
+++ build_distr_linux.sh	2014-11-30 23:14:46 +0000
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 
 src_dir="."
-distr_dir="../../workcraft_3.0.3_alpha"
+distr_dir="../../workcraft_3.0.3_beta"
 template_dir="../../distr-template-linux"
 
 ./build_distr.sh -s $src_dir -d $distr_dir -t $template_dir
 
=== modified file 'build_distr_windows.sh'
--- build_distr_windows.sh	2014-11-24 15:37:13 +0000
+++ build_distr_windows.sh	2014-11-30 23:14:46 +0000
@@ -1,7 +1,7 @@
 #!/usr/bin/env bash
 
 src_dir="."
-distr_dir="../../workcraft_3.0.3_alpha"
+distr_dir="../../workcraft_3.0.3_beta"
 template_dir="../../distr-template-windows"
 
 ./build_distr.sh -s $src_dir -d $distr_dir -t $template_dir