Merge lp:~danilovesky/workcraft/trunk-circuit-env-stg into lp:workcraft

[Danil Sokolov]

[Danil Sokolov (danilovesky)]

review: Approve

=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitModule.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitModule.java	2013-09-17 14:58:15 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/CircuitModule.java	2014-04-29 16:24:51 +0000
@@ -9,8 +9,6 @@
 import org.workcraft.gui.propertyeditor.SettingsPage;
 import org.workcraft.plugins.circuit.serialisation.FunctionDeserialiser;
 import org.workcraft.plugins.circuit.serialisation.FunctionSerialiser;
-import org.workcraft.plugins.circuit.tools.CheckCircuitDeadlockTool;
-import org.workcraft.plugins.circuit.tools.CheckCircuitHazardTool;
 import org.workcraft.plugins.circuit.tools.CheckCircuitTool;
 import org.workcraft.plugins.circuit.tools.STGGeneratorTool;
 import org.workcraft.serialisation.xml.XMLDeserialiser;
@@ -34,20 +32,6 @@
 				return new STGGeneratorTool(framework);
 			}
 		});
-	
-		pm.registerClass(Tool.class, new Initialiser<Tool>() {
-			@Override
-			public Tool create() {
-				return new CheckCircuitDeadlockTool(framework);
-			}
-		});
-
-		pm.registerClass(Tool.class, new Initialiser<Tool>() {
-			@Override
-			public Tool create() {
-				return new CheckCircuitHazardTool(framework);
-			}
-		});
 
 		pm.registerClass(Tool.class, new Initialiser<Tool>() {
 			@Override
@@ -56,6 +40,66 @@
 			}
 		});
 
+		pm.registerClass(Tool.class, new Initialiser<Tool>() {
+			@Override
+			public Tool create() {
+				return new CheckCircuitTool(framework) {
+					@Override
+					public String getDisplayName() {
+						return "Check circuit only for conformation";
+					}
+					@Override
+					public boolean checkDeadlock() {
+						return false;
+					}
+					@Override
+					public boolean checkHazard() {
+						return false;
+					}
+				};
+			}
+		});
+
+		pm.registerClass(Tool.class, new Initialiser<Tool>() {
+			@Override
+			public Tool create() {
+				return new CheckCircuitTool(framework) {
+					@Override
+					public String getDisplayName() {
+						return "Check circuit only for deadlocks";
+					}
+					@Override
+					public boolean checkConformation() {
+						return false;
+					}
+					@Override
+					public boolean checkHazard() {
+						return false;
+					}
+				};
+			}
+		});
+
+		pm.registerClass(Tool.class, new Initialiser<Tool>() {
+			@Override
+			public Tool create() {
+				return new CheckCircuitTool(framework) {
+					@Override
+					public String getDisplayName() {
+						return "Check circuit only for hazards";
+					}
+					@Override
+					public boolean checkConformation() {
+						return false;
+					}
+					@Override
+					public boolean checkDeadlock() {
+						return false;
+					}
+				};
+			}
+		});
+
 		pm.registerClass(ModelDescriptor.class, CircuitModelDescriptor.class);
 		pm.registerClass(XMLSerialiser.class, FunctionSerialiser.class);
 		pm.registerClass(XMLDeserialiser.class, FunctionDeserialiser.class);
 
=== added file 'CircuitPlugin/src/org/workcraft/plugins/circuit/Environment.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/Environment.java	1970-01-01 00:00:00 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/Environment.java	2014-04-29 16:24:51 +0000
@@ -0,0 +1,21 @@
+package org.workcraft.plugins.circuit;
+
+import java.io.File;
+
+import org.workcraft.dom.math.MathNode;
+
+public class Environment extends MathNode {
+	private File file;
+	
+	public Environment() {
+		
+	}
+	
+	public File getFile() {
+		return file;
+	}
+	
+	public void setFile(File file) {
+		this.file = file;
+	}
+}
 
=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/VisualCircuit.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/VisualCircuit.java	2014-04-09 22:33:19 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/VisualCircuit.java	2014-04-29 16:24:51 +0000
@@ -37,6 +37,7 @@
 import org.workcraft.exceptions.VisualModelInstantiationException;
 import org.workcraft.gui.propertyeditor.Properties;
 import org.workcraft.plugins.circuit.Contact.IOType;
+import org.workcraft.serialisation.xml.NoAutoSerialisation;
 import org.workcraft.util.Hierarchy;
 
 
@@ -45,10 +46,9 @@
 public class VisualCircuit extends AbstractVisualModel {
 
 	private Circuit circuit;
-	private File environmentFile;
 	
 	@Override
-	public void validateConnection(Node first, Node second)	throws InvalidConnectionException {
+	public void validateConnection(Node first, Node second) throws InvalidConnectionException {
 		if (first==second) {
 			throw new InvalidConnectionException ("Connections are only valid between different objects");
 		}
@@ -77,24 +77,12 @@
 		}
 	}
 	
-/*	
-	private final class StateSupervisorExtension extends StateSupervisor {
-		@Override
-		public void handleEvent(StateEvent e) {
-//			if(e instanceof PropertyChangedEvent)
-				
-		}
-	}
-*/
-
-	public VisualCircuit(Circuit model, VisualGroup root)
-	{
+	public VisualCircuit(Circuit model, VisualGroup root) {
 		super(model, root);
 		circuit=model;
 	}
 
-	public VisualCircuit(Circuit model)
-	throws VisualModelInstantiationException {
+	public VisualCircuit(Circuit model) throws VisualModelInstantiationException {
 		super(model);
 		circuit=model;
 		try {
@@ -102,13 +90,10 @@
 		} catch (NodeCreationException e) {
 			throw new VisualModelInstantiationException(e);
 		}
-		
-		//new StateSupervisorExtension().attach(getRoot());
 	}
 
 	@Override
-	public void connect(Node first, Node second)
-			throws InvalidConnectionException {
+	public void connect(Node first, Node second) throws InvalidConnectionException {
 		validateConnection(first, second);
 		
 		if (first instanceof VisualComponent && second instanceof VisualComponent) {
@@ -121,6 +106,56 @@
 			nearestAncestor.add(connection);
 		}
 	}
+
+	public VisualFunctionContact  getOrCreateOutput(String name, double x, double y) {
+		for(VisualFunctionContact c : Hierarchy.filterNodesByType(
+				getRoot().getChildren(), VisualFunctionContact.class)) {
+			if(c.getName().equals(name)) return c;
+		}
+		VisualFunctionContact vc = new VisualFunctionContact(new FunctionContact(IOType.OUTPUT));
+        vc.setPosition(new Point2D.Double(x, y));
+        addFunctionContact(vc);
+        vc.setName(name);
+		return vc;
+	}
+	
+	public void addFunctionComponent(VisualFunctionComponent component) {
+		for (Node node : component.getMathReferences()) {
+			circuit.add(node);
+		}
+		super.add(component);
+	}
+	 
+	 public void addJoint(VisualJoint joint) {
+		 for (Node node : joint.getMathReferences()) {
+			 circuit.add(node);
+		 }
+		 super.add(joint);
+	 }
+	 
+	 public void addFunctionContact(VisualFunctionContact contact) {
+		 circuit.add(contact.getFunction());
+		 super.add(contact);
+	 }
+
+	 @NoAutoSerialisation
+	public File getEnvironmentFile() {
+		File result = null;
+		for (Environment env: Hierarchy.filterNodesByType(getRoot().getChildren(), Environment.class)) {
+			result = env.getFile();
+		}
+		return result;
+	}
+
+	@NoAutoSerialisation
+	public void setEnvironmentFile(File value) {
+		for (Environment env: Hierarchy.filterNodesByType(getRoot().getChildren(), Environment.class)) {
+			remove(env);
+		}
+		Environment env = new Environment();
+		env.setFile(value);
+		add(env);
+	}
 	
 	@Override
 	public Properties getProperties(Node node) {
@@ -138,31 +173,4 @@
 		return properties;
 	}
 
-	public VisualFunctionContact  getOrCreateOutput(String name, double x, double y) {
-		
-		for(VisualFunctionContact c : Hierarchy.filterNodesByType(getRoot().getChildren(), VisualFunctionContact.class)) {
-			if(c.getName().equals(name)) return c;
-		}
-		
-		FunctionContact fc = new FunctionContact(IOType.OUTPUT);
-		VisualFunctionContact vc = new VisualFunctionContact(fc);
-		Point2D p2d = new Point2D.Double();
-		p2d.setLocation(x,y);
-		vc.setPosition(p2d);
-		circuit.add(fc);
-		this.add(vc);
-		
-		vc.setName(name);
-		
-		return vc;
-	}
-
-	public File getEnvironmentFile() {
-		return environmentFile;
-	}
-
-	public void setEnvironmentFile(File value) {
-		this.environmentFile = value;
-	}
-
 }
 
=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/VisualContact.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/VisualContact.java	2014-01-15 14:11:43 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/VisualContact.java	2014-04-29 16:24:51 +0000
@@ -375,7 +375,8 @@
 	public static boolean isDriver(Node contact) {
 		if (!(contact instanceof VisualContact)) return false;
 		
-		return (((VisualContact)contact).getIOType() == IOType.OUTPUT) == (((VisualContact)contact).getParent() instanceof VisualComponent);
+		return (((VisualContact)contact).getIOType() == IOType.OUTPUT) 
+				== (((VisualContact)contact).getParent() instanceof VisualComponent);
 	}
 
 
 
=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/VisualFunctionContact.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/VisualFunctionContact.java	2014-04-09 17:11:48 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/VisualFunctionContact.java	2014-04-29 16:24:51 +0000
@@ -89,16 +89,18 @@
 	}
 	
 	FormulaRenderingResult getRenderedSetFormula(FontRenderContext fcon) {
-		if (renderedSetFormula == null) {
+		if (((FunctionContact)getReferencedContact()).getSetFunction() == null) {
+			return null;
+		} else if (renderedSetFormula == null) {
 			renderedSetFormula = FormulaToGraphics.render(((FunctionContact)getReferencedContact()).getSetFunction(), fcon, font);
 		}
 		return renderedSetFormula;
 	}
 	
 	FormulaRenderingResult getRenderedResetFormula(FontRenderContext fcon) {
-		if (((FunctionContact)getReferencedContact()).getResetFunction()==null) return null;
-		
-		if (renderedResetFormula == null) {
+		if (((FunctionContact)getReferencedContact()).getResetFunction() == null) {
+			return null;
+		} else if (renderedResetFormula == null) {
 			renderedResetFormula = FormulaToGraphics.render(((FunctionContact)getReferencedContact()).getResetFunction(), fcon, font);
 		}
 		return renderedResetFormula;
@@ -154,6 +156,8 @@
 	
 	
 	private void drawFormula(Graphics2D g, int arrowType, float xOffset, float yOffset, Color foreground, Color background, FormulaRenderingResult result) {
+		if (result == null) return;
+		
 		Rectangle2D textBB = result.boundingBox;
 		float textX = 0;
 		float textY = (float)-textBB.getCenterY()-(float)0.5-yOffset;
 
=== removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitDeadlockTask.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitDeadlockTask.java	2014-04-16 21:55:15 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitDeadlockTask.java	1970-01-01 00:00:00 +0000
@@ -1,111 +0,0 @@
-package org.workcraft.plugins.circuit.tasks;
-
-import java.io.File;
-
-import org.workcraft.Framework;
-import org.workcraft.interop.Exporter;
-import org.workcraft.plugins.circuit.VisualCircuit;
-import org.workcraft.plugins.circuit.tools.STGGenerator;
-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.mpsat.tasks.MpsatChainResult;
-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.shared.tasks.ExternalProcessResult;
-import org.workcraft.plugins.stg.STGModel;
-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.workspace.WorkspaceEntry;
-
-
-public class CheckCircuitDeadlockTask extends MpsatChainTask {
-	private final MpsatSettings settings;
-	private final WorkspaceEntry we;
-	private final Framework framework;
-	
-	public CheckCircuitDeadlockTask(WorkspaceEntry we, Framework framework) {
-		super (we, null, framework);
-		this.we = we;
-		this.framework = framework;
-		this.settings = new MpsatSettings("Deadlock freedom", MpsatMode.DEADLOCK, 0, 
-				MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(), null);
-	}
-	
-	@Override
-	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
-		try {
-			monitor.progressUpdate(0.05);
-			VisualCircuit circuit = (VisualCircuit) we.getModelEntry().getVisualModel();
-			STGModel model = (STGModel) STGGenerator.generate(circuit).getMathModel();
-			monitor.progressUpdate(0.10);
-			
-			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());
-			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);
-				}
-				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, null, null, settings));
-			}
-			monitor.progressUpdate(0.20);
-			
-			File mciFile = File.createTempFile("unfolding", ".mci");
-			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
-			netFile.delete();
-			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				mciFile.delete();
-				if (punfResult.getOutcome() == Outcome.CANCELLED) {
-					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				}
-				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, null, settings));
-			}
-			monitor.progressUpdate(0.70);
-
-			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon);
-			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
-				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
-					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				}
-				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings ));
-			}
-			monitor.progressUpdate(0.90);
-			
-			MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue());
-			if (!mdp.getSolutions().isEmpty()) {
-				mciFile.delete();
-				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit has a deadlock"));
-			}
-			monitor.progressUpdate(1.0);
-
-			mciFile.delete();
-			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit is deadlock-free"));
-			
-		} catch (Throwable e) {
-			return new Result<MpsatChainResult>(e);
-		}
-	}
-
-}
 
=== removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitHazardTask.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitHazardTask.java	2014-04-16 21:55:15 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitHazardTask.java	1970-01-01 00:00:00 +0000
@@ -1,110 +0,0 @@
-package org.workcraft.plugins.circuit.tasks;
-
-import java.io.File;
-
-import org.workcraft.Framework;
-import org.workcraft.interop.Exporter;
-import org.workcraft.plugins.circuit.VisualCircuit;
-import org.workcraft.plugins.circuit.tools.STGGenerator;
-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.mpsat.tasks.MpsatChainResult;
-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.shared.tasks.ExternalProcessResult;
-import org.workcraft.plugins.stg.STGModel;
-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.workspace.WorkspaceEntry;
-
-
-public class CheckCircuitHazardTask extends MpsatChainTask {
-	private final MpsatSettings settings;
-	private final WorkspaceEntry we;
-	private final Framework framework;
-	
-	public CheckCircuitHazardTask(WorkspaceEntry we, Framework framework) {
-		super (we, null, framework);
-		this.we = we;
-		this.framework = framework;
-		this.settings = new MpsatSettings("Output persistence", MpsatMode.STG_REACHABILITY, 0, 
-				MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(),
-				MpsatSettings.reachSemimodularity);
-}
-	
-	@Override
-	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
-		try {
-			monitor.progressUpdate(0.05);
-			VisualCircuit circuit = (VisualCircuit) we.getModelEntry().getVisualModel();
-			STGModel model = (STGModel) STGGenerator.generate(circuit).getMathModel();
-			monitor.progressUpdate(0.10);
-			
-			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());
-			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);
-				}
-				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, null, settings));
-			}
-			monitor.progressUpdate(0.20);
-			
-			File mciFile = File.createTempFile("unfolding", ".mci");
-			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
-			netFile.delete();
-			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				mciFile.delete();
-				if (punfResult.getOutcome() == Outcome.CANCELLED) {
-					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				}
-				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, null, settings));
-			}
-			monitor.progressUpdate(0.70);
-
-			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running semimodularity checking [MPSat]", mon);
-			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
-				if (mpsatResult.getOutcome() == Outcome.CANCELLED)
-					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				
-				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings));
-			}
-			
-			MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue());
-			if (!mdp.getSolutions().isEmpty()) {
-				mciFile.delete();
-				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit has hazard(s)"));
-			}
-			monitor.progressUpdate(1.0);
-
-			mciFile.delete();
-			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Circuit is hazard-free"));
-			
-		} catch (Throwable e) {
-			return new Result<MpsatChainResult>(e);
-		}
-	}
-
-}
 
=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java	2014-04-16 21:55:15 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java	2014-04-29 16:24:51 +0000
@@ -14,8 +14,10 @@
 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.shared.tasks.ExternalProcessResult;
-import org.workcraft.plugins.stg.STGModel;
+import org.workcraft.plugins.stg.STG;
 import org.workcraft.serialisation.Format;
 import org.workcraft.tasks.ProgressMonitor;
 import org.workcraft.tasks.Result;
@@ -23,111 +25,254 @@
 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 CheckCircuitTask extends MpsatChainTask {
-	private final MpsatSettings deadlockSettings;
-	private final MpsatSettings hazardSettings;
+	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 MpsatSettings deadlockSettings = new MpsatSettings("Deadlock freedom",
+			MpsatMode.DEADLOCK, 0, MpsatUtilitySettings.getSolutionMode(), 
+			MpsatUtilitySettings.getSolutionCount(), null);
+	
+	private final MpsatSettings hazardSettings = new MpsatSettings("Output persistence", 
+			MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), 
+			MpsatUtilitySettings.getSolutionCount(), MpsatSettings.reachSemimodularity);
+
 	private final WorkspaceEntry we;
 	private final Framework framework;
+	private final boolean checkConformation;
+	private final boolean checkDeadlock;
+	private final boolean checkHazard;
 	
