Merge lp:~danilovesky/workcraft/trunk-bug-1503646 into lp:workcraft

[Danil Sokolov]

[Danil Sokolov (danilovesky)]

review: Approve

=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/stg/CircuitStgUtils.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/stg/CircuitStgUtils.java	2015-08-03 12:45:13 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/stg/CircuitStgUtils.java	2015-10-13 11:40:49 +0000
@@ -2,24 +2,31 @@
 
 import java.io.File;
 import java.io.IOException;
+import java.util.Collection;
+import java.util.Set;
 
 import org.workcraft.Framework;
+import org.workcraft.PluginManager;
 import org.workcraft.exceptions.DeserialisationException;
 import org.workcraft.interop.Exporter;
 import org.workcraft.plugins.circuit.VisualCircuit;
+import org.workcraft.plugins.mpsat.tasks.MpsatChainResult;
 import org.workcraft.plugins.pcomp.tasks.PcompTask;
 import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode;
 import org.workcraft.plugins.shared.CommonDebugSettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.plugins.stg.STG;
+import org.workcraft.plugins.stg.SignalTransition.Type;
 import org.workcraft.plugins.stg.StgUtils;
 import org.workcraft.plugins.stg.VisualSTG;
 import org.workcraft.serialisation.Format;
+import org.workcraft.tasks.ProgressMonitor;
 import org.workcraft.tasks.Result;
-import org.workcraft.tasks.Result.Outcome;
+import org.workcraft.tasks.SubtaskMonitor;
 import org.workcraft.util.Export;
 import org.workcraft.util.Export.ExportTask;
 import org.workcraft.util.FileUtils;
+import org.workcraft.workspace.ModelEntry;
 import org.workcraft.workspace.WorkspaceEntry;
 
 public class CircuitStgUtils {
@@ -28,95 +35,141 @@
 		CircuitToStgConverter generator = new CircuitToStgConverter(circuit);
 		File envFile = circuit.getEnvironmentFile(); 
 		if ((envFile != null) && envFile.exists()) {
-			VisualSTG devStg = generator.getStg();
-			VisualSTG systemStg = composeDevStgWithEvnFile(devStg, envFile, circuit.getTitle());
+			STG devStg = (STG)generator.getStg().getMathModel();
+			STG systemStg = createSystemStg(devStg, envFile, circuit.getTitle());
 			if (systemStg != null) {
-				generator = new CircuitToStgConverter(circuit, systemStg);
+				generator = new CircuitToStgConverter(circuit, new VisualSTG(systemStg));
 			}
 		}
 		return generator;
 	}
 	
-	public static VisualSTG composeDevStgWithEvnFile(VisualSTG devStg, File envFile, String title) {
-		VisualSTG resultStg = null;
-		Framework framework = Framework.getInstance();
+	private static STG createSystemStg(STG devStg, File envFile, String title) {
+		STG systemStg = null;
 		String prefix = FileUtils.getTempPrefix(title);
 		File directory = FileUtils.createTempDirectory(prefix);
 		try {
 			File devStgFile = exportDevStg(devStg, directory);
 			File envStgFile = exportEnvStg(envFile, directory);
-			File stgFile = composeDevStgWithEnvStg(devStgFile, envStgFile, directory);
-			if (stgFile != null) {
-				WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true);
-				STG stg = (STG)stgWorkspaceEntry.getModelEntry().getMathModel();
-				resultStg = new VisualSTG(stg);
-				framework.getWorkspace().close(stgWorkspaceEntry);
+			File compStgFile = createComposedStg(devStgFile, envStgFile, directory);
+			if (compStgFile != null) {
+				systemStg = importStg(compStgFile);
+				Set<String> inputSignalNames = devStg.getSignalNames(Type.INPUT, null);
+				restoreInputSignals(systemStg, inputSignalNames);
 			}
 		} catch (Throwable e) {
 		} finally {
 			FileUtils.deleteFile(directory, CommonDebugSettings.getKeepTemporaryFiles());
 		}
-		return resultStg;
-	}
-
-	private static File composeDevStgWithEnvStg(File devStgFile, File envStgFile, File directory) throws IOException {
-		File stgFile = null;
-		Framework framework = Framework.getInstance();
-		if ((devStgFile != null) && (envStgFile != null)) {
-			// Generating .g for the whole system (circuit and environment)
-			stgFile = new File(directory, StgUtils.SYSTEM_FILE_NAME + StgUtils.ASTG_FILE_EXT);
-			PcompTask pcompTask = new PcompTask(new File[]{devStgFile, envStgFile}, 
-					ConversionMode.OUTPUT, true, false, directory);
-			
-			Result<? extends ExternalProcessResult>  pcompResult = framework.getTaskManager().execute(
-					pcompTask, "Running pcomp", null);
-
-			if (pcompResult.getOutcome() == Outcome.FINISHED) {
-				FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput()));
-			} else {
-				stgFile = null;
-			}
-		}
-		return stgFile;
+		return systemStg;
 	}
 
 	private static File exportEnvStg(File envFile, File directory) throws DeserialisationException, IOException {
-		Framework framework = Framework.getInstance();
 		File envStgFile = null;
 		if (envFile.getName().endsWith(StgUtils.ASTG_FILE_EXT)) {
 			envStgFile = envFile;
 		} else {
-			STG envStg = (STG)framework.loadFile(envFile).getMathModel();
-			Exporter envStgExporter = Export.chooseBestExporter(framework.getPluginManager(), envStg, Format.STG);
-			envStgFile = new File(directory, StgUtils.ENVIRONMENT_FILE_NAME + StgUtils.ASTG_FILE_EXT);
-			ExportTask envExportTask = new ExportTask(envStgExporter, envStg, envStgFile.getCanonicalPath());
-			Result<? extends Object> envExportResult = framework.getTaskManager().execute(
-					envExportTask, "Exporting environment .g", null);
-			if (envExportResult.getOutcome() != Outcome.FINISHED) {
-				envStgFile = null;
-			}
+			Framework framework = Framework.getInstance();
+			ModelEntry modelEntry = framework.loadFile(envFile);
+			STG envStg = (STG)modelEntry.getMathModel();
+			envStgFile = exportStg(envStg, StgUtils.ENVIRONMENT_FILE_NAME + StgUtils.ASTG_FILE_EXT, directory);
 		}
 		return envStgFile;
 	}
 
