From c9eb9466c84c0d28a64ac6dc3593b67dec4f809d Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Sun, 31 May 2015 10:19:28 +0200
Subject: [PATCH] [Bugfix] Trace exploration fails silently after loading an
 external TLC output file into the Model editor's result page.

Loading an existing TLC output file into the Model editor's results page
only creates the MC.out, but not the MC_TE.out file. Then trace
exploration fails silently due to the missing MC_TE.out file. It is
unknown why there has to be a MC_TE.out file which is an identical copy
of the MC.out file in the first place.
---
 .../tool/tlc/ui/editor/page/ResultPage.java   | 62 ++++++++++++++-----
 .../toolbox/tool/tlc/util/ModelHelper.java    | 29 ++++++---
 2 files changed, 68 insertions(+), 23 deletions(-)

diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
index 3cfbe47f9..313a2d1ee 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
@@ -11,7 +11,14 @@ import java.util.Vector;
 import java.util.concurrent.locks.Lock;
 import java.util.concurrent.locks.ReentrantLock;
 
+import org.eclipse.core.resources.IWorkspace;
+import org.eclipse.core.resources.ResourcesPlugin;
+import org.eclipse.core.resources.WorkspaceJob;
 import org.eclipse.core.runtime.CoreException;
+import org.eclipse.core.runtime.IProgressMonitor;
+import org.eclipse.core.runtime.IStatus;
+import org.eclipse.core.runtime.Status;
+import org.eclipse.core.runtime.jobs.Job;
 import org.eclipse.debug.core.ILaunchConfiguration;
 import org.eclipse.jface.action.Action;
 import org.eclipse.jface.resource.JFaceResources;
@@ -51,6 +58,7 @@ import org.eclipse.ui.forms.widgets.Hyperlink;
 import org.eclipse.ui.forms.widgets.Section;
 import org.eclipse.ui.forms.widgets.TableWrapData;
 import org.eclipse.ui.forms.widgets.TableWrapLayout;
+import org.eclipse.ui.progress.UIJob;
 import org.lamport.tla.toolbox.tool.tlc.output.data.CoverageInformationItem;
 import org.lamport.tla.toolbox.tool.tlc.output.data.ITLCModelLaunchDataPresenter;
 import org.lamport.tla.toolbox.tool.tlc.output.data.StateSpaceInformationItem;
@@ -585,21 +593,45 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
 		}
 
 		public void run() {
-			FileDialog fileDialog = new FileDialog(new Shell());
-			String path = fileDialog.open();
-			try {
-				TLCOutputSourceRegistry modelCheckSourceRegistry = TLCOutputSourceRegistry
-						.getModelCheckSourceRegistry();
-				modelCheckSourceRegistry
-						.removeTLCStatusSource(new ILaunchConfiguration[] { getConfig() });
-				ModelHelper.createModelOutputLogFile(getConfig(),
-						new FileInputStream(new File(path)));
-				ResultPage.this.loadData();
-			} catch (CoreException e) {
-				e.printStackTrace();
-			} catch (FileNotFoundException e) {
-				e.printStackTrace();
-			}
+			// Get the user input (the path to the TLC output file).
+			final FileDialog fileDialog = new FileDialog(new Shell());
+			final String path = fileDialog.open();
+			
+			// I/O operations should never run inside the UI thread.
+			final Job j = new WorkspaceJob("Loading output file...") {
+				public IStatus runInWorkspace(final IProgressMonitor monitor) throws CoreException {
+					try {
+						// Import the file into the Toolbox on the file/resource layer.
+						final TLCOutputSourceRegistry modelCheckSourceRegistry = TLCOutputSourceRegistry
+								.getModelCheckSourceRegistry();
+						modelCheckSourceRegistry
+								.removeTLCStatusSource(new ILaunchConfiguration[] { getConfig() });
+						ModelHelper.createModelOutputLogFile(getConfig(),
+								new FileInputStream(new File(path)), monitor);
+						
+						// Once the output has been imported on the
+						// file/resource layer, update the UI.
+						final Job job = new UIJob("Updating results page with loaded output...") {
+							public IStatus runInUIThread(IProgressMonitor monitor) {
+								try {
+									ResultPage.this.loadData();
+								} catch (CoreException e) {
+									return new Status(IStatus.ERROR, TLCUIActivator.PLUGIN_ID, e.getMessage(), e);
+								}
+								return Status.OK_STATUS;
+							}
+						};
+						job.schedule();
+						
+					} catch (FileNotFoundException e) {
+						return new Status(IStatus.ERROR, TLCUIActivator.PLUGIN_ID, e.getMessage(), e);
+					}
+	                return Status.OK_STATUS;
+				}
+			};
+		   	final IWorkspace workspace = ResourcesPlugin.getWorkspace();
+			j.setRule(workspace.getRuleFactory().buildRule());
+			j.schedule();
 		}
 	}
 
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
index 0a8a3f715..50ca3324f 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
@@ -30,7 +30,6 @@ import org.eclipse.core.runtime.CoreException;
 import org.eclipse.core.runtime.IPath;
 import org.eclipse.core.runtime.IProgressMonitor;
 import org.eclipse.core.runtime.IStatus;