-	public CheckCircuitTask(WorkspaceEntry we, Framework framework) {
+	public CheckCircuitTask(WorkspaceEntry we, Framework framework,  
+			boolean checkConformation, boolean checkDeadlock, boolean checkHazard) {
 		super (we, null, framework);
 		this.we = we;
 		this.framework = framework;
-		
-		this.deadlockSettings = new MpsatSettings("Deadlock freedom", MpsatMode.DEADLOCK, 0, 
-				MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(), null);
-		
-		this.hazardSettings = new MpsatSettings("Output persistence", MpsatMode.STG_REACHABILITY, 0, 
-				MpsatUtilitySettings.getSolutionMode(), MpsatUtilitySettings.getSolutionCount(), 
-				MpsatSettings.reachSemimodularity);
+		this.checkConformation = checkConformation;
+		this.checkDeadlock = checkDeadlock;
+		this.checkHazard = checkHazard;
 	}
 	
 	@Override
 	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
 		try {
+			// Common variables
 			monitor.progressUpdate(0.05);
-			VisualCircuit circuit = (VisualCircuit) we.getModelEntry().getVisualModel();
-			STGModel model = (STGModel) STGGenerator.generate(circuit).getMathModel();
+			String title = we.getWorkspacePath().getNode();
+			if (title.endsWith(".work")) {
+				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.");
+			}
+			SubtaskMonitor<Object> subtaskMonitor = new SubtaskMonitor<Object>(monitor);
 			monitor.progressUpdate(0.10);
-			
-			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());
-			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) {
+
+			// Generating .g for the circuit
+			File circuitStgFile = File.createTempFile(title + "-circuit-", stgExporter.getExtenstion());
+			ExportTask circuitExportTask = new ExportTask(stgExporter, circuitStg, circuitStgFile.getCanonicalPath());
+			Result<? extends Object> circuitExportResult = framework.getTaskManager().execute(
+					circuitExportTask, "Exporting circuit .g", subtaskMonitor);
+			
+			if (circuitExportResult.getOutcome() != Outcome.FINISHED) {
+				circuitStgFile.delete();
+				if (circuitExportResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
-				return new Result<MpsatChainResult>(Outcome.FAILED,
-						new MpsatChainResult(exportResult, null, null, deadlockSettings));
+				return new Result<MpsatChainResult>(Outcome.FAILED, 
+						new MpsatChainResult(circuitExportResult, null, null, null, toolchainPreparationSettings));
 			}
 			monitor.progressUpdate(0.20);
 			
-			File mciFile = File.createTempFile("unfolding", ".mci");
-			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
-			netFile.delete();
+			// Generating .g for the environment
+			File stgFile;
+			STG stg;
+			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;
+			} else {
+				// Compose circuit with its environment
+				File environmentStgFile;
+				if (environmentFile.getName().endsWith(".g")) {
+					environmentStgFile = environmentFile;
+				} else {
+					STG environementStg = (STG)framework.loadFile(environmentFile).getMathModel();
+					environmentStgFile = File.createTempFile(title + "-environment-", stgExporter.getExtenstion());
+					ExportTask environmentExportTask = new ExportTask(stgExporter, environementStg, environmentStgFile.getCanonicalPath());
+					Result<? extends Object> environmentExportResult = framework.getTaskManager().execute(
+							environmentExportTask, "Exporting environment .g", subtaskMonitor);
+					
+					if (environmentExportResult.getOutcome() != Outcome.FINISHED) {
+						environmentStgFile.delete();
+						if (environmentExportResult.getOutcome() == Outcome.CANCELLED) {
+							return new Result<MpsatChainResult>(Outcome.CANCELLED);
+						}
+						return new Result<MpsatChainResult>(Outcome.FAILED, 
+								new MpsatChainResult(environmentExportResult, null, null, null, toolchainPreparationSettings));
+					}
+				}
+				monitor.progressUpdate(0.25);
+
+				// Generating .g for the whole system (circuit and environment)
+				stgFile = File.createTempFile(title + "-system-", stgExporter.getExtenstion());
+				PcompTask pcompTask = new PcompTask(new File[]{circuitStgFile, environmentStgFile}, PCompOutputMode.OUTPUT, false);
+				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));
+				}
+				FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput()));
+				WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true);
+				stg = (STG)stgWorkspaceEntry.getModelEntry().getMathModel();
+			}		
+			monitor.progressUpdate(0.30);
+
+			// Generate unfolding
+			File mciFile = File.createTempFile(title+"-unfolding-", ".mci");
+			PunfTask punfTask = new PunfTask(stgFile.getCanonicalPath(), mciFile.getCanonicalPath());
+			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
+					punfTask, "Unfolding .g", subtaskMonitor);
+			
+			stgFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
 				mciFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, null, deadlockSettings));
+						new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainPreparationSettings));
 			}
 			monitor.progressUpdate(0.40);
-
-			MpsatTask mpsatTask = new MpsatTask(deadlockSettings.getMpsatArguments(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon);
-			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
-				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
-					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				}
-				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings));
+			
+			// Check for interface conformation (only if the environment is specified) 
+			if (hasEnvironment && checkConformation) {
+				String reachConformation = MpsatSettings.genReachConformation(stg, circuitStg);
+				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(), mciFile.getCanonicalPath());
+				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(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings));
+				}
+				monitor.progressUpdate(0.50);
+
+				MpsatResultParser mpsatConformationParser = new MpsatResultParser(mpsatConformationResult.getReturnValue());
+				if (!mpsatConformationParser.getSolutions().isEmpty()) {
+					mciFile.delete();
+					return new Result<MpsatChainResult>(Outcome.FINISHED, 
+							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatConformationResult, conformationSettings, 
+									"Circuit does not conform to the environment after the following trace:"));
+				}
 			}
 			monitor.progressUpdate(0.60);
 			
-			MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue());
-			if (!mdp.getSolutions().isEmpty()) {
-				mciFile.delete();
-				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings, "Circuit has a deadlock"));
-			}
-			monitor.progressUpdate(0.70);
-			
-			mpsatTask = new MpsatTask(hazardSettings.getMpsatArguments(), mciFile.getCanonicalPath());
-			mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running semimodularity checking [MPSat]", mon);
-			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
-				if (mpsatResult.getOutcome() == Outcome.CANCELLED)
-					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				
-				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings));
-			}
-			monitor.progressUpdate(0.90);
-
-			mdp = new MpsatResultParser(mpsatResult.getReturnValue());
-			if (!mdp.getSolutions().isEmpty()) {
-				mciFile.delete();
-				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Circuit has hazard(s)"));
+			// Check for deadlock
+			if (checkDeadlock) {
+				MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(), mciFile.getCanonicalPath());
+				Result<? extends ExternalProcessResult> mpsatDeadlockResult = framework.getTaskManager().execute(
+						mpsatDeadlockTask, "Running deadlock check [MPSat]", subtaskMonitor);
+			
+				if (mpsatDeadlockResult.getOutcome() != Outcome.FINISHED) {
+					if (mpsatDeadlockResult.getOutcome() == Outcome.CANCELLED) {
+						return new Result<MpsatChainResult>(Outcome.CANCELLED);
+					}
+					return new Result<MpsatChainResult>(Outcome.FAILED, 
+							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings));
+				}
+				monitor.progressUpdate(0.70);
+			
+				MpsatResultParser mpsatDeadlockParser = new MpsatResultParser(mpsatDeadlockResult.getReturnValue());
+				if (!mpsatDeadlockParser.getSolutions().isEmpty()) {
+					mciFile.delete();
+					return new Result<MpsatChainResult>(Outcome.FINISHED, 
+							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatDeadlockResult, deadlockSettings, 
+									"Circuit has a deadlock after the following trace:"));
+				}
+			}
+			monitor.progressUpdate(0.80);
+			
+			// Check for hazards
+			if (checkHazard) {
+				MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(), mciFile.getCanonicalPath());
+				if (MpsatUtilitySettings.getDebugReach()) {
+					System.out.println("\nReach expression for the hazard property:");
+					System.out.println(hazardSettings.getReach());
+				}
+				Result<? extends ExternalProcessResult>  mpsatHazardResult = framework.getTaskManager().execute(
+						mpsatHazardTask, "Running hazard check [MPSat]", subtaskMonitor);
+
+				if (mpsatHazardResult.getOutcome() != Outcome.FINISHED) {
+					if (mpsatHazardResult.getOutcome() == Outcome.CANCELLED) {
+						return new Result<MpsatChainResult>(Outcome.CANCELLED);
+					}
+					return new Result<MpsatChainResult>(Outcome.FAILED, 
+							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings));
+				}
+				monitor.progressUpdate(0.90);
+
+				MpsatResultParser mpsatHazardParser = new MpsatResultParser(mpsatHazardResult.getReturnValue());
+				if (!mpsatHazardParser.getSolutions().isEmpty()) {
+					mciFile.delete();
+					return new Result<MpsatChainResult>(Outcome.FINISHED, 
+							new MpsatChainResult(circuitExportResult, pcompResult, punfResult, mpsatHazardResult, hazardSettings, 
+									"Circuit has a hazard  after the following trace:"));
+				}
 			}
 			monitor.progressUpdate(1.0);
 
+			// Success
 			mciFile.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";
+			}
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Circuit is deadlock-free and hazard-free"));
-			
+					new MpsatChainResult(circuitExportResult, pcompResult, punfResult, null, toolchainCompletionSettings, message));
+
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
 		}
 
=== removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitDeadlockTool.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitDeadlockTool.java	2013-09-17 14:58:15 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitDeadlockTool.java	1970-01-01 00:00:00 +0000
@@ -1,43 +0,0 @@
-package org.workcraft.plugins.circuit.tools;
-
-import org.workcraft.Framework;
-import org.workcraft.Tool;
-import org.workcraft.plugins.circuit.Circuit;
-import org.workcraft.plugins.circuit.tasks.CheckCircuitDeadlockTask;
-import org.workcraft.plugins.mpsat.MpsatChainResultHandler;
-import org.workcraft.workspace.WorkspaceEntry;
-
-public class CheckCircuitDeadlockTool implements Tool {
-	private final Framework framework;
-
-	public CheckCircuitDeadlockTool(Framework framework) {
-		this.framework = framework;
-	}
-	
-	public String getDisplayName() {
-		return "Check circuit for deadlocks";
-	}
-
-
-	@Override
-	public String getSection() {
-		return "Verification";
-	}
-
-	@Override
-	public boolean isApplicableTo(WorkspaceEntry we) {
-		return we.getModelEntry().getMathModel() instanceof Circuit;
-	}
-
-	@Override
-	public void run(WorkspaceEntry we) {
-		final CheckCircuitDeadlockTask task = new CheckCircuitDeadlockTask(we, framework);
-		String description = "MPSat tool chain";
-		String title = we.getModelEntry().getModel().getTitle();
-		if (!title.isEmpty()) {
-			description += "(" + title +")";
-		}
-		framework.getTaskManager().queue(task, description, new MpsatChainResultHandler(task));
-	}
-
-}
 