-	private static File exportDevStg(VisualSTG visualStg, File directory) throws IOException {
-		Framework framework = Framework.getInstance();
-
-		STG devStg = (STG)visualStg.getMathModel();
-		Exporter devStgExporter = Export.chooseBestExporter(framework.getPluginManager(), devStg, Format.STG);
-		if (devStgExporter == null) {
-			throw new RuntimeException("Exporter not available: model class " + devStg.getClass().getName() + " to .g format.");
-		}
-
-		File devStgFile =  new File(directory, StgUtils.DEVICE_FILE_NAME + StgUtils.ASTG_FILE_EXT);
-		ExportTask devExportTask = new ExportTask(devStgExporter, devStg, devStgFile.getCanonicalPath());
-		Result<? extends Object> devExportResult = framework.getTaskManager().execute(
-				devExportTask, "Exporting device .g", null);
-		if (devExportResult.getOutcome() != Outcome.FINISHED) {
-			devStgFile = null;
-		}
-		
-		return devStgFile;
+	private static File exportDevStg(STG devStg, File directory) throws IOException {
+		return exportStg(devStg, StgUtils.DEVICE_FILE_NAME + StgUtils.ASTG_FILE_EXT, directory);
+	}
+
+	private static File exportSytemStg(STG systemStg, File directory) throws IOException {
+		return exportStg(systemStg, StgUtils.SYSTEM_FILE_NAME + StgUtils.ASTG_FILE_EXT, directory);
+	}
+
+	private static File exportStg(STG stg, String fileName, File directory) throws IOException {
+		File stgFile = new File(directory, fileName);
+		Result<? extends Object> exportResult = exportStg(stg, stgFile, directory, null);
+		
+		switch (exportResult.getOutcome()) {
+		case FINISHED:
+			break;
+		case CANCELLED:
+			stgFile = null;
+			break;
+		case FAILED:
+			throw new RuntimeException("Export failed for file '" + fileName + "':\n" + exportResult.getCause());
+		}
+		return stgFile;
+	}
+
+	public static Result<? extends Object> exportStg(STG stg, File stgFile, File directory, 
+			ProgressMonitor<? super MpsatChainResult> monitor) throws IOException {
+		
+		Framework framework = Framework.getInstance();
+		PluginManager pluginManager = framework.getPluginManager();
+		Exporter stgExporter = Export.chooseBestExporter(pluginManager, stg, Format.STG);
+		if (stgExporter == null) {
+			throw new RuntimeException("Exporter not available: model class " + stg.getClass().getName() + " to .g format.");
+		}
+		
+		ExportTask exportTask = new ExportTask(stgExporter, stg, stgFile.getCanonicalPath());
+		String description = "Exporting " + stgFile.getAbsolutePath();
+		SubtaskMonitor<Object> subtaskMonitor = null;
+		if (monitor != null) {
+			subtaskMonitor = new SubtaskMonitor<Object>(monitor);
+		}
+		return framework.getTaskManager().execute(exportTask, description, subtaskMonitor);
+	}
+
+	private static File createComposedStg(File devStgFile, File envStgFile, File directory) throws IOException {
+		File compStgFile = null;
+		if ((devStgFile != null) && (envStgFile != null)) {
+			// Generating .g for the whole system (circuit and environment)
+			compStgFile = new File(directory, StgUtils.COMPOSITION_FILE_NAME + StgUtils.ASTG_FILE_EXT);
+			Result<? extends ExternalProcessResult> pcompResult = composeDevWithEnv(devStgFile, envStgFile, directory, null);
+
+			switch (pcompResult.getOutcome()) {
+			case FINISHED:
+				FileUtils.writeAllText(compStgFile, new String(pcompResult.getReturnValue().getOutput()));
+				break;
+			case CANCELLED:
+				compStgFile = null;
+				break;
+			case FAILED:
+				throw new RuntimeException("Composition failed:\n" + pcompResult.getCause());
+			}
+		}
+		return compStgFile;
+	}
+
+	public static Result<? extends ExternalProcessResult> composeDevWithEnv(File devStgFile, File envStgFile, File directory,
+			ProgressMonitor<? super MpsatChainResult> monitor) {
+		Framework framework = Framework.getInstance();
+		File[] inputFiles = new File[]{devStgFile, envStgFile};
+		PcompTask pcompTask = new PcompTask(inputFiles, ConversionMode.OUTPUT, true, false, directory);
+		String description = "Running pcomp";
+		SubtaskMonitor<Object> subtaskMonitor = null;
+		if (monitor != null) {
+			subtaskMonitor = new SubtaskMonitor<Object>(monitor);
+		}
+		return framework.getTaskManager().execute(pcompTask, description, subtaskMonitor);
+	}
+
+	public static STG importStg(File stgFile) {
+		STG stg = null;
+		try {
+			Framework framework = Framework.getInstance();
+			WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true);
+			stg = (STG)stgWorkspaceEntry.getModelEntry().getMathModel();
+			framework.getWorkspace().close(stgWorkspaceEntry);
+		} catch (DeserialisationException e) {
+		}
+		return stg;
+	}
+	
+	public static void restoreInputSignals(STG stg, Collection<String> inputSignalNames) {
+		for (String inputName: inputSignalNames) {
+			stg.setSignalType(inputName, Type.INPUT, null);
+		}
 	}
 
 }

=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/stg/CircuitToStgConverter.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/stg/CircuitToStgConverter.java	2015-09-25 14:43:34 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/stg/CircuitToStgConverter.java	2015-10-13 11:40:49 +0000
@@ -242,17 +242,10 @@
 		String signalName = CircuitUtils.getSignalName(circuit, signal);
 		SignalTransition.Type signalType = CircuitUtils.getSignalType(circuit, signal);
 		for(DnfClause clause : clauses) {	
-			VisualSignalTransition transition = stg.createSignalTransition(signalName, signalType, direction, container);
-			transition.setLabel(FormulaToString.toString(clause));
-			transitions.add(transition);
-			
-			try {
-				stg.connect(predPlace, transition);
-				stg.connect(transition, succPlace);
-			} catch (InvalidConnectionException e) {
-				throw new RuntimeException(e);
-			}
-			
+			// In self-looped signals the read-arcs will clash with producing/consuming arcs:
+			// 1) a read-arc from a preset place is redundant (is superseded by a consuming arc);
+			// 2) a read-arc from a postset place makes the transition dead.
+			boolean isDeadTransition = false;
 			HashSet<VisualPlace> placesToRead = new HashSet<VisualPlace>();
 			for (Literal literal : clause.getLiterals()) {
 				BooleanVariable variable = literal.getVariable();
@@ -263,23 +256,40 @@
 					throw new RuntimeException("No source for '" + circuit.getMathName(sourceContact) + "' while generating '" + signalName + "'.");
 				}
 				VisualPlace place = literal.getNegation() ? sourceDriverStg.zero : sourceDriverStg.one;
-				placesToRead.add(place);
-			}
-			
-			if (placesToRead.remove(predPlace)) {
-				System.out.println("Warning: signal '" + signalName + "' depends on itself.");
-			}
-			
-			for (VisualPlace place : placesToRead) {
+				if (place != predPlace) {
+					// 1) a read-arc from a preset place is redundant (is superseded by a consuming arc);
+					placesToRead.add(place);
+				}
+				
+				if (place == succPlace) {
+					// 2) a read-arc from a postset place makes the transition dead.
+					isDeadTransition = true;
+				}
+			}
+			
+			if ( !isDeadTransition ) {
+				VisualSignalTransition transition = stg.createSignalTransition(signalName, signalType, direction, container);
+				transition.setLabel(FormulaToString.toString(clause));
+				transitions.add(transition);
+				// Create read-arcs.
+				for (VisualPlace place : placesToRead) {
+					try {
+						stg.connectUndirected(place, transition);
+					} catch (InvalidConnectionException e) {
+						throw new RuntimeException(e);
+					}
+				}
+				// Create producing/consuming arcs.
 				try {
-					stg.connectUndirected(place, transition);
+					stg.connect(predPlace, transition);
+					stg.connect(transition, succPlace);
 				} catch (InvalidConnectionException e) {
 					throw new RuntimeException(e);
 				}
 			}
 		}
 	}