-import org.eclipse.core.runtime.NullProgressMonitor;
 import org.eclipse.core.runtime.Status;
 import org.eclipse.core.runtime.SubProgressMonitor;
 import org.eclipse.core.runtime.jobs.ISchedulingRule;
@@ -715,25 +714,39 @@ public class ModelHelper implements IModelConfigurationConstants, IModelConfigur
         return null;
     }
     
-    public static void createModelOutputLogFile(ILaunchConfiguration config, InputStream is) throws CoreException {
+    public static void createModelOutputLogFile(ILaunchConfiguration config, InputStream is, IProgressMonitor monitor) throws CoreException {
         Assert.isNotNull(config);
         IFolder targetFolder = ModelHelper.getModelTargetDirectory(config);
-		// create targetFolder which might be missing if the model has never
+		// Create targetFolder which might be missing if the model has never
 		// been checked but the user wants to load TLC output anyway.
 		// This happens with distributed TLC, where the model is executed
 		// remotely and the log is send to the user afterwards.
         if (targetFolder == null || !targetFolder.exists()) {
             String modelName = getModelName(config.getFile());
     		targetFolder = config.getFile().getProject().getFolder(modelName);
-    		targetFolder.create(true, true, new NullProgressMonitor());
+    		targetFolder.create(true, true, monitor);
         }
         if (targetFolder != null && targetFolder.exists())
         {
-        	IFile file = targetFolder.getFile(ModelHelper.FILE_OUT);
-        	if (file.exists()) {
-        		file.delete(true, new NullProgressMonitor());
+			// Always refresh the folder in case it has to override an existing
+			// file that is out-of-sync with the Eclipse foundation layer.
+        	targetFolder.refreshLocal(IFolder.DEPTH_INFINITE, monitor);
+        	
+        	// Import MC.out
+        	IFile mcOutFile = targetFolder.getFile(ModelHelper.FILE_OUT);
+        	if (mcOutFile.exists()) {
+        		mcOutFile.delete(true, monitor);
         	}
-        	file.create(is, true, new NullProgressMonitor());
+        	mcOutFile.create(is, true, monitor); // create closes the InputStream is.
+        	
+        	// Import MC_TE.out by copying the MC.out file to MC_TE.out.
+			// The reason why there are two identical files (MC.out and
+			// MC_TE.out) has been lost in history.
+        	IFile mcTEOutfile = targetFolder.getFile(ModelHelper.TE_TRACE_SOURCE);
+        	if (mcTEOutfile.exists()) {
+        		mcTEOutfile.delete(true, monitor);
+        	}
+        	mcOutFile.copy(mcTEOutfile.getFullPath(), true, monitor);
         }
     }
 
-- 
GitLab