=== removed file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitHazardTool.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitHazardTool.java	2013-09-17 14:58:15 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitHazardTool.java	1970-01-01 00:00:00 +0000
@@ -1,43 +0,0 @@
-package org.workcraft.plugins.circuit.tools;
-
-import org.workcraft.Framework;
-import org.workcraft.Tool;
-import org.workcraft.plugins.circuit.Circuit;
-import org.workcraft.plugins.circuit.tasks.CheckCircuitHazardTask;
-import org.workcraft.plugins.mpsat.MpsatChainResultHandler;
-import org.workcraft.workspace.WorkspaceEntry;
-
-public class CheckCircuitHazardTool implements Tool {
-	private final Framework framework;
-
-	public CheckCircuitHazardTool(Framework framework) {
-		this.framework = framework;
-	}
-	
-	public String getDisplayName() {
-		return "Check circuit for hazards";
-	}
-
-
-	@Override
-	public String getSection() {
-		return "Verification";
-	}
-
-	@Override
-	public boolean isApplicableTo(WorkspaceEntry we) {
-		return we.getModelEntry().getMathModel() instanceof Circuit;
-	}
-
-	@Override
-	public void run(WorkspaceEntry we) {
-		final CheckCircuitHazardTask task = new CheckCircuitHazardTask(we, framework);
-		String description = "MPSat tool chain";
-		String title = we.getModelEntry().getModel().getTitle();
-		if (!title.isEmpty()) {
-			description += "(" + title +")";
-		}
-		framework.getTaskManager().queue(task, description, new MpsatChainResultHandler(task));
-	}
-
-}
 
=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitTool.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitTool.java	2013-09-17 14:58:15 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/CheckCircuitTool.java	2014-04-29 16:24:51 +0000
@@ -15,10 +15,9 @@
 	}
 	
 	public String getDisplayName() {
-		return "Check circuit for deadlocks and hazards (reuse unfolding data)";
+		return "Check circuit for conformation, deadlocks and hazards (reuse unfolding)";
 	}
 
-
 	@Override
 	public String getSection() {
 		return "Verification";
@@ -31,7 +30,8 @@
 
 	@Override
 	public void run(WorkspaceEntry we) {
-		final CheckCircuitTask task = new CheckCircuitTask(we, framework);
+		final CheckCircuitTask task = new CheckCircuitTask(we, framework, 
+				checkConformation(), checkDeadlock(), checkHazard());
 		String description = "MPSat tool chain";
 		String title = we.getModelEntry().getModel().getTitle();
 		if (!title.isEmpty()) {
@@ -40,4 +40,16 @@
 		framework.getTaskManager().queue(task, description, new MpsatChainResultHandler(task));
 	}
 
+	public boolean checkConformation() {
+		return true;
+	}
+
+	public boolean checkDeadlock() {
+		return true;
+	}
+
+	public boolean checkHazard() {
+		return true;
+	}
+
 }
 
=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java	2014-01-14 10:38:16 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tools/STGGenerator.java	2014-04-29 16:24:51 +0000
@@ -22,6 +22,7 @@
 import org.workcraft.dom.visual.VisualNode;
 import org.workcraft.exceptions.InvalidConnectionException;
 import org.workcraft.plugins.circuit.Contact;
+import org.workcraft.plugins.circuit.Contact.IOType;
 import org.workcraft.plugins.circuit.VisualCircuit;
 import org.workcraft.plugins.circuit.VisualCircuitComponent;
 import org.workcraft.plugins.circuit.VisualCircuitConnection;
@@ -29,7 +30,6 @@
 import org.workcraft.plugins.circuit.VisualFunctionComponent;
 import org.workcraft.plugins.circuit.VisualFunctionContact;
 import org.workcraft.plugins.circuit.VisualJoint;
-import org.workcraft.plugins.circuit.Contact.IOType;
 import org.workcraft.plugins.cpog.optimisation.Literal;
 import org.workcraft.plugins.cpog.optimisation.booleanvisitors.FormulaToString;
 import org.workcraft.plugins.cpog.optimisation.dnf.Dnf;
@@ -40,9 +40,9 @@
 import org.workcraft.plugins.petri.VisualPlace;
 import org.workcraft.plugins.stg.STG;
 import org.workcraft.plugins.stg.SignalTransition;
+import org.workcraft.plugins.stg.SignalTransition.Direction;
 import org.workcraft.plugins.stg.VisualSTG;
 import org.workcraft.plugins.stg.VisualSignalTransition;
-import org.workcraft.plugins.stg.SignalTransition.Direction;
 import org.workcraft.util.Hierarchy;
 
 public class STGGenerator {
@@ -172,36 +172,34 @@
 			}
 			
 			// generate implementation for each of the drivers
-			for(VisualContact c : drivers.keySet())
-			{
+			for(VisualContact c : drivers.keySet()) {
 				if (c instanceof VisualFunctionContact) {
 					// function based driver
+					Dnf set = null;
+					Dnf reset = null;
 					VisualFunctionContact contact = (VisualFunctionContact)c;
-					Dnf set = DnfGenerator.generate(contact.getFunction().getSetFunction());
-					Dnf reset = null;
-					
-					if (contact.getFunction().getResetFunction()!=null) 
-						reset = DnfGenerator.generate(contact.getFunction().getResetFunction());
-					else {
-						BooleanOperations.worker = new DumbBooleanWorker();
-						reset = DnfGenerator.generate(BooleanOperations.worker.not(contact.getFunction().getSetFunction()));
-					}
-					
 					SignalTransition.Type ttype = SignalTransition.Type.OUTPUT;
-					
-					
 					if (contact.getParent() instanceof VisualCircuitComponent) {
-						if (((VisualCircuitComponent)contact.getParent()).getIsEnvironment()) 
-								ttype = SignalTransition.Type.INPUT; 
-						else if (contact.getIOType()==IOType.INPUT)
+						set = DnfGenerator.generate(contact.getFunction().getSetFunction());
+						if (contact.getFunction().getResetFunction() != null) { 
+							reset = DnfGenerator.generate(contact.getFunction().getResetFunction());
+						} else {
+							BooleanOperations.worker = new DumbBooleanWorker();
+							reset = DnfGenerator.generate(BooleanOperations.worker.not(contact.getFunction().getSetFunction()));
+						}
+						if (((VisualCircuitComponent)contact.getParent()).getIsEnvironment()) { 
+							ttype = SignalTransition.Type.INPUT; 
+						} else if (contact.getIOType()==IOType.INPUT) {
 							ttype = SignalTransition.Type.INPUT;
+						}
 					} else {
-						if (contact.getIOType()==IOType.INPUT)
+						set = DnfGenerator.generate(contact.getFunction().getSetFunction());
+						reset = DnfGenerator.generate(contact.getFunction().getResetFunction());
+						if (contact.getIOType()==IOType.INPUT) {
 							ttype = SignalTransition.Type.INPUT;
+						}
 					}
-					
 					implementDriver(circuit, stg, contact, drivers, targetDrivers, set, reset, ttype);
-					
 				} else {
 					// some generic driver implementation otherwise
 					Dnf set = new Dnf(new DnfClause());
@@ -209,7 +207,6 @@
 					implementDriver(circuit, stg, c, drivers, targetDrivers, set, reset, SignalTransition.Type.INPUT);
 				}
 			}
-			
 			return stg;
 		} catch (InvalidConnectionException e) {
 			throw new RuntimeException(e);
 
=== modified file 'CpogsPlugin/src/org/workcraft/plugins/cpog/optimisation/dnf/DnfGenerator.java'
--- CpogsPlugin/src/org/workcraft/plugins/cpog/optimisation/dnf/DnfGenerator.java	2012-07-25 10:32:14 +0000
+++ CpogsPlugin/src/org/workcraft/plugins/cpog/optimisation/dnf/DnfGenerator.java	2014-04-29 16:24:51 +0000
@@ -20,6 +20,9 @@
 public class DnfGenerator {
 	public static Dnf generate(BooleanFormula formula)
 	{
+		if (formula == null) {
+			formula = One.instance();
+		}
 		return formula.accept(new BooleanVisitor<Dnf>()
 				{
 					boolean negation = false;
@@ -218,7 +221,6 @@
 			
 		}
 		
-		
 		return simplifyDnf(result);
 	}
 
 
=== modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/VisualDfs.java'
--- DfsPlugin/src/org/workcraft/plugins/dfs/VisualDfs.java	2014-04-08 08:59:38 +0000
+++ DfsPlugin/src/org/workcraft/plugins/dfs/VisualDfs.java	2014-04-29 16:24:51 +0000
@@ -28,7 +28,6 @@
 
 import org.workcraft.annotations.CustomTools;
 import org.workcraft.annotations.DisplayName;
-import org.workcraft.dom.Connection;
 import org.workcraft.dom.Node;
 import org.workcraft.dom.math.MathConnection;
 import org.workcraft.dom.math.MathNode;
@@ -221,11 +220,4 @@
 		return result;
 	} 
 	
-	public Connection getConnection(Node first, Node second) {
-		for(Connection connection : getConnections(first)) {
-			if (connection.getSecond() == second) return connection;
-		}
-		return null;
-	}
-	
-}
 \ No newline at end of file
+}
 
=== modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java'
--- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java	2014-04-16 21:55:15 +0000
+++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java	2014-04-29 16:24:51 +0000
@@ -53,20 +53,24 @@
 			File netFile = File.createTempFile("net", exporter.getExtenstion());
 			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);
+			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);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, null, null, settings));
+						new MpsatChainResult(exportResult, null, null, null, settings));
 			}
 			monitor.progressUpdate(0.20);
 			
 			File mciFile = File.createTempFile("unfolding", ".mci");
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
+			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
+					punfTask, "Unfolding .g", mon);
+			
 			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
 				mciFile.delete();
@@ -74,18 +78,21 @@
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, null, settings));
+						new MpsatChainResult(exportResult, null, punfResult, null, settings));
 			}
 			monitor.progressUpdate(0.70);
 
 			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon);
