[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.

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();
+			// 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 {
-				TLCOutputSourceRegistry modelCheckSourceRegistry = TLCOutputSourceRegistry
+						// 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)));
+								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) {
-				e.printStackTrace();
+									return new Status(IStatus.ERROR, TLCUIActivator.PLUGIN_ID, e.getMessage(), e);
+								}
+								return Status.OK_STATUS;
+							}
+						};
+						job.schedule();
+						
 					} catch (FileNotFoundException e) {
-				e.printStackTrace();
+						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();
 		}
 	}
 

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);
+        	}
+        	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);
         	}
-        	file.create(is, true, new NullProgressMonitor());
+        	mcOutFile.copy(mcTEOutfile.getFullPath(), true, monitor);
         }
     }