-	
+
 
 	private TwoWayMap<VisualContact, SignalStg> associateDriversToStgs(HashSet<VisualContact> drivers) {
 		TwoWayMap<VisualContact, SignalStg> result = new TwoWayMap<>();

=== modified file 'CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java'
--- CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java	2015-08-03 12:45:13 +0000
+++ CircuitPlugin/src/org/workcraft/plugins/circuit/tasks/CheckCircuitTask.java	2015-10-13 11:40:49 +0000
@@ -10,8 +10,8 @@
 import java.util.Set;
 
 import org.workcraft.Framework;
-import org.workcraft.interop.Exporter;
 import org.workcraft.plugins.circuit.VisualCircuit;
+import org.workcraft.plugins.circuit.stg.CircuitStgUtils;
 import org.workcraft.plugins.circuit.stg.CircuitToStgConverter;
 import org.workcraft.plugins.mpsat.MpsatMode;
 import org.workcraft.plugins.mpsat.MpsatResultParser;
@@ -21,20 +21,15 @@
 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.tasks.PcompTask;
-import org.workcraft.plugins.pcomp.tasks.PcompTask.ConversionMode;
 import org.workcraft.plugins.shared.CommonDebugSettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.plugins.stg.STG;
 import org.workcraft.plugins.stg.SignalTransition.Type;
 import org.workcraft.plugins.stg.StgUtils;
-import org.workcraft.serialisation.Format;
 import org.workcraft.tasks.ProgressMonitor;
 import org.workcraft.tasks.Result;
 import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.tasks.SubtaskMonitor;
-import org.workcraft.util.Export;
-import org.workcraft.util.Export.ExportTask;
 import org.workcraft.util.FileUtils;
 import org.workcraft.workspace.WorkspaceEntry;
 
@@ -83,20 +78,9 @@
 
 			CircuitToStgConverter generator = new CircuitToStgConverter(visualCircuit);
 			STG devStg = (STG)generator.getStg().getMathModel();
-			Exporter devStgExporter = Export.chooseBestExporter(framework.getPluginManager(), devStg, Format.STG);
-			if (devStgExporter == null) {
-				throw new RuntimeException("Exporter not available: model class " + devStg.getClass().getName() + " to .g format.");
-			}
-			SubtaskMonitor<Object> subtaskMonitor = new SubtaskMonitor<Object>(monitor);
-			monitor.progressUpdate(0.10);
-
-			// Generating .g for the circuit
 			String devStgName = (hasEnvironment ? StgUtils.DEVICE_FILE_NAME : StgUtils.SYSTEM_FILE_NAME) + StgUtils.ASTG_FILE_EXT;
 			File devStgFile =  new File(directory, devStgName);
-			ExportTask devExportTask = new ExportTask(devStgExporter, devStg, devStgFile.getCanonicalPath());
-			Result<? extends Object> devExportResult = framework.getTaskManager().execute(
-					devExportTask, "Exporting circuit .g", subtaskMonitor);
-			
+			Result<? extends Object> devExportResult = CircuitStgUtils.exportStg(devStg, devStgFile, directory, monitor);
 			if (devExportResult.getOutcome() != Outcome.FINISHED) {
 				if (devExportResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
@@ -104,27 +88,23 @@
 				return new Result<MpsatChainResult>(Outcome.FAILED, 
 						new MpsatChainResult(devExportResult, null, null, null, toolchainPreparationSettings));
 			}
-			monitor.progressUpdate(0.20);
+			monitor.progressUpdate(0.10);
 			
 			// Generating .g for the environment
-			STG stg;
-			File stgFile = null;
+			STG sysStg;
+			File sysStgFile = null;
 			Result<? extends ExternalProcessResult>  pcompResult = null;
 			if ( !hasEnvironment ) {
-				 stgFile = devStgFile;
-				 stg = devStg;
+				 sysStgFile = devStgFile;
+				 sysStg = devStg;
 			} else {
 				File envStgFile = null;
 				if (envFile.getName().endsWith(StgUtils.ASTG_FILE_EXT)) {
 					envStgFile = envFile;
 				} else {
 					STG envStg = (STG)framework.loadFile(envFile).getMathModel();
-					Exporter envStgExporter = Export.chooseBestExporter(framework.getPluginManager(), envStg, Format.STG);
 					envStgFile = new File(directory, StgUtils.ENVIRONMENT_FILE_NAME + StgUtils.ASTG_FILE_EXT);
-					ExportTask envExportTask = new ExportTask(envStgExporter, envStg, envStgFile.getCanonicalPath());
-					Result<? extends Object> envExportResult = framework.getTaskManager().execute(
-							envExportTask, "Exporting environment .g", subtaskMonitor);
-					
+					Result<? extends Object> envExportResult = CircuitStgUtils.exportStg(envStg, envStgFile, directory, monitor);
 					if (envExportResult.getOutcome() != Outcome.FINISHED) {
 						if (envExportResult.getOutcome() == Outcome.CANCELLED) {
 							return new Result<MpsatChainResult>(Outcome.CANCELLED);
@@ -133,14 +113,10 @@
 								new MpsatChainResult(envExportResult, null, null, null, toolchainPreparationSettings));
 					}
 				}
-				monitor.progressUpdate(0.25);
+				monitor.progressUpdate(0.20);
 
 				// Generating .g for the whole system (circuit and environment)
-				stgFile = new File(directory, StgUtils.SYSTEM_FILE_NAME + StgUtils.ASTG_FILE_EXT);
-				PcompTask pcompTask = new PcompTask(new File[]{devStgFile, envStgFile}, ConversionMode.OUTPUT, true, false, directory);
-				pcompResult = framework.getTaskManager().execute(
-						pcompTask, "Running pcomp", subtaskMonitor);
-				
+				pcompResult = CircuitStgUtils.composeDevWithEnv(devStgFile, envStgFile, directory, monitor);
 				if (pcompResult.getOutcome() != Outcome.FINISHED) {
 					if (pcompResult.getOutcome() == Outcome.CANCELLED) {
 						return new Result<MpsatChainResult>(Outcome.CANCELLED);
@@ -148,18 +124,32 @@
 					return new Result<MpsatChainResult>(Outcome.FAILED, 
 							new MpsatChainResult(devExportResult, pcompResult, null, null, toolchainPreparationSettings));
 				}
-				FileUtils.writeAllText(stgFile, new String(pcompResult.getReturnValue().getOutput()));
-				WorkspaceEntry stgWorkspaceEntry = framework.getWorkspace().open(stgFile, true);
-				stg = (STG)stgWorkspaceEntry.getModelEntry().getMathModel();
-				framework.getWorkspace().close(stgWorkspaceEntry);
+				File compStgFile = new File(directory, StgUtils.COMPOSITION_FILE_NAME + StgUtils.ASTG_FILE_EXT);
+				FileUtils.writeAllText(compStgFile, new String(pcompResult.getReturnValue().getOutput()));
+				monitor.progressUpdate(0.25);
+
+				// Restore input signals of the composed STG (these can be converted to outputs by PComp)
+				sysStg = CircuitStgUtils.importStg(compStgFile);
+				Set<String> inputSignalNames = devStg.getSignalNames(Type.INPUT, null);
+				CircuitStgUtils.restoreInputSignals(sysStg, inputSignalNames);
+				sysStgFile = new File(directory, StgUtils.SYSTEM_FILE_NAME + StgUtils.ASTG_FILE_EXT);
+				Result<? extends Object> sysExportResult = CircuitStgUtils.exportStg(sysStg, sysStgFile, directory, monitor);
+				if (sysExportResult.getOutcome() != Outcome.FINISHED) {
+					if (sysExportResult.getOutcome() == Outcome.CANCELLED) {
+						return new Result<MpsatChainResult>(Outcome.CANCELLED);
+					}
+					return new Result<MpsatChainResult>(Outcome.FAILED, 
+							new MpsatChainResult(sysExportResult, null, null, null, toolchainPreparationSettings));
+				}
 			}		
 			monitor.progressUpdate(0.30);
 
 			// Generate unfolding
 			File unfoldingFile = new File(directory, StgUtils.SYSTEM_FILE_NAME + MpsatUtilitySettings.getUnfoldingExtension(true));
-			PunfTask punfTask = new PunfTask(stgFile.getCanonicalPath(), unfoldingFile.getCanonicalPath(), true);
+			PunfTask punfTask = new PunfTask(sysStgFile.getCanonicalPath(), unfoldingFile.getCanonicalPath(), true);
+			SubtaskMonitor<Object> punfMonitor = new SubtaskMonitor<Object>(monitor);
 			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
-					punfTask, "Unfolding .g", subtaskMonitor);
+					punfTask, "Unfolding .g", punfMonitor);
 			
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
@@ -174,8 +164,7 @@
 			if (hasEnvironment && checkConformation) {
 				Set<String> devOutputNames = devStg.getSignalFlatNames(Type.OUTPUT);
 				Set<String> devPlaceNames = parsePlaceNames(pcompResult.getReturnValue().getOutputFile("places.list"), 0);
-//				String reachConformation = MpsatSettings.genReachConformation(devOutputNames, devPlaceNames);
-				String reachConformation = MpsatSettings.genReachConformationDetail(stg, devOutputNames, devPlaceNames);
+				String reachConformation = MpsatSettings.genReachConformationDetail(sysStg, devOutputNames, devPlaceNames);
 				if (MpsatUtilitySettings.getDebugReach()) {
 					System.out.println("\nReach expression for the interface conformation property:");
 					System.out.println(reachConformation);
@@ -184,10 +173,11 @@
 						MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), 
 						MpsatUtilitySettings.getSolutionCount(), reachConformation, true);
 				
-				MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), 
+				MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(directory), 
 						unfoldingFile.getCanonicalPath(), directory, true);