+			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
+					mpsatTask, "Running deadlock checking [MPSat]", mon);
+			
 			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
 				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, new String(mpsatResult.getReturnValue().getErrors())));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, 
+								new String(mpsatResult.getReturnValue().getErrors())));
 			}
 			monitor.progressUpdate(0.90);
 			
@@ -93,13 +100,13 @@
 			if (!mdp.getSolutions().isEmpty()) {
 				mciFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow has a deadlock"));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow has a deadlock"));
 			}
 			monitor.progressUpdate(1.0);
 
 			mciFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow is deadlock-free"));
+					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow is deadlock-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
 
=== modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java'
--- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java	2014-04-16 21:55:15 +0000
+++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java	2014-04-29 16:24:51 +0000
@@ -54,38 +54,45 @@
 			File netFile = File.createTempFile("net", exporter.getExtenstion());
 			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);
+			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);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, null, null, settings));
+						new MpsatChainResult(exportResult, null, null, null, settings));
 			}
 			monitor.progressUpdate(0.20);
 			
 			File mciFile = File.createTempFile("unfolding", ".mci");
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
+			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
+					punfTask, "Unfolding .g", mon);
+			
 			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
 				mciFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
-				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, punfResult, null, settings));
+				return new Result<MpsatChainResult>(Outcome.FAILED, 
+						new MpsatChainResult(exportResult, null, punfResult, null, settings));
 			}
 			monitor.progressUpdate(0.40);
 
 			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running semimodularity checking [MPSat]", mon);
+			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
+					mpsatTask, "Running semimodularity checking [MPSat]", mon);
+			
 			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
 				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings));
 			}
 			monitor.progressUpdate(0.90);
 			
@@ -93,13 +100,13 @@
 			if (!mdp.getSolutions().isEmpty()) {
 				mciFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow has hazard(s)"));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow has hazard(s)"));
 			}
 			monitor.progressUpdate(1.0);
 
 			mciFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Dataflow is hazard-free"));
+					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow is hazard-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
 
=== modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java'
--- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java	2014-04-16 21:55:15 +0000
+++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java	2014-04-29 16:24:51 +0000
@@ -59,20 +59,24 @@
 			File netFile = File.createTempFile("net", exporter.getExtenstion());
 			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);
+			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);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, null, null, deadlockSettings));
+						new MpsatChainResult(exportResult, null, null, null, deadlockSettings));
 			}
 			monitor.progressUpdate(0.20);
 			
 			File mciFile = File.createTempFile("unfolding", ".mci");
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
+			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
+					punfTask, "Unfolding .g", mon);
+			
 			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
 				mciFile.delete();
@@ -80,18 +84,20 @@
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, null, deadlockSettings));
+						new MpsatChainResult(exportResult, null, punfResult, null, deadlockSettings));
 			}
 			monitor.progressUpdate(0.40);
 
 			MpsatTask mpsatTask = new MpsatTask(deadlockSettings.getMpsatArguments(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon);
+			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
+					mpsatTask, "Running deadlock checking [MPSat]", mon);
+			
 			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
 				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, deadlockSettings));
 			}
 			monitor.progressUpdate(0.60);
 			
@@ -99,7 +105,7 @@
 			if (!mdp.getSolutions().isEmpty()) {
 				mciFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, deadlockSettings, "Dataflow has a deadlock"));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, deadlockSettings, "Dataflow has a deadlock"));
 			}
 			monitor.progressUpdate(0.70);
 
@@ -110,7 +116,7 @@
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings));
 			}
 			monitor.progressUpdate(0.90);
 			
@@ -118,13 +124,13 @@
 			if (!mdp.getSolutions().isEmpty()) {
 				mciFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Dataflow has hazard(s)"));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings, "Dataflow has hazard(s)"));
 			}
 			monitor.progressUpdate(1.0);
 
 			mciFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(exportResult, punfResult, mpsatResult, hazardSettings, "Dataflow is deadlock-free and hazard-free"));
+					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings, "Dataflow is deadlock-free and hazard-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatChainResultHandler.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatChainResultHandler.java	2014-04-16 21:55:15 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatChainResultHandler.java	2014-04-29 16:24:51 +0000
@@ -26,6 +26,9 @@
 		if (result.getOutcome() == Outcome.FINISHED) {
 			final MpsatMode mpsatMode = result.getReturnValue().getMpsatSettings().getMode();
 			switch (mpsatMode) {
+			case UNDEFINED:
+				SwingUtilities.invokeLater(new MpsatUndefinedResultHandler(task, result));
+				break;
 			case STG_REACHABILITY:
 			case CSC_CONFLICT_DETECTION:
 			case USC_CONFLICT_DETECTION:
@@ -41,7 +44,6 @@
 			case COMPLEX_GATE_IMPLEMENTATION:
 				SwingUtilities.invokeLater(new MpsatSynthesisResultHandler(task, result));
 				break;
-
 			default:
 				SwingUtilities.invokeLater(new Runnable() {
 					@Override
@@ -53,57 +55,62 @@
 				});
 				break;
 			}			
-		}
-		else if (result.getOutcome() != Outcome.CANCELLED) {
+		} else if (result.getOutcome() != Outcome.CANCELLED) {
 			errorMessage = "MPSat tool chain execution failed :-(";
-
 			Throwable cause1 = result.getCause();
 
 			if (cause1 != null) {
 				// Exception was thrown somewhere in the chain task run() method (not in any of the subtasks)
 				errorMessage += "\n\nFailure caused by: " + cause1.toString() + "\nPlease see the \"Problems\" tab for more details.";
-			} else
-			{
-				Result<? extends Object> exportResult = result.getReturnValue().getExportResult();
-				if (exportResult.getOutcome() == Outcome.FAILED) {
+			} else {
+				MpsatChainResult returnValue = result.getReturnValue();
+				Result<? extends Object> exportResult = returnValue.getExportResult();
+				Result<? extends ExternalProcessResult> pcompResult = returnValue.getPcompResult();
+				Result<? extends ExternalProcessResult> punfResult = returnValue.getPunfResult();
+				Result<? extends ExternalProcessResult> mpsatResult = returnValue.getMpsatResult();
+				if (exportResult != null && exportResult.getOutcome() == Outcome.FAILED) {
 					errorMessage += "\n\nFailed to export the model as a .g file.";
 					Throwable cause = exportResult.getCause();
-					if (cause != null)
-						errorMessage += "\n\nFailure caused by: " + cause.toString() + "\nPlease see the \"Problems\" tab for more details.";
-					else
+					if (cause != null) {
+						errorMessage += "\n\nFailure caused by: " + cause.toString();
+					} else {
 						errorMessage += "\n\nThe exporter class did not offer further explanation.";
+					}
+				} else if (pcompResult != null && pcompResult.getOutcome() == Outcome.FAILED) {
+					errorMessage += "\n\nPcomp could not compose the STGs.";
+					Throwable cause = pcompResult.getCause();
+					if (cause != null) {
+						errorMessage += "\n\nFailure caused by: " + cause.toString();
+					} else {
+						errorMessage += "\n\nFailure caused by the following errors:\n" + new String(pcompResult.getReturnValue().getErrors());
+					}
+				} else if (punfResult != null && punfResult.getOutcome() == Outcome.FAILED) {
+					errorMessage += "\n\nPunf could not build the unfolding prefix.";
+					Throwable cause = punfResult.getCause();
+					if (cause != null) {
+						errorMessage += "\n\nFailure caused by: " + cause.toString();
+					} else {
+						errorMessage += "\n\nFailure caused by the following errors:\n" + new String(punfResult.getReturnValue().getErrors());
+					}
+				} else if (mpsatResult != null && mpsatResult.getOutcome() == Outcome.FAILED) {
+					errorMessage += "\n\nMPSat failed to execute as expected.";
+					Throwable cause = mpsatResult.getCause();
+					if (cause != null) {
+						errorMessage += "\n\nFailure caused by: " + cause.toString();
+					} else {
+						errorMessage += "\n\nFailure caused by the following errors:\n" + new String(mpsatResult.getReturnValue().getErrors());
+					}
 				} else {
-					Result<? extends ExternalProcessResult> punfResult = result.getReturnValue().getPunfResult();
-
-					if (punfResult.getOutcome() == Outcome.FAILED) {
-						errorMessage += "\n\nPunf could not build the unfolding prefix.";
-						Throwable cause = punfResult.getCause();
-						if (cause != null)
-							errorMessage += "\n\nFailure caused by: " + cause.toString() + "\nPlease see the \"Problems\" tab for more details.";
-						else
-							errorMessage += "\n\nFailure caused by the following errors:\n" + new String(punfResult.getReturnValue().getErrors()); 
-					} else {
-						Result<? extends ExternalProcessResult> mpsatResult = result.getReturnValue().getMpsatResult();
-
-						if (mpsatResult.getOutcome() == Outcome.FAILED) {
-							errorMessage += "\n\nMPSat failed to execute as expected.";
-							Throwable cause = mpsatResult.getCause();
-							if (cause != null)
-								errorMessage += "\n\nFailure caused by: " + cause.toString() + "\nPlease see the \"Problems\" tab for more details.";
-							else
-								errorMessage += "\n\nFailure caused by the following errors:\n" + new String(mpsatResult.getReturnValue().getErrors());
-						}
-						else {
-							errorMessage += "\n\nMPSat chain task returned failure status without further explanation. This should not have happened -_-a.";
-						}
-					}
+					errorMessage += "\n\nMPSat chain task returned failure status without further explanation.";
 				}
 			}
 			SwingUtilities.invokeLater(new Runnable() {
 				@Override
 				public void run() {
-					JOptionPane.showMessageDialog(null, errorMessage, "Oops..", JOptionPane.ERROR_MESSAGE);				}
+					JOptionPane.showMessageDialog(null, errorMessage, "Oops..", JOptionPane.ERROR_MESSAGE);
+				}
 			});
 		}
 	}
