Filter all TLC command-line parameters that interfere or can interfere

with trace exploration if set.

[Refactor][Toolbox]

org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/job/TLCJob.java

@@ -120,29 +120,25 @@ public abstract class TLCJob extends AbstractJob implements IModelConfigurationC
         ILaunchConfiguration config = launch.getLaunchConfiguration();
 
         // deadlock
-        boolean checkDeadlock = config.getAttribute(IModelConfigurationConstants.MODEL_CORRECTNESS_CHECK_DEADLOCK,
-                IModelConfigurationDefaults.MODEL_CORRECTNESS_CHECK_DEADLOCK_DEFAULT);
-        if (!checkDeadlock) /* "!" added by LL on 22 Aug 2009 */
+        if (!checkDeadlock()) /* "!" added by LL on 22 Aug 2009 */
         {
             arguments.add("-deadlock");
         }
 
         // adjust checkpointing
+        if (checkPoint()) {
         	arguments.add("-checkpoint");
         	arguments.add(String.valueOf(CHECKPOINT_INTERVAL));
+        }
 
         boolean hasSpec = config.getAttribute(MODEL_BEHAVIOR_SPEC_TYPE, MODEL_BEHAVIOR_TYPE_DEFAULT) != IModelConfigurationDefaults.MODEL_BEHAVIOR_TYPE_NO_SPEC;
 
         if (hasSpec)
         {
-            boolean runAsModelCheck = config.getAttribute(IModelConfigurationConstants.LAUNCH_MC_MODE,
-                    IModelConfigurationDefaults.LAUNCH_MC_MODE_DEFAULT);
-            if (runAsModelCheck)
+            if (runAsModelCheck())
             {
                 // look for advanced model checking parameters
-                boolean isDepthFirst = config.getAttribute(IModelConfigurationConstants.LAUNCH_DFID_MODE,
-                        IModelConfigurationDefaults.LAUNCH_DFID_MODE_DEFAULT);
-                if (isDepthFirst)
+                if (isDepthFirst())
                 {
                     // for depth-first run, look for the depth
                     int dfidDepth = config.getAttribute(IModelConfigurationConstants.LAUNCH_DFID_DEPTH,
@@ -183,9 +179,7 @@ public abstract class TLCJob extends AbstractJob implements IModelConfigurationC
         // recover from checkpoint
         if (hasSpec)
         {
-            boolean recover = config.getAttribute(IModelConfigurationConstants.LAUNCH_RECOVER,
-                    IModelConfigurationDefaults.LAUNCH_RECOVER_DEFAULT);
-            if (recover)
+            if (recover())
             {
                 IResource[] checkpoints = config.getAdapter(Model.class).getCheckpoints(false);
                 if (checkpoints.length > 0)
@@ -225,8 +219,7 @@ public abstract class TLCJob extends AbstractJob implements IModelConfigurationC
         }
         
         // Visualize state graph
-        final boolean visualizeStateGraph = launch.getLaunchConfiguration().getAttribute(LAUNCH_VISUALIZE_STATEGRAPH, false);
-		if (visualizeStateGraph && hasSpec) {
+		if (visualizeStateGraph() && hasSpec) {
 			// Visualize state graph when requested and a behavior spec is given. A behavior
 			// spec is required for TLC to create states. Default to always colorize edges and 
 			// not to add action edge labels.
@@ -275,6 +268,37 @@ public abstract class TLCJob extends AbstractJob implements IModelConfigurationC
         return (String[]) arguments.toArray(new String[arguments.size()]);
     }
     
+	// Allow subclasses to veto command line parameters if needed.
+
+	protected boolean recover() throws CoreException {
+		return launch.getLaunchConfiguration().getAttribute(IModelConfigurationConstants.LAUNCH_RECOVER,
+				IModelConfigurationDefaults.LAUNCH_RECOVER_DEFAULT);
+	}
+
+	protected boolean isDepthFirst() throws CoreException {
+		return launch.getLaunchConfiguration().getAttribute(IModelConfigurationConstants.LAUNCH_DFID_MODE,
+				IModelConfigurationDefaults.LAUNCH_DFID_MODE_DEFAULT);
+	}
+
+	protected boolean runAsModelCheck() throws CoreException {
+		return launch.getLaunchConfiguration().getAttribute(IModelConfigurationConstants.LAUNCH_MC_MODE,
+				IModelConfigurationDefaults.LAUNCH_MC_MODE_DEFAULT);
+	}
+
+	protected boolean checkPoint() {
+		return true;
+	}
+
+	protected boolean checkDeadlock() throws CoreException {
+		return launch.getLaunchConfiguration().getAttribute(
+				IModelConfigurationConstants.MODEL_CORRECTNESS_CHECK_DEADLOCK,
+				IModelConfigurationDefaults.MODEL_CORRECTNESS_CHECK_DEADLOCK_DEFAULT);
+	}
+
+	protected boolean visualizeStateGraph() throws CoreException {
+		return launch.getLaunchConfiguration().getAttribute(LAUNCH_VISUALIZE_STATEGRAPH, false);
+	}
+
 	/**
      * Returns the action that tells all registered result
      * presenters to show results. Result presenters are registered

org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/job/TraceExplorerJob.java

 package org.lamport.tla.toolbox.tool.tlc.job;
 
-import java.util.Vector;
-
 import org.eclipse.core.runtime.CoreException;
 import org.eclipse.debug.core.ILaunch;
 import org.eclipse.swt.widgets.Display;
@@ -46,28 +44,64 @@ public class TraceExplorerJob extends TLCProcessJob
         });
     }
 
-    /**
-     * We override this method in order to always
-     * make sure that deadlock is always checked.
-     * This method simply removes "-deadlock" from the
-     * array of arguments, if it is present in the super class
-     * implementation of this method.
-     * 
-     * @throws CoreException 
+	// Veto several TLC command line arguments only relevant for regular model
+	// checking but not for trace exploration. This demonstrates why
+	// TraceExplorerJob shouldn't be a subclass of TLCJob.
+    
+	/* (non-Javadoc)
+	 * @see org.lamport.tla.toolbox.tool.tlc.job.TLCJob#recover()
 	 */
-    public String[] constructProgramArguments() throws CoreException
-    {
-        Vector args = new Vector();
-        String[] argsFromSuper = super.constructProgramArguments();
-        for (int i = 0; i < argsFromSuper.length; i++)
-        {
-            if (!argsFromSuper[i].equals("-deadlock"))
-            {
-                args.add(argsFromSuper[i]);
+	@Override
+	protected boolean recover() throws CoreException {
+		// There is nothing that trace exploration could recover from.
+		return false;
+	}
+
+	/* (non-Javadoc)
+	 * @see org.lamport.tla.toolbox.tool.tlc.job.TLCJob#isDepthFirst()
+	 */
+	@Override
+	protected boolean isDepthFirst() throws CoreException {
+		// Always want BFS in trace exploration.
+		return false;
 	}
+
+	/* (non-Javadoc)
+	 * @see org.lamport.tla.toolbox.tool.tlc.job.TLCJob#runAsModelCheck()
+	 */
+	@Override
+	protected boolean runAsModelCheck() throws CoreException {
+		// We don't want trace exploration to run in simulation mode.
+		return true;
 	}
 
-        return (String[]) args.toArray(new String[args.size()]);
+	/* (non-Javadoc)
+	 * @see org.lamport.tla.toolbox.tool.tlc.job.TLCJob#checkPoint()
+	 */
+	@Override
+	protected boolean checkPoint() {
+		// Why would the trace explorer create a checkpoint!?!
+		return false;
 	}
 
+	/* (non-Javadoc)
+	 * @see org.lamport.tla.toolbox.tool.tlc.job.TLCJob#checkDeadlock()
+	 */
+	@Override
+	protected boolean checkDeadlock() throws CoreException {
+		// We override this method in order to always make sure that deadlock is always
+		// checked. This method simply removes "-deadlock" from the array of arguments,
+		// if it is present in the super class implementation of this method.
+		return false;
+	}
+
+	/* (non-Javadoc)
+	 * @see org.lamport.tla.toolbox.tool.tlc.job.TLCJob#visualizeStateGraph()
+	 */
+	@Override
+	protected boolean visualizeStateGraph() throws CoreException {
+		// Never use an IStateWriter to write out the states created by trace
+		// exploration. A trace is just a txt file with a sequence of states.
+		return false;
+	}
 }