+				SubtaskMonitor<Object> mpsatMonitor = new SubtaskMonitor<Object>(monitor);
 				Result<? extends ExternalProcessResult>  mpsatConformationResult = framework.getTaskManager().execute(
-						mpsatConformationTask, "Running conformation check [MPSat]", subtaskMonitor);
+						mpsatConformationTask, "Running conformation check [MPSat]", mpsatMonitor);
 
 				if (mpsatConformationResult.getOutcome() != Outcome.FINISHED) {
 					if (mpsatConformationResult.getOutcome() == Outcome.CANCELLED) {
@@ -209,10 +199,11 @@
 			
 			// Check for deadlock
 			if (checkDeadlock) {
-				MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(), 
+				MpsatTask mpsatDeadlockTask = new MpsatTask(deadlockSettings.getMpsatArguments(directory), 
 						unfoldingFile.getCanonicalPath(), directory, true);
+				SubtaskMonitor<Object> mpsatMonitor = new SubtaskMonitor<Object>(monitor);
 				Result<? extends ExternalProcessResult> mpsatDeadlockResult = framework.getTaskManager().execute(
-						mpsatDeadlockTask, "Running deadlock check [MPSat]", subtaskMonitor);
+						mpsatDeadlockTask, "Running deadlock check [MPSat]", mpsatMonitor);
 			
 				if (mpsatDeadlockResult.getOutcome() != Outcome.FINISHED) {
 					if (mpsatDeadlockResult.getOutcome() == Outcome.CANCELLED) {
@@ -234,14 +225,15 @@
 			
 			// Check for hazards
 			if (checkHazard) {
-				MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(), 
+				MpsatTask mpsatHazardTask = new MpsatTask(hazardSettings.getMpsatArguments(directory), 
 						unfoldingFile.getCanonicalPath(), directory, true);
 				if (MpsatUtilitySettings.getDebugReach()) {
 					System.out.println("\nReach expression for the hazard property:");
 					System.out.println(hazardSettings.getReach());
 				}
+				SubtaskMonitor<Object> mpsatMonitor = new SubtaskMonitor<Object>(monitor);
 				Result<? extends ExternalProcessResult>  mpsatHazardResult = framework.getTaskManager().execute(
-						mpsatHazardTask, "Running hazard check [MPSat]", subtaskMonitor);
+						mpsatHazardTask, "Running hazard check [MPSat]", mpsatMonitor);
 
 				if (mpsatHazardResult.getOutcome() != Outcome.FINISHED) {
 					if (mpsatHazardResult.getOutcome() == Outcome.CANCELLED) {

=== modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java'
--- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java	2015-09-25 14:43:34 +0000
+++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowDeadlockTask.java	2015-10-13 11:40:49 +0000
@@ -14,6 +14,7 @@
 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.CommonDebugSettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.plugins.stg.STGModel;
 import org.workcraft.serialisation.Format;
@@ -23,6 +24,7 @@
 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;
 
 
@@ -41,7 +43,11 @@
 	@Override
 	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
 		final Framework framework = Framework.getInstance();
+		File directory = null;
 		try {
+			String prefix = FileUtils.getTempPrefix(we.getTitle());
+			directory = FileUtils.createTempDirectory(prefix);
+			
 			StgGenerator generator = new StgGenerator((VisualDfs)we.getModelEntry().getVisualModel());
 			STGModel model = (STGModel)generator.getStgModel().getMathModel(); 
 			Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG);
@@ -50,14 +56,13 @@
 			}
 			monitor.progressUpdate(0.10);
 			
-			File netFile = File.createTempFile("net", exporter.getExtenstion());
+			File netFile = new File(directory, "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);
 				}
@@ -66,14 +71,12 @@
 			}
 			monitor.progressUpdate(0.20);
 			
-			File unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension(true));
+			File unfoldingFile = new File(directory, "unfolding" + MpsatUtilitySettings.getUnfoldingExtension(true));
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), unfoldingFile.getCanonicalPath(), true);
 			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
 					punfTask, "Unfolding .g", mon);
 			
-			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				unfoldingFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
@@ -82,7 +85,8 @@
 			}
 			monitor.progressUpdate(0.70);
 
-			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), unfoldingFile.getCanonicalPath(), null, true);
+			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(directory), 
+					unfoldingFile.getCanonicalPath(), directory, true);
 			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
 					mpsatTask, "Running deadlock checking [MPSat]", mon);
 			
@@ -98,18 +102,18 @@
 			
 			MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue());
 			if (!mdp.getSolutions().isEmpty()) {
-				unfoldingFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
 						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow has a deadlock"));
 			}
 			monitor.progressUpdate(1.0);
 
-			unfoldingFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
 					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow is deadlock-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
+		} finally {
+			FileUtils.deleteFile(directory, CommonDebugSettings.getKeepTemporaryFiles());
 		}
 	}
 

=== modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java'
--- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java	2015-09-25 14:43:34 +0000
+++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowHazardTask.java	2015-10-13 11:40:49 +0000
@@ -14,6 +14,7 @@
 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.CommonDebugSettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.plugins.stg.STGModel;
 import org.workcraft.serialisation.Format;
@@ -23,6 +24,7 @@
 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;
 
 
@@ -41,7 +43,11 @@
 	@Override
 	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
 		final Framework framework = Framework.getInstance();
+		File directory = null;
 		try {
+			String prefix = FileUtils.getTempPrefix(we.getTitle());
+			directory = FileUtils.createTempDirectory(prefix);
+			
 			StgGenerator generator = new StgGenerator((VisualDfs)we.getModelEntry().getVisualModel());
 			STGModel model = (STGModel)generator.getStgModel().getMathModel(); 
 			Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG);
@@ -50,14 +56,13 @@
 			}
 			monitor.progressUpdate(0.10);
 			
-			File netFile = File.createTempFile("net", exporter.getExtenstion());
+			File netFile = new File(directory, "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);
 				}
@@ -66,14 +71,12 @@
 			}
 			monitor.progressUpdate(0.20);
 			
-			File unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension(true));
+			File unfoldingFile = new File(directory, "unfolding" + MpsatUtilitySettings.getUnfoldingExtension(true));
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), unfoldingFile.getCanonicalPath(), true);
 			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
 					punfTask, "Unfolding .g", mon);
 			