-}
 \ No newline at end of file
+
+}
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java	2010-10-06 15:51:01 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatMode.java	2014-04-29 16:24:51 +0000
@@ -4,6 +4,7 @@
 package org.workcraft.plugins.mpsat;
 
 public enum MpsatMode {
+	UNDEFINED (null, null, false), // Special mode to integrate foreign tasks into Mpsat toolchain (export, composition, unfolding)
 	DEADLOCK ("-D", "Deadlock checking", false),
 	REACHABILITY ("-F", "Reachability analysis", true), 
 	STG_REACHABILITY ("-Fs", "STG reachability analysis", true),
@@ -20,8 +21,7 @@
 	private String description;
 	private boolean reach;
 	
-	public static final MpsatMode[] modes = 
-	{
+	public static final MpsatMode[] modes = {
 		DEADLOCK,
 		REACHABILITY,
 		STG_REACHABILITY,
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java	2014-04-16 21:55:15 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java	2014-04-29 16:24:51 +0000
@@ -6,9 +6,14 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
+import java.util.HashSet;
 import java.util.LinkedHashMap;
 import java.util.Map;
 
+import org.workcraft.dom.Node;
+import org.workcraft.plugins.stg.STG;
+import org.workcraft.plugins.stg.SignalTransition;
+import org.workcraft.plugins.stg.SignalTransition.Type;
 import org.workcraft.util.FileUtils;
 
 public class MpsatSettings {
@@ -33,12 +38,12 @@
 		}
 	}
 
-	private String name = null;
-	private MpsatMode mode = MpsatMode.DEADLOCK;
-	private int verbosity = 0;
-	private SolutionMode solutionMode = SolutionMode.FIRST;
-	private int solutionNumberLimit = 0;
-	private String reach = "";
+	private final String name;
+	private final MpsatMode mode;
+	private final int verbosity;
+	private final SolutionMode solutionMode;
+	private final int solutionNumberLimit;
+	private final String reach;
 	
 	// Reach expression for checking signal consistency
 	public static final String reachConsistency = 
@@ -52,17 +57,121 @@
 
 	// 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"+
+		"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";
 	
+	// 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 =
+		"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";
+	
+	// FIXME: Currently 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.getSignalNames(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);
+				}
+			}
+		}
+		// Generate Reach expression
+		String result = "";
+		for (String s : circuitStg.getSignalNames(Type.OUTPUT)) {
+			String circuitPredicate = "";
+			String environmentPredicate = "";
+			for (SignalTransition t: stg.getSignalTransitions(Type.OUTPUT)) {
+				if (!t.getSignalName().equals(s)) continue;
+				String circuitPreset = "";
+				String environmentPreset = "";
+				for (Node p: stg.getPreset(t)) {
+					String name = stg.getNodeReference(p);
+					if (circuitPlaces.contains(p)) {
+						if (circuitPreset.isEmpty()) {
+							circuitPreset += "{";
+						} else {
+							circuitPreset += ", ";
+						}
+						circuitPreset += "\"" + name + "\"";
+					} else {
+						if (environmentPreset.isEmpty()) {
+							environmentPreset += "{";
+						} else {
+							environmentPreset += ", ";
+						}
+						environmentPreset += "\"" + name + "\"";
+					}
+				}
+				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 += "|\n";
+			}
+			result += "/* Conformation check for signal " + s + " */\n";
+			result += "(\n";
+			result += circuitPredicate;
+			result += "   &\n";
+			result += environmentPredicate;
+			result += ")\n";
+		}
+		return result;
+	}
+
+	
 	public MpsatSettings(String name, MpsatMode mode, int verbosity, SolutionMode solutionMode, int solutionNumberLimit, String reach) {
 		super();
 		this.name = name;
@@ -122,10 +231,11 @@
 			break;
 		case ALL:
 			int solutionNumberLimit = getSolutionNumberLimit();
-			if (solutionNumberLimit>0)
+			if (solutionNumberLimit>0) {
 				args.add("-a" + Integer.toString(solutionNumberLimit));
-			else
+			} else {
 				args.add("-a");
+			}
 		}
 
 		return args.toArray(new String[args.size()]);
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatStgReachabilityResultHandler.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatStgReachabilityResultHandler.java	2014-04-16 21:55:15 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatStgReachabilityResultHandler.java	2014-04-29 16:24:51 +0000
@@ -22,24 +22,32 @@
 		this.result = result;
 	}
 	
+	private String getPropertyName() {
+		String propertyName;
+		MpsatSettings settings = task.getSettings();
+		if (settings != null && settings.getName() != null) {
+			propertyName = settings.getName();
+		} else {
+			propertyName = "The property";
+		}
+		return propertyName;
+	}
 	
 	@Override
 	public void run() {
 		MpsatResultParser mdp = new MpsatResultParser(result.getReturnValue().getMpsatResult().getReturnValue());
 		List<Trace> solutions = mdp.getSolutions();
-		String propertyName = task.getSettings().getName();
-		if (propertyName == null) {
-			propertyName = "The property";
-		}
+		String message = result.getReturnValue().getMessage();
 		if (!solutions.isEmpty()) {
-			String message = propertyName + " is violated with the following trace:\n";
+			if (message == null) {
+				message = getPropertyName() + " is violated with the following trace:\n";
+			}
 			final SolutionsDialog solutionsDialog = new SolutionsDialog(task, message, solutions);
 			GUI.centerAndSizeToParent(solutionsDialog, task.getFramework().getMainWindow());
 			solutionsDialog.setVisible(true);
 		} else {
-			String message = result.getReturnValue().getMessage();
 			if (message == null) {
-				message = propertyName + " is satisfied.";
+				message = getPropertyName() + " is satisfied.";
 			}
 			JOptionPane.showMessageDialog(null, message);
 		}
 
=== added file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUndefinedResultHandler.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUndefinedResultHandler.java	1970-01-01 00:00:00 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUndefinedResultHandler.java	2014-04-29 16:24:51 +0000
@@ -0,0 +1,32 @@
+package org.workcraft.plugins.mpsat;
+
+import javax.swing.JOptionPane;
+
+import org.workcraft.plugins.mpsat.tasks.MpsatChainResult;
+import org.workcraft.plugins.mpsat.tasks.MpsatChainTask;
+import org.workcraft.tasks.Result;
+
+
+final class MpsatUndefinedResultHandler implements Runnable {
+
+	private final Result<? extends MpsatChainResult> result;
+	private final MpsatChainTask task;
+	
+	MpsatUndefinedResultHandler(MpsatChainTask task, Result<? extends MpsatChainResult> result) {
+		this.task = task;
+		this.result = result;
+	}
+	
+	@Override
+	public void run() {
+		String message = result.getReturnValue().getMessage();
+		if (message == null) {
+			MpsatSettings settings = task.getSettings();
+			if (settings != null && settings.getName() != null) {
+				message = settings.getName();
+			}
+		}
+		JOptionPane.showMessageDialog(null, message);
+	}
+
+}
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java	2013-10-15 12:25:49 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatUtilitySettings.java	2014-04-29 16:24:51 +0000
@@ -35,10 +35,12 @@
 	private static final String commandKey = "Tools.mpsat.command";
 	private static final String solutionModeKey = "Tools.mpsat.solutionMode";
 	private static final String extraArgsKey = "Tools.mpsat.args";
+	private static final String debugReachKey = "Tools.mpsat.debugReach";
 	
 	private static String command = "mpsat";
 	private static SolutionMode solutionMode = SolutionMode.MINIMUM_COST;
 	private static String extraArgs = "";
+	private static Boolean debugReach = false;
 
 	public MpsatUtilitySettings() {
 		properties = new LinkedList<PropertyDescriptor>();
@@ -72,6 +74,16 @@
 				return MpsatUtilitySettings.getExtraArgs();
 			}
 		});
+
+		properties.add(new PropertyDeclaration<MpsatUtilitySettings, Boolean>(
+				this, "MPSat debug", Boolean.class) {
+			protected void setter(MpsatUtilitySettings object, Boolean value) {
+				MpsatUtilitySettings.setDebugReach(value);
+			}
+			protected Boolean getter(MpsatUtilitySettings object) {
+				return MpsatUtilitySettings.getDebugReach();
+			}
+		});
 	}
 	
 	@Override
@@ -84,6 +96,7 @@
 		command = config.getString(commandKey, "mpsat");
 		solutionMode = config.getEnum(solutionModeKey, SolutionMode.class, SolutionMode.FIRST);
 		extraArgs = config.getString(extraArgsKey, "");
+		debugReach = config.getBoolean(debugReachKey, false);
 	}
 
 	@Override
@@ -91,6 +104,7 @@
 		config.set(commandKey, command);
 		config.setEnum(solutionModeKey, SolutionMode.class, solutionMode);
 		config.set(extraArgsKey, extraArgs);
+		config.setBoolean(debugReachKey, debugReach);
 	}
 	
 	@Override
@@ -130,4 +144,12 @@
 	public static int getSolutionCount() {
 		return (MpsatUtilitySettings.solutionMode == SolutionMode.ALL) ? 10 : 1;
 	}
