Support launching TLC from a relative path.

As a side effect, TLC will create the states/ directory in the CWD.

This is incomplete in that it has only been tested for BFS mode but not
for DFS, simulation, or checkfile.

[Bug][TLC]

tlatools/src/tlc2/TLC.java

@@ -932,7 +932,8 @@ public int process()
                 if (isBFS())
                 {
 					TLCGlobals.mainChecker = new ModelChecker(tool, metadir, stateWriter, deadlock, fromChkpt,
-							FPSetFactory.getFPSetInitialized(fpSetConfiguration, metadir, mainFile), startTime);
+							FPSetFactory.getFPSetInitialized(fpSetConfiguration, metadir, new File(mainFile).getName()),
+							startTime);
 					modelCheckerMXWrapper = new ModelCheckerMXWrapper((ModelChecker) TLCGlobals.mainChecker, this);
 					result = TLCGlobals.mainChecker.modelCheck();
                 } else

tlatools/src/tlc2/tool/CheckImpl.java

@@ -40,7 +40,7 @@ public CheckImpl(ITool tool, String metadir, boolean deadlock,
     this.depth = depth;
     this.curState = null;
     this.coverSet = FPSetFactory.getFPSet();
-    this.coverSet.init(TLCGlobals.getNumWorkers(), this.metadir, tool.getRootFile()+"_cs");
+    this.coverSet.init(TLCGlobals.getNumWorkers(), this.metadir, tool.getRootName()+"_cs");
     this.stateEnum = null;
   }
 

tlatools/src/tlc2/tool/ITool.java

@@ -164,6 +164,15 @@ Context getFcnContext(IFcnLambdaValue fcn, ExprOrOpArgNode[] args, Context c, TL
 
 	String[] getImpliedActNames();
 
+	/**
+	 * @return The name of the root module.
+	 */
+	String getRootName();
+
+	/**
+	 * @return The file name of the root module which might contain the
+	 *         full or relative path information.
+	 */
 	String getRootFile();
 
 	String getConfigFile();

tlatools/src/tlc2/tool/ModelChecker.java

@@ -78,7 +78,7 @@ public ModelChecker(ITool tool, String metadir, final IStateWriter stateWriter,
     public ModelChecker(ITool tool, String metadir, final IStateWriter stateWriter, boolean deadlock, String fromChkpt,
             final FPSetConfiguration fpSetConfig, long startTime) throws EvalException, IOException {
     	this(tool, metadir, stateWriter, deadlock, fromChkpt, startTime);
-    	this.theFPSet = FPSetFactory.getFPSet(fpSetConfig).init(TLCGlobals.getNumWorkers(), metadir, tool.getRootFile());
+    	this.theFPSet = FPSetFactory.getFPSet(fpSetConfig).init(TLCGlobals.getNumWorkers(), metadir, tool.getRootName());
     }
 
     /**
@@ -98,13 +98,13 @@ private ModelChecker(ITool tool, String metadir, final IStateWriter stateWriter,
         // this.theStateQueue = new MemStateQueue(this.metadir);
 
         // Finally, initialize the trace file:
-        this.trace = new ConcurrentTLCTrace(this.metadir, this.tool.getRootFile(), this.tool);
+        this.trace = new ConcurrentTLCTrace(this.metadir, this.tool.getRootName(), this.tool);
 
         // Initialize all the workers:
         this.workers = new Worker[TLCGlobals.getNumWorkers()];
         for (int i = 0; i < this.workers.length; i++)
         {
-            this.workers[i] = this.trace.addWorker(new Worker(i, this, this.metadir, this.tool.getRootFile()));
+            this.workers[i] = this.trace.addWorker(new Worker(i, this, this.metadir, this.tool.getRootName()));
         }
     }
 
@@ -269,7 +269,7 @@ protected int modelCheckImpl() throws Exception
 					// to rewrite the trace file but to reconstruct actual states referenced by
 					// their fingerprints in the trace.
 					this.doNext(this.predErrState, this.checkLiveness ? new SetOfStates() : null,
-							new Worker(4223, this, this.metadir, tool.getRootFile()));
+							new Worker(4223, this, this.metadir, tool.getRootName()));
                 } catch (FingerprintException e)
                 {
                     result = MP.printError(EC.TLC_FINGERPRINT_EXCEPTION, new String[]{e.getTrace(), e.getRootCause().getMessage()});

tlatools/src/tlc2/tool/impl/Spec.java

@@ -93,7 +93,7 @@ abstract class Spec implements ValueConstants, ToolGlobals, Serializable
     protected final String[] impliedActNames; // ... and their names
     protected final ExprNode[] modelConstraints; // Model constraints
     protected final ExprNode[] actionConstraints; // Action constraints
-    protected final ExprNode[] assumptions; // Assumpt	ions
+    protected final ExprNode[] assumptions; // Assumptions
     protected final boolean[] assumptionIsAxiom; // assumptionIsAxiom[i] is true iff assumptions[i]
                                            // is an AXIOM.  Added 26 May 2010 by LL
     private final FilenameToStream resolver; // takes care of path to stream resolution
@@ -118,7 +118,7 @@ public Spec(String specDir, String specFile, String configFile, FilenameToStream
 		// SpecProcessor has be factored out to be able to assign the variables below as
 		// final. SpecProcessor duplicates most of the variables here but I don't have
 		// time to clean it up.
-		final SpecProcessor processor = new SpecProcessor(rootFile, resolver, toolId, defns, config, this, tlaClass);
+		final SpecProcessor processor = new SpecProcessor(getRootName(), resolver, toolId, defns, config, this, tlaClass);
         this.rootModule = processor.getRootModule();
         this.moduleTbl = processor.getModuleTbl();
         this.variablesNodes = processor.getVariablesNodes();
@@ -903,6 +903,10 @@ public FilenameToStream getResolver()
         return resolver;
     }
 
+    public String getRootName() {
+    	return new File(this.rootFile).getName();
+    }
+
     public String getRootFile() {
     	return this.rootFile;
     }