-			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				unfoldingFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
@@ -82,7 +85,8 @@
 			}
 			monitor.progressUpdate(0.40);
 
-			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), unfoldingFile.getCanonicalPath(), null, true);
+			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(directory), 
+					unfoldingFile.getCanonicalPath(), directory, true);
 			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
 					mpsatTask, "Running semimodularity checking [MPSat]", mon);
 			
@@ -97,18 +101,18 @@
 			
 			MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue());
 			if (!mdp.getSolutions().isEmpty()) {
-				unfoldingFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
 						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow has hazard(s)"));
 			}
 			monitor.progressUpdate(1.0);
 
-			unfoldingFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
 					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Dataflow is hazard-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
+		} finally {
+			FileUtils.deleteFile(directory, CommonDebugSettings.getKeepTemporaryFiles());
 		}
 	}
 

=== modified file 'DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java'
--- DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java	2015-09-25 14:43:34 +0000
+++ DfsPlugin/src/org/workcraft/plugins/dfs/tasks/CheckDataflowTask.java	2015-10-13 11:40:49 +0000
@@ -14,6 +14,7 @@
 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.CommonDebugSettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.plugins.stg.STGModel;
 import org.workcraft.serialisation.Format;
@@ -22,6 +23,7 @@
 import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.tasks.SubtaskMonitor;
 import org.workcraft.util.Export;
+import org.workcraft.util.FileUtils;
 import org.workcraft.util.Export.ExportTask;
 import org.workcraft.workspace.WorkspaceEntry;
 
@@ -46,7 +48,11 @@
 	@Override
 	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
 		final Framework framework = Framework.getInstance();
+		File directory = null;
 		try {
+			String prefix = FileUtils.getTempPrefix(we.getTitle());
+			directory = FileUtils.createTempDirectory(prefix);
+
 			StgGenerator generator = new StgGenerator((VisualDfs)we.getModelEntry().getVisualModel());
 			STGModel model = (STGModel)generator.getStgModel().getMathModel(); 
 			Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG);
@@ -55,14 +61,13 @@
 			}
 			monitor.progressUpdate(0.10);
 			
-			File netFile = File.createTempFile("net", exporter.getExtenstion());
+			File netFile = new File(directory, "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);
 				}
@@ -71,14 +76,12 @@
 			}
 			monitor.progressUpdate(0.20);
 			
-			File unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension(true));
+			File unfoldingFile = new File(directory, "unfolding" + MpsatUtilitySettings.getUnfoldingExtension(true));
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), unfoldingFile.getCanonicalPath(), true);
 			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
 					punfTask, "Unfolding .g", mon);
 			
-			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				unfoldingFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
@@ -87,7 +90,8 @@
 			}
 			monitor.progressUpdate(0.40);
 
-			MpsatTask mpsatTask = new MpsatTask(deadlockSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath(), null, true);
+			MpsatTask mpsatTask = new MpsatTask(deadlockSettings.getMpsatArguments(directory), 
+					unfoldingFile.getCanonicalPath(), directory, true);
 			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
 					mpsatTask, "Running deadlock checking [MPSat]", mon);
 			
@@ -102,13 +106,13 @@
 			
 			MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue());
 			if (!mdp.getSolutions().isEmpty()) {
-				unfoldingFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
 						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, deadlockSettings, "Dataflow has a deadlock"));
 			}
 			monitor.progressUpdate(0.70);
 
-			mpsatTask = new MpsatTask(hazardSettings.getMpsatArguments(), unfoldingFile.getCanonicalPath(), null, true);
+			mpsatTask = new MpsatTask(hazardSettings.getMpsatArguments(directory), 
+					unfoldingFile.getCanonicalPath(), directory, true);
 			mpsatResult = framework.getTaskManager().execute(mpsatTask, "Running semimodularity checking [MPSat]", mon);
 			if (mpsatResult.getOutcome() != Outcome.FINISHED) {
 				if (mpsatResult.getOutcome() == Outcome.CANCELLED) {
@@ -121,18 +125,18 @@
 			
 			mdp = new MpsatResultParser(mpsatResult.getReturnValue());
 			if (!mdp.getSolutions().isEmpty()) {
-				unfoldingFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
 						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings, "Dataflow has hazard(s)"));
 			}
 			monitor.progressUpdate(1.0);
 
-			unfoldingFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
 					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, hazardSettings, "Dataflow is deadlock-free and hazard-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
+		} finally {
+			FileUtils.deleteFile(directory, CommonDebugSettings.getKeepTemporaryFiles());
 		}
 	}
 

=== modified file 'FstPlugin/src/org/workcraft/plugins/fst/task/WriteSgConversionTask.java'
--- FstPlugin/src/org/workcraft/plugins/fst/task/WriteSgConversionTask.java	2015-07-22 17:40:16 +0000
+++ FstPlugin/src/org/workcraft/plugins/fst/task/WriteSgConversionTask.java	2015-10-13 11:40:49 +0000
@@ -27,6 +27,7 @@
 import org.workcraft.tasks.Task;
 import org.workcraft.util.Export;
 import org.workcraft.util.Export.ExportTask;
+import org.workcraft.util.FileUtils;
 import org.workcraft.workspace.WorkspaceEntry;
 
 
@@ -139,9 +140,7 @@
 		} catch (Throwable e) {
 			return new Result<WriteSgConversionResult>(e);
 		} finally {
-			if ((pnFile != null) && !CommonDebugSettings.getKeepTemporaryFiles() ) {
-				pnFile.delete();
-			}
+			FileUtils.deleteFile(pnFile, CommonDebugSettings.getKeepTemporaryFiles());
 		}
 	}
 

=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java	2015-09-29 15:26:23 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/MpsatSettings.java	2015-10-13 11:40:49 +0000
@@ -244,7 +244,7 @@
 		return inversePredicate;
 	}
 
-	public String[] getMpsatArguments() {
+	public String[] getMpsatArguments(File workingDirectory) {
 		ArrayList<String> args = new ArrayList<String>();
 		for (String option: getMode().getArgument().split("\\s")) {
 			args.add(option);
@@ -252,12 +252,16 @@
 		
 		if (getMode().hasReach()) {
 			try {
-				File reachFile = File.createTempFile("reach", null);
-				reachFile.deleteOnExit();
-//				FileUtils.dumpString(reach, getFlatReach());
+				File reachFile = null;
+				if (workingDirectory == null) {
+					reachFile = File.createTempFile("reach", ".txt");
+					reachFile.deleteOnExit();
+				} else {
+					reachFile = new File(workingDirectory, "reach.txt");
+				}
 				FileUtils.dumpString(reachFile, getReach());
 				args.add("-d");
-				args.add("@"+reachFile.getCanonicalPath());
+				args.add("@" + reachFile.getCanonicalPath());
 			} catch (IOException e) {
 				throw new RuntimeException(e);
 			}

=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java	2015-10-08 16:41:22 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatChainTask.java	2015-10-13 11:40:49 +0000
@@ -77,7 +77,7 @@
 			monitor.progressUpdate(0.66);
 
 			// Run MPSat on the generated unfolding
-			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), 
+			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(directory), 
 					unfoldingFile.getCanonicalPath(), directory, tryPnml);
 			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
 					mpsatTask, "Running mpsat model-checking", subtaskMonitor);

=== modified file 'MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java	2015-10-08 16:41:22 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/mpsat/tasks/MpsatConformationTask.java	2015-10-13 11:40:49 +0000
@@ -151,7 +151,7 @@
 					MpsatMode.STG_REACHABILITY, 0, MpsatUtilitySettings.getSolutionMode(), 
 					MpsatUtilitySettings.getSolutionCount(), reachConformation, true);
 			