+
+	public static Boolean getDebugReach() {
+		return debugReach;
+	}
+
+	public static void setDebugReach(Boolean debug) {
+		MpsatUtilitySettings.debugReach = debug;
+	}
 }
 \ No newline at end of file
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java	2014-04-16 22:13:32 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/MpsatConfigurationDialog.java	2014-04-29 16:24:51 +0000
@@ -154,7 +154,7 @@
 	}
 
 	private void createSolutionModeButtons() {
-		firstSolutionButton = new JRadioButton ("Find any solution (default)");
+		firstSolutionButton = new JRadioButton ("Find any solution");
 		firstSolutionButton.setSelected(true);
 		firstSolutionButton.addActionListener(new ActionListener() {
 			@Override
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/SolutionPanel.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/SolutionPanel.java	2014-04-16 21:55:15 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/gui/SolutionPanel.java	2014-04-29 16:24:51 +0000
@@ -43,7 +43,7 @@
 		
 		JButton saveButton = new JButton("Save");		
 		
-		JButton playButton = new JButton("Play trace");
+		JButton playButton = new JButton("Play");
 		playButton.addActionListener(new ActionListener()
 		{
 			@Override
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainResult.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainResult.java	2010-11-18 02:08:34 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainResult.java	2014-04-29 16:24:51 +0000
@@ -5,38 +5,47 @@
 import org.workcraft.tasks.Result;
 
 public class MpsatChainResult {
+	private Result<? extends Object> exportResult; 
+	private Result<? extends ExternalProcessResult> pcompResult;
 	private Result<? extends ExternalProcessResult> punfResult;
 	private Result<? extends ExternalProcessResult> mpsatResult;
-	private Result<? extends Object> exportResult; 
 	private MpsatSettings mpsatSettings;
 	private String message;
+	
+	public MpsatChainResult(Result<? extends Object> exportResult,
+			Result<? extends ExternalProcessResult> pcompResult,
+			Result<? extends ExternalProcessResult> punfResult,
+			Result<? extends ExternalProcessResult> mpsatResult,
+			MpsatSettings mpsatSettings, String message) {
 		
+		this.exportResult = exportResult;
+		this.pcompResult = pcompResult;
+		this.punfResult = punfResult;
+		this.mpsatResult = mpsatResult;
+		this.mpsatSettings = mpsatSettings;
+		this.message = message;
+	}
+	
 	public MpsatChainResult(Result<? extends Object> exportResult,
-				Result<? extends ExternalProcessResult> punfResult,
+			Result<? extends ExternalProcessResult> pcompResult,
+			Result<? extends ExternalProcessResult> punfResult,
 			Result<? extends ExternalProcessResult> mpsatResult,
 			MpsatSettings mpsatSettings) {
-		this.punfResult = punfResult;
-		this.mpsatResult = mpsatResult;
-		this.exportResult = exportResult;
-		this.mpsatSettings = mpsatSettings;
-	}
-	
-	public MpsatChainResult(Result<? extends Object> exportResult,
-			Result<? extends ExternalProcessResult> punfResult,
-		Result<? extends ExternalProcessResult> mpsatResult,
-		MpsatSettings mpsatSettings, String message) {
-		
-		this.punfResult = punfResult;
-		this.mpsatResult = mpsatResult;
-		this.exportResult = exportResult;
-		this.mpsatSettings = mpsatSettings;
-		
-		this.message = message;
+		
+		this(exportResult, pcompResult, punfResult, mpsatResult, mpsatSettings, null);
 	}
 	
 	public MpsatSettings getMpsatSettings() {
 		return mpsatSettings;
 	}
+	
+	public Result<? extends Object> getExportResult() {
+		return exportResult;
+	}
+
+	public Result<? extends ExternalProcessResult> getPcompResult() {
+		return pcompResult;
+	}
 
 	public Result<? extends ExternalProcessResult> getPunfResult() {
 		return punfResult;
@@ -49,8 +58,4 @@
 	public String getMessage() {
 		return message;
 	}
-
-	public Result<? extends Object> getExportResult() {
-		return exportResult;
-	}
 }
 \ No newline at end of file
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java	2014-04-16 21:55:15 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java	2014-04-29 16:24:51 +0000
@@ -50,7 +50,7 @@
 				netFile.delete();
 				if (exportResult.getOutcome() == Outcome.CANCELLED)
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, null, settings));
+				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, null, null, settings));
 			}
 			monitor.progressUpdate(0.33);
 			
@@ -63,7 +63,7 @@
 				mciFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED)
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, punfResult, null, settings));
+				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, punfResult, null, settings));
 			}
 
 			monitor.progressUpdate(0.66);
@@ -75,12 +75,12 @@
 			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
 				if (mpsatResult.getOutcome() == Outcome.CANCELLED)
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
-				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, punfResult, mpsatResult, settings ));
+				return new Result<MpsatChainResult>(Outcome.FAILED, new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings ));
 			}
 		
 			monitor.progressUpdate(1.0);
 			
-			return new Result<MpsatChainResult>(Outcome.FINISHED, new MpsatChainResult(exportResult, punfResult, mpsatResult, settings));
+			return new Result<MpsatChainResult>(Outcome.FINISHED, new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings));
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
 		}
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompResultHandler.java'
--- MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompResultHandler.java	2010-09-21 15:39:20 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompResultHandler.java	2014-04-29 16:24:51 +0000
@@ -40,9 +40,9 @@
 				if (result.getCause() != null) {
 					message = result.getCause().getMessage();
 					result.getCause().printStackTrace();
-				}
-				else
+				} else {
 					message = "Pcomp errors: \n" + new String(result.getReturnValue().getErrors());
+				}
 				JOptionPane.showMessageDialog(framework.getMainWindow(), message, "Parallel composition failed", JOptionPane.ERROR_MESSAGE);
 			} else if (result.getOutcome() == Outcome.FINISHED) {
 				try {
 
=== modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java'
--- MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java	2014-04-16 17:52:01 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tools/PcompTool.java	2014-04-29 16:24:51 +0000
@@ -45,7 +45,9 @@
 				inputs.add(dotGProvider.getDotG(p));
 			}
 			
-			framework.getTaskManager().queue(new PcompTask(inputs.toArray(new File[0]), dialog.getMode(), dialog.isImprovedPcompChecked()), "Running pcomp", new PcompResultHandler(framework, dialog.showInEditor()));
+			PcompTask pcompTask = new PcompTask(inputs.toArray(new File[0]), dialog.getMode(), dialog.isImprovedPcompChecked());
+			PcompResultHandler pcompResult = new PcompResultHandler(framework, dialog.showInEditor());
+			framework.getTaskManager().queue(pcompTask,	"Running pcomp", pcompResult);
 		}
 	}
 
 
=== modified file 'PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java'
--- PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java	2014-04-16 21:55:15 +0000
+++ PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java	2014-04-29 16:24:51 +0000
@@ -53,20 +53,24 @@
 			File netFile = File.createTempFile("net", exporter.getExtenstion());
 			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);
+			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);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, null, null, settings));
+						new MpsatChainResult(exportResult, null, null, null, settings));
 			}
 			monitor.progressUpdate(0.20);
 			
 			File mciFile = File.createTempFile("unfolding", ".mci");
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(punfTask, "Unfolding .g", mon);
+			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
+					punfTask, "Unfolding .g", mon);
+			
 			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
 				mciFile.delete();
@@ -74,18 +78,21 @@
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, null, settings));
+						new MpsatChainResult(exportResult, null, punfResult, null, settings));
 			}
 			monitor.progressUpdate(0.70);
 
 			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), mciFile.getCanonicalPath());
-			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running deadlock checking [MPSat]", mon);
+			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
+					mpsatTask, "Running deadlock checking [MPSat]", mon);
+			
 			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
 				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, new String(mpsatResult.getReturnValue().getErrors())));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, 
+								new String(mpsatResult.getReturnValue().getErrors())));
 			}
 			monitor.progressUpdate(0.90);
 			
@@ -93,13 +100,13 @@
 			if (!mdp.getSolutions().isEmpty()) {
 				mciFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
-						new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Policy net has a deadlock"));
+						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net has a deadlock"));
 			}
 			monitor.progressUpdate(1.0);
 
 			mciFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
-					new MpsatChainResult(exportResult, punfResult, mpsatResult, settings, "Policy net is deadlock-free"));
+					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net is deadlock-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
 
=== modified file 'STGPlugin/src/org/workcraft/plugins/stg/LabelParser.java'
--- STGPlugin/src/org/workcraft/plugins/stg/LabelParser.java	2014-04-03 17:30:41 +0000
+++ STGPlugin/src/org/workcraft/plugins/stg/LabelParser.java	2014-04-29 16:24:51 +0000
@@ -20,7 +20,7 @@
 	
 	public static Pair<String, String> parseImplicitPlaceReference(String ref) {
 		String[] parts = ref.replaceAll(" ", "").split(",");
-		if (parts.length < 2 || !parts[0].startsWith("<") || !parts[0].endsWith(">")) {
+		if (parts.length < 2 || !parts[0].startsWith("<") || !parts[1].endsWith(">")) {
 			return null;
 		}
 		return Pair.of(parts[0].substring(1), parts[1].substring(0, parts[1].length()-1));
 
=== modified file 'STGPlugin/src/org/workcraft/plugins/stg/STG.java'
--- STGPlugin/src/org/workcraft/plugins/stg/STG.java	2014-04-22 13:51:18 +0000
+++ STGPlugin/src/org/workcraft/plugins/stg/STG.java	2014-04-29 16:24:51 +0000
@@ -320,12 +320,8 @@
 					throw new RuntimeException(
 							"An implicit place cannot have more that one transition in its preset or postset.");
 				}
-				return "<"
-						+ referenceManager.getNodeReference(preset.iterator()
-								.next())
-						+ ","
-						+ referenceManager.getNodeReference(postset.iterator()
-								.next()) + ">";
+				return "<" + referenceManager.getNodeReference(preset.iterator().next()) + ","
+						+ referenceManager.getNodeReference(postset.iterator().next()) + ">";
 			} else {
 				return referenceManager.getNodeReference(node);
 			}