-			MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(), 
+			MpsatTask mpsatConformationTask = new MpsatTask(conformationSettings.getMpsatArguments(directory), 
 					unfoldingFile.getCanonicalPath(), directory, true);
 			Result<? extends ExternalProcessResult>  mpsatConformationResult = framework.getTaskManager().execute(
 					mpsatConformationTask, "Running conformation check [MPSat]", subtaskMonitor);

=== modified file 'MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java'
--- MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java	2015-08-03 12:45:13 +0000
+++ MpsatPlugin/src/org/workcraft/plugins/pcomp/tasks/PcompTask.java	2015-10-13 11:40:49 +0000
@@ -67,6 +67,7 @@
 		try {
 			if (directory == null) {
 				listFile = File.createTempFile("places_", ".list");
+				listFile.deleteOnExit();
 			} else {
 				listFile = new File(directory, "places.list");
 			}

=== modified file 'PetrifyPlugin/src/org/workcraft/plugins/petrify/PetrifyModule.java'
--- PetrifyPlugin/src/org/workcraft/plugins/petrify/PetrifyModule.java	2015-04-17 14:54:25 +0000
+++ PetrifyPlugin/src/org/workcraft/plugins/petrify/PetrifyModule.java	2015-10-13 11:40:49 +0000
@@ -14,6 +14,8 @@
 import org.workcraft.plugins.petrify.tools.PetrifySynthesisGeneralisedCelement;
 import org.workcraft.plugins.petrify.tools.PetrifySynthesisTechnologyMapping;
 import org.workcraft.plugins.petrify.tools.PetrifyUntoggle;
+import org.workcraft.plugins.petrify.tools.ShowSg;
+import org.workcraft.plugins.petrify.tools.ShowSgBinary;
 
 public class PetrifyModule implements Module {
 
@@ -33,7 +35,8 @@
 		pm.registerClass(Tool.class, PetrifyDummyContraction.class);
 		pm.registerClass(Tool.class, PetrifyNetSynthesis.class);
 		pm.registerClass(Tool.class, PetrifyNetSynthesisWithEr.class);
-//		pm.registerClass(Tool.class, ShowSg.class);
+		pm.registerClass(Tool.class, ShowSg.class);
+		pm.registerClass(Tool.class, ShowSgBinary.class);
 	}
 
 	@Override

=== modified file 'PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/DrawAstgTask.java'
--- PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/DrawAstgTask.java	2015-08-03 12:45:13 +0000
+++ PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/DrawAstgTask.java	2015-10-13 11:40:49 +0000
@@ -28,12 +28,15 @@
 		ArrayList<String> command = new ArrayList<String>();
 		command.add(PetrifyUtilitySettings.getDrawAstgCommand());
 		
-		for (String arg : PetrifyUtilitySettings.getDrawAstgArgs().split(" "))
-			if (!arg.isEmpty())
+		for (String arg : PetrifyUtilitySettings.getDrawAstgArgs().split(" ")) {
+			if (!arg.isEmpty()) {
 				command.add(arg);
+			}
+		}
 		
-		for (String arg : options)
+		for (String arg : options) {
 			command.add(arg);
+		}
 		
 		command.add(inputPath);
 		command.add("-o");

=== modified file 'PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/DrawSgTask.java'
--- PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/DrawSgTask.java	2014-12-28 22:42:47 +0000
+++ PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/DrawSgTask.java	2015-10-13 11:40:49 +0000
@@ -11,6 +11,8 @@
 
 import org.workcraft.Framework;
 import org.workcraft.dom.Model;
+import org.workcraft.plugins.petri.PetriNetModel;
+import org.workcraft.plugins.shared.CommonDebugSettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.serialisation.Format;
 import org.workcraft.tasks.ProgressMonitor;
@@ -19,6 +21,9 @@
 import org.workcraft.tasks.Task;
 import org.workcraft.util.Export;
 import org.workcraft.util.Export.ExportTask;
+import org.workcraft.util.FileUtils;
+import org.workcraft.util.WorkspaceUtils;
+import org.workcraft.workspace.WorkspaceEntry;
 
 public class DrawSgTask implements Task<DrawSgResult> {
 	
@@ -46,20 +51,26 @@
 		}
 	}
 
-	final Pattern hugeSgPattern = Pattern.compile("with ([0-9]+) states"); 
-	private final Model model;
+	final Pattern hugeSgPattern = Pattern.compile("with ([0-9]+) states");
+	
+	private final WorkspaceEntry we;
+	private boolean binary;
 
-	public DrawSgTask(Model model) {
-		this.model = model;
+	public DrawSgTask(WorkspaceEntry we, boolean binary) {
+		this.we = we;
+		this.binary = binary;
 	}
 
 	@Override
 	public Result<? extends DrawSgResult> run(ProgressMonitor<? super DrawSgResult> monitor) {
 		final Framework framework = Framework.getInstance();
-		try	{
-			File dotG = File.createTempFile("workcraft", ".g");
-			dotG.deleteOnExit();
+		File directory = null;
+		try {
+			String prefix = FileUtils.getTempPrefix(we.getTitle());
+			directory = FileUtils.createTempDirectory(prefix);
 
+			File dotG = new File(directory, "model.g");
+			Model model = WorkspaceUtils.getAs(we, PetriNetModel.class);
 			ExportTask exportTask = Export.createExportTask(model, dotG, Format.STG, framework.getPluginManager());
 			final Result<? extends Object> dotGResult = framework.getTaskManager().execute(exportTask, "Exporting to .g" );
 
@@ -74,10 +85,11 @@
 				return Result.cancelled();
 			}
 
-			File sg = File.createTempFile("workcraft", ".g");
-			sg.deleteOnExit();
-
+			File sg = new File(directory, "model.sg");
 			List<String> writeSgOptions = new ArrayList<String>();
+			if (binary) {
+				writeSgOptions.add("-bin");
+			}
 			while (true) {
 				WriteSgTask writeSgTask = new WriteSgTask(dotG.getAbsolutePath(), sg.getAbsolutePath(), writeSgOptions);
 				Result<? extends ExternalProcessResult> writeSgResult = framework.getTaskManager().execute(
@@ -108,10 +120,12 @@
 					}
 				}
 			}
-			File ps = File.createTempFile("workcraft", ".ps");
-			ps.deleteOnExit();
-
-			DrawAstgTask drawAstgTask = new DrawAstgTask(sg.getAbsolutePath(), ps.getAbsolutePath(), new ArrayList<String>());
+			File ps = new File(directory, "model.ps");
+			ArrayList<String> drawAstgOptions = new ArrayList<String>();
+			if (binary) {
+				drawAstgOptions.add("-bin");
+			}
+			DrawAstgTask drawAstgTask = new DrawAstgTask(sg.getAbsolutePath(), ps.getAbsolutePath(), drawAstgOptions);
 			final Result<? extends ExternalProcessResult> drawAstgResult = framework.getTaskManager().execute(drawAstgTask, "Running draw_astg");
 
 			if (drawAstgResult.getOutcome() != Outcome.FINISHED) {
@@ -125,13 +139,11 @@
 				}
 				return Result.cancelled();
 			}
-
-			dotG.delete();
-			sg.delete();
 			return Result.finished(new DrawSgResult(ps, "No errors"));
 		} catch (Throwable e) {
-			e.printStackTrace();
 			return Result.exception(e);
+		} finally {
+			FileUtils.deleteFile(directory, CommonDebugSettings.getKeepTemporaryFiles());
 		}
 	}
 	