@@ -335,8 +331,7 @@
 	}
 
 	public Node getNodeByReference(String reference) {
-		Pair<String, String> implicitPlaceTransitions = LabelParser
-				.parseImplicitPlaceReference(reference);
+		Pair<String, String> implicitPlaceTransitions = LabelParser.parseImplicitPlaceReference(reference);
 		if (implicitPlaceTransitions != null) {
 			Node t1 = referenceManager
 					.getNodeByReference(implicitPlaceTransitions.getFirst());
 
=== modified file 'STGPlugin/src/org/workcraft/plugins/stg/VisualSTG.java'
--- STGPlugin/src/org/workcraft/plugins/stg/VisualSTG.java	2014-04-17 15:33:40 +0000
+++ STGPlugin/src/org/workcraft/plugins/stg/VisualSTG.java	2014-04-29 16:24:51 +0000
@@ -246,12 +246,5 @@
 		}
 		return null;
 	}
-	
-	public Connection getConnection(Node first, Node second) {
-		for(Connection connection : getConnections(first)) {
-			if (connection.getSecond() == second) return connection;
-		}
-		return null;
-	}
 
 }
 
=== modified file 'WorkcraftCore/src/org/workcraft/dom/AbstractModel.java'
--- WorkcraftCore/src/org/workcraft/dom/AbstractModel.java	2014-01-29 19:00:22 +0000
+++ WorkcraftCore/src/org/workcraft/dom/AbstractModel.java	2014-04-29 16:24:51 +0000
@@ -131,4 +131,12 @@
 	protected ReferenceManager getReferenceManager() {
 		return referenceManager;
 	}
-}
 \ No newline at end of file
+	
+	public Connection getConnection(Node first, Node second) {
+		for(Connection connection : getConnections(first)) {
+			if (connection.getSecond() == second) return connection;
+		}
+		return null;
+	}
+
+}
 
=== modified file 'WorkcraftCore/src/org/workcraft/gui/propertyeditor/FileCellEditor.java'
--- WorkcraftCore/src/org/workcraft/gui/propertyeditor/FileCellEditor.java	2014-04-09 22:33:19 +0000
+++ WorkcraftCore/src/org/workcraft/gui/propertyeditor/FileCellEditor.java	2014-04-29 16:24:51 +0000
@@ -11,8 +11,6 @@
 import javax.swing.JTable;
 import javax.swing.table.TableCellEditor;
 
-import org.workcraft.gui.FileFilters;
-
 @SuppressWarnings("serial")
 public class FileCellEditor extends AbstractCellEditor implements TableCellEditor, ActionListener {
 	
@@ -34,7 +32,6 @@
 		if (EDIT.equals(e.getActionCommand())) {
 			JFileChooser fc = new JFileChooser();
 			fc.setDialogType(JFileChooser.OPEN_DIALOG);
-			fc.setFileFilter(FileFilters.DOCUMENT_FILES);
 			fc.setMultiSelectionEnabled(false);
 			fc.setSelectedFile(file);
 			fc.setDialogTitle("Open environment file");
 
=== modified file 'WorkcraftCore/src/org/workcraft/plugins/BuiltinSerialisers.java'
--- WorkcraftCore/src/org/workcraft/plugins/BuiltinSerialisers.java	2012-05-22 09:39:39 +0000
+++ WorkcraftCore/src/org/workcraft/plugins/BuiltinSerialisers.java	2014-04-29 16:24:51 +0000
@@ -20,6 +20,8 @@
 import org.workcraft.plugins.serialisation.xml.DoubleSerialiser;
 import org.workcraft.plugins.serialisation.xml.EnumDeserialiser;
 import org.workcraft.plugins.serialisation.xml.EnumSerialiser;
+import org.workcraft.plugins.serialisation.xml.FileDeserialiser;
+import org.workcraft.plugins.serialisation.xml.FileSerialiser;
 import org.workcraft.plugins.serialisation.xml.IntDeserialiser;
 import org.workcraft.plugins.serialisation.xml.IntSerialiser;
 import org.workcraft.plugins.serialisation.xml.StringDeserialiser;
@@ -46,6 +48,7 @@
 		p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, BezierSerialiser.class);
 		p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, ConnectionSerialiser.class);
 		p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, VisualConnectionSerialiser.class);
+		p.registerClass(org.workcraft.serialisation.xml.XMLSerialiser.class, FileSerialiser.class);
 		
 		p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, AffineTransformDeserialiser.class);
 		p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, BooleanDeserialiser.class);
@@ -57,6 +60,7 @@
 		p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, BezierDeserialiser.class);
 		p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, ConnectionDeserialiser.class);
 		p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, VisualConnectionDeserialiser.class);
+		p.registerClass(org.workcraft.serialisation.xml.XMLDeserialiser.class, FileDeserialiser.class);
 	}
 
 	@Override
 
=== added file 'WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileDeserialiser.java'
--- WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileDeserialiser.java	1970-01-01 00:00:00 +0000
+++ WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileDeserialiser.java	2014-04-29 16:24:51 +0000
@@ -0,0 +1,19 @@
+package org.workcraft.plugins.serialisation.xml;
+
+import java.io.File;
+
+import org.w3c.dom.Element;
+import org.workcraft.exceptions.DeserialisationException;
+import org.workcraft.serialisation.xml.BasicXMLDeserialiser;
+
+public class FileDeserialiser implements BasicXMLDeserialiser{
+	
+	public String getClassName() {
+		return File.class.getName();
+	}
+
+	public Object deserialise(Element element) throws DeserialisationException {
+		return new File(element.getAttribute("path"));
+	}
+
+}
 
=== added file 'WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileSerialiser.java'
--- WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileSerialiser.java	1970-01-01 00:00:00 +0000
+++ WorkcraftCore/src/org/workcraft/plugins/serialisation/xml/FileSerialiser.java	2014-04-29 16:24:51 +0000
@@ -0,0 +1,22 @@
+package org.workcraft.plugins.serialisation.xml;
+
+import java.io.File;
+
+import org.w3c.dom.Element;
+import org.workcraft.exceptions.SerialisationException;
+import org.workcraft.serialisation.xml.BasicXMLSerialiser;
+
+public class FileSerialiser implements BasicXMLSerialiser {
+	
+	public String getClassName() {
+		return File.class.getName();
+	}
+
+	public void serialise(Element element, Object object)
+			throws SerialisationException {
+		if (object != null) {
+			element.setAttribute("path", ((File)object).getPath());
+		}
+	}
+
+}
 
=== modified file 'WorkcraftCore/src/org/workcraft/plugins/shared/CommonEditorSettings.java'
--- WorkcraftCore/src/org/workcraft/plugins/shared/CommonEditorSettings.java	2014-03-13 15:09:13 +0000
+++ WorkcraftCore/src/org/workcraft/plugins/shared/CommonEditorSettings.java	2014-04-29 16:24:51 +0000
@@ -31,12 +31,17 @@
 
 public class CommonEditorSettings implements SettingsPage {
 	private static LinkedList<PropertyDescriptor> properties;
-
+
+	private static final String backgroundColorKey = "CommonEditorSettings.backgroundColor";
+	private static final String showGridKey = "CommonEditorSettings.showGrid";
+	private static final String showRulersKey = "CommonEditorSettings.showRulers";
+	private static final String iconSizeKey = "CommonEditorSettings.iconSize";
+	private static final String debugClipboardKey = "CommonEditorSettings.debugClipboard";
+
 	protected static Color backgroundColor = Color.WHITE;
 	private static boolean showGrid = true;
 	private static boolean showRulers = true;
 	protected static int iconSize = 24;
-	
 	private static boolean debugClipboard = false; 
 
 	public String getSection() {
@@ -115,19 +120,19 @@
 	}
 
 	public void load(Config config) {
-		backgroundColor = config.getColor("CommonEditorSettings.backgroundColor", Color.WHITE);
-		showGrid = config.getBoolean("CommonEditorSettings.showGrid", true);
-		showRulers = config.getBoolean("CommonEditorSettings.showRullers", true);
-		iconSize = config.getInt("CommonEditorSettings.iconSize", 24);
-		debugClipboard = config.getBoolean("CommonEditorSettings.debugClipboard", false);
+		backgroundColor = config.getColor(backgroundColorKey, Color.WHITE);
+		showGrid = config.getBoolean(showGridKey, true);
+		showRulers = config.getBoolean(showRulersKey, true);
+		iconSize = config.getInt(iconSizeKey, 24);
+		debugClipboard = config.getBoolean(debugClipboardKey, false);
 	}
 
 	public void save(Config config) {
-		config.setColor("CommonEditorSettings.backgroundColor", backgroundColor);
-		config.setBoolean("CommonEditorSettings.showGrid", showGrid);
-		config.setBoolean("CommonEditorSettings.showRullers", showRulers);
-		config.setInt("CommonEditorSettings.iconSize", iconSize);
-		config.setBoolean("CommonEditorSettings.debugClipboard", debugClipboard);
+		config.setColor(backgroundColorKey, backgroundColor);
+		config.setBoolean(showGridKey, showGrid);
+		config.setBoolean(showRulersKey, showRulers);
+		config.setInt(iconSizeKey, iconSize);
+		config.setBoolean(debugClipboardKey, debugClipboard);
 	}
 	
 	public static Color getBackgroundColor() {