=== modified file 'PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/TransformationTask.java'
--- PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/TransformationTask.java	2015-07-22 17:40:16 +0000
+++ PetrifyPlugin/src/org/workcraft/plugins/petrify/tasks/TransformationTask.java	2015-10-13 11:40:49 +0000
@@ -20,6 +20,7 @@
 import org.workcraft.tasks.Task;
 import org.workcraft.util.Export;
 import org.workcraft.util.Export.ExportTask;
+import org.workcraft.util.FileUtils;
 import org.workcraft.workspace.WorkspaceEntry;
 
 public class TransformationTask implements Task<TransformationResult>{
@@ -91,9 +92,7 @@
 		} catch (Throwable e) {
 			return Result.exception(e);
 		} finally {
-			if ((modelFile != null) && !CommonDebugSettings.getKeepTemporaryFiles() ) {
-				modelFile.delete();
-			}
+			FileUtils.deleteFile(modelFile, CommonDebugSettings.getKeepTemporaryFiles());
 		}
 	}
 	

=== modified file 'PetrifyPlugin/src/org/workcraft/plugins/petrify/tools/ShowSg.java'
--- PetrifyPlugin/src/org/workcraft/plugins/petrify/tools/ShowSg.java	2014-12-27 22:40:44 +0000
+++ PetrifyPlugin/src/org/workcraft/plugins/petrify/tools/ShowSg.java	2015-10-13 11:40:49 +0000
@@ -24,19 +24,24 @@
 
 	@Override
 	public String getSection() {
-		return "State graph";
+		return "External visualiser";
 	}
 
 	@Override
 	public String getDisplayName() {
-		return "Show state graph [Petrify]";
+		return "Basic state graph [write_sg + draw_astg]";
+	}
+	
+	public boolean isBinaryEncodded() {
+		return false;
 	}
 
 	@Override
 	public void run(WorkspaceEntry we) {
-		DrawSgTask task = new DrawSgTask(WorkspaceUtils.getAs(we, PetriNetModel.class));
+		DrawSgTask task = new DrawSgTask(we, isBinaryEncodded());
 		final Framework framework = Framework.getInstance();
-		framework.getTaskManager().queue(task, "Show state graph", new ProgressMonitor<DrawSgResult>() {
+		
+		ProgressMonitor<DrawSgResult> monitor = new ProgressMonitor<DrawSgResult>() {
 			@Override
 			public void progressUpdate(double completion) {
 			}
@@ -56,28 +61,28 @@
 
 			@Override
 			public void finished(Result<? extends DrawSgResult> result, String description) {
-				
 				if (result.getOutcome() == Outcome.FINISHED) {
 					SystemOpen.open(result.getReturnValue().getPsFile());
 				} else  if (result.getOutcome() != Outcome.CANCELLED) {
-						String errorMessage = "Petrify tool chain execution failed :-(";
-						Throwable cause = result.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: \n" + result.getReturnValue().getErrorMessages();
+					String errorMessage = "Petrify tool chain execution failed :-(";
+					Throwable cause = result.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: \n" + result.getReturnValue().getErrorMessages();
+					}
+					final String err = errorMessage;
+					SwingUtilities.invokeLater(new Runnable() {
+						@Override
+						public void run() {
+							JOptionPane.showMessageDialog(null, err, "Oops..", JOptionPane.ERROR_MESSAGE);				
 						}
-						
-						final String err = errorMessage;
-						SwingUtilities.invokeLater(new Runnable() {
-							@Override
-							public void run() {
-								JOptionPane.showMessageDialog(null, err, "Oops..", JOptionPane.ERROR_MESSAGE);				
-							}
-						});
-					}	
+					});
+				}	
 			}
-		});
+		};
+		
+		framework.getTaskManager().queue(task, "Show state graph", monitor);
 	}
 
 }

=== added file 'PetrifyPlugin/src/org/workcraft/plugins/petrify/tools/ShowSgBinary.java'
--- PetrifyPlugin/src/org/workcraft/plugins/petrify/tools/ShowSgBinary.java	1970-01-01 00:00:00 +0000
+++ PetrifyPlugin/src/org/workcraft/plugins/petrify/tools/ShowSgBinary.java	2015-10-13 11:40:49 +0000
@@ -0,0 +1,23 @@
+package org.workcraft.plugins.petrify.tools;
+
+import org.workcraft.plugins.stg.STG;
+import org.workcraft.util.WorkspaceUtils;
+import org.workcraft.workspace.WorkspaceEntry;
+
+public class ShowSgBinary extends ShowSg {
+	
+	@Override
+	public boolean isApplicableTo(WorkspaceEntry we) {
+		return WorkspaceUtils.canHas(we, STG.class);
+	}
+
+	@Override
+	public String getDisplayName() {
+		return "Binary-encoded state graph [write_sg + draw_astg]";
+	}
+	
+	public boolean isBinaryEncodded() {
+		return true;
+	}
+
+}

=== modified file 'PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java'
--- PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java	2015-04-28 22:14:55 +0000
+++ PolicyNetPlugin/src/org/workcraft/plugins/policy/tasks/CheckDeadlockTask.java	2015-10-13 11:40:49 +0000
@@ -15,6 +15,7 @@
 import org.workcraft.plugins.petri.PetriNet;
 import org.workcraft.plugins.policy.VisualPolicyNet;
 import org.workcraft.plugins.policy.tools.PetriNetGenerator;
+import org.workcraft.plugins.shared.CommonDebugSettings;
 import org.workcraft.plugins.shared.tasks.ExternalProcessResult;
 import org.workcraft.serialisation.Format;
 import org.workcraft.tasks.ProgressMonitor;
@@ -22,6 +23,7 @@
 import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.tasks.SubtaskMonitor;
 import org.workcraft.util.Export;
+import org.workcraft.util.FileUtils;
 import org.workcraft.util.Export.ExportTask;
 import org.workcraft.workspace.WorkspaceEntry;
 
@@ -40,7 +42,11 @@
 	@Override
 	public Result<? extends MpsatChainResult> run(ProgressMonitor<? super MpsatChainResult> monitor) {
 		final Framework framework = Framework.getInstance();
+		File directory = null;
 		try {
+			String prefix = FileUtils.getTempPrefix(we.getTitle());
+			directory = FileUtils.createTempDirectory(prefix);
+
 			PetriNetGenerator generator = new PetriNetGenerator((VisualPolicyNet)we.getModelEntry().getVisualModel());
 			PetriNet model = (PetriNet)generator.getPetriNet().getMathModel(); 
 			Exporter exporter = Export.chooseBestExporter(framework.getPluginManager(), model, Format.STG);
@@ -49,14 +55,13 @@
 			}
 			monitor.progressUpdate(0.10);
 			
-			File netFile = File.createTempFile("net", exporter.getExtenstion());
+			File netFile = new File(directory, "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);
 				}
@@ -65,14 +70,12 @@
 			}
 			monitor.progressUpdate(0.20);
 			
-			File unfoldingFile = File.createTempFile("unfolding", MpsatUtilitySettings.getUnfoldingExtension(true));
+			File unfoldingFile = new File(directory, "unfolding" + MpsatUtilitySettings.getUnfoldingExtension(true));
 			PunfTask punfTask = new PunfTask(netFile.getCanonicalPath(), unfoldingFile.getCanonicalPath(), true);
 			Result<? extends ExternalProcessResult> punfResult = framework.getTaskManager().execute(
 					punfTask, "Unfolding .g", mon);
 			
-			netFile.delete();
 			if (punfResult.getOutcome() != Outcome.FINISHED) {
-				unfoldingFile.delete();
 				if (punfResult.getOutcome() == Outcome.CANCELLED) {
 					return new Result<MpsatChainResult>(Outcome.CANCELLED);
 				}
@@ -81,7 +84,8 @@
 			}
 			monitor.progressUpdate(0.70);
 
-			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(), unfoldingFile.getCanonicalPath(), null, true);
+			MpsatTask mpsatTask = new MpsatTask(settings.getMpsatArguments(directory), 
+					unfoldingFile.getCanonicalPath(), directory, true);
 			Result<? extends ExternalProcessResult> mpsatResult = framework.getTaskManager().execute(
 					mpsatTask, "Running deadlock checking [MPSat]", mon);
 			
@@ -97,18 +101,18 @@
 			
 			MpsatResultParser mdp = new MpsatResultParser(mpsatResult.getReturnValue());
 			if (!mdp.getSolutions().isEmpty()) {
-				unfoldingFile.delete();
 				return new Result<MpsatChainResult>(Outcome.FINISHED, 
 						new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net has a deadlock"));
 			}
 			monitor.progressUpdate(1.0);
 
-			unfoldingFile.delete();
 			return new Result<MpsatChainResult>(Outcome.FINISHED, 
 					new MpsatChainResult(exportResult, null, punfResult, mpsatResult, settings, "Policy net is deadlock-free"));
 			
 		} catch (Throwable e) {
 			return new Result<MpsatChainResult>(e);
+		} finally {
+			FileUtils.deleteFile(directory, CommonDebugSettings.getKeepTemporaryFiles());
 		}
 	}
 

=== modified file 'STGPlugin/src/org/workcraft/plugins/stg/StgUtils.java'
--- STGPlugin/src/org/workcraft/plugins/stg/StgUtils.java	2015-09-10 22:34:47 +0000
+++ STGPlugin/src/org/workcraft/plugins/stg/StgUtils.java	2015-10-13 11:40:49 +0000
@@ -10,6 +10,7 @@
 public class StgUtils {
 	public static final String DEVICE_FILE_NAME = "device"; 
 	public static final String ENVIRONMENT_FILE_NAME = "environment"; 
+	public static final String COMPOSITION_FILE_NAME = "composition"; 
 	public static final String SYSTEM_FILE_NAME = "system"; 
 	public static final String ASTG_FILE_EXT = ".g"; 
 	

=== modified file 'WorkcraftCore/src/org/workcraft/gui/tasks/TaskControl.java'
--- WorkcraftCore/src/org/workcraft/gui/tasks/TaskControl.java	2010-07-19 17:07:08 +0000
+++ WorkcraftCore/src/org/workcraft/gui/tasks/TaskControl.java	2015-10-13 11:40:49 +0000
@@ -40,7 +40,6 @@
 	JLabel label;
 	JProgressBar progressBar;
 	JButton btnCancel;
-	JButton btnLog;
 	
 	volatile boolean cancelRequested;
 
@@ -50,7 +49,9 @@
 				{20, 20, 20}
 		};
 		
-		Border lineBorder = BorderFactory.createCompoundBorder(BorderFactory.createLineBorder(Color.LIGHT_GRAY), BorderFactory.createEmptyBorder(3, 3, 3, 3));
+		Border outsideBorder = BorderFactory.createLineBorder(Color.LIGHT_GRAY);
+		Border insideBorder = BorderFactory.createEmptyBorder(3, 3, 3, 3);
+		Border lineBorder = BorderFactory.createCompoundBorder(outsideBorder, insideBorder);
 		
 		setBorder(lineBorder);
 					
@@ -71,7 +72,6 @@
 		progressBar.setMinimumSize(new Dimension (100,20));
 		progressBar.setPreferredSize(new Dimension (300,20));
 
-		btnLog = new JButton("Show log");
 		btnCancel = new JButton("Cancel");
 		btnCancel.addActionListener(new ActionListener() {
 			@Override
@@ -82,7 +82,6 @@
 		
 		add(label, "0,0,2,0");
 		add(progressBar, "0,1,2,1" );
-		add(btnLog, "1,2");
 		add(btnCancel, "2,2");
 	}
 

=== modified file 'WorkcraftCore/src/org/workcraft/gui/tasks/TaskManagerWindow.java'
--- WorkcraftCore/src/org/workcraft/gui/tasks/TaskManagerWindow.java	2014-12-12 18:43:40 +0000
+++ WorkcraftCore/src/org/workcraft/gui/tasks/TaskManagerWindow.java	2015-10-13 11:40:49 +0000
@@ -44,9 +44,9 @@
 import org.workcraft.tasks.DummyProgressMonitor;
 import org.workcraft.tasks.ProgressMonitor;
 import org.workcraft.tasks.Result;
+import org.workcraft.tasks.Result.Outcome;
 import org.workcraft.tasks.Task;
 import org.workcraft.tasks.TaskMonitor;
-import org.workcraft.tasks.Result.Outcome;
 
 @SuppressWarnings("serial")
 public class TaskManagerWindow extends JPanel implements TaskMonitor {
@@ -162,15 +162,23 @@
 		scroll.setViewportView(content);
 		scroll.setHorizontalScrollBarPolicy(ScrollPaneConstants.HORIZONTAL_SCROLLBAR_NEVER);
 
-		Border lineBorder = BorderFactory.createCompoundBorder(BorderFactory.createLineBorder(Color.LIGHT_GRAY), BorderFactory.createEmptyBorder(2, 2, 2, 2));
+		Border outsideBorder = BorderFactory.createLineBorder(Color.LIGHT_GRAY);
+		Border insideBorder = BorderFactory.createEmptyBorder(2, 2, 2, 2);
+		Border lineBorder = BorderFactory.createCompoundBorder(outsideBorder, insideBorder);
 		setBorder(lineBorder);
 
 		final Framework framework = Framework.getInstance();
 		framework.getTaskManager().addObserver(this);
-		
-		JButton comp = new JButton("Queue test task");
-		
-		comp.addActionListener(new ActionListener() {
+
+		// Do we really need this "Queue test task" button? Probably not.
+		// addQueueTestTasksButton(framework);
+		
+	}
+
+	private void addQueueTestTasksButton(final Framework framework) {
+		JButton testTaskButton = new JButton("Queue test task");
+		
+		testTaskButton.addActionListener(new ActionListener() {
 			@Override
 			public void actionPerformed(ActionEvent e) {
 				framework.getTaskManager().queue(new Task<Object>(){
@@ -192,8 +200,7 @@
 
 						@Override
 						public void finished(Result<? extends Object> result, final String description) {
-							if (result.getOutcome() == Outcome.FINISHED )
-							{
+							if (result.getOutcome() == Outcome.FINISHED ) {
 								SwingUtilities.invokeLater(new Runnable() {
 									@Override
 									public void run() {
@@ -206,8 +213,8 @@
 					});
 			}
 		});
-		
-		content.add (comp);
+
+		content.add (testTaskButton);
 	}
 	
 	public void removeTaskControl (TaskControl taskControl) {

=== modified file 'WorkcraftCore/src/org/workcraft/plugins/shared/tasks/ExternalProcessTask.java'
--- WorkcraftCore/src/org/workcraft/plugins/shared/tasks/ExternalProcessTask.java	2015-08-03 12:45:13 +0000
+++ WorkcraftCore/src/org/workcraft/plugins/shared/tasks/ExternalProcessTask.java	2015-10-13 11:40:49 +0000
@@ -65,9 +65,9 @@
 			}
 		}
 		
-		if (userCancelled)
+		if (userCancelled) {
 			return Result.cancelled();
-		
+		}
 		ExternalProcessResult result = new ExternalProcessResult(returnCode, stdoutAccum.getData(), stderrAccum.getData(), Collections.<String, byte[]>emptyMap());
 		
 		return Result.finished(result);
@@ -111,4 +111,5 @@
 		this.returnCode = returnCode;
 		this.finished = true;
 	}
+	
 }