// Last modified on Wed Dec  5 22:37:20 PST 2001 by yuanyu 
//      modified on Wed Jun 16 15:42:32 PDT 1999 by wischik

package tlatk;

import java.io.*;
import java.util.Random;
import tlatk.ast.*;
import tlatk.tool.*;
import tlatk.value.Value;
import tlatk.util.*;

public class TLC {
  /*
   * This TLA checker (TLC) provides the following functionalities:
   *  1. Syntax checking of TLA+ specs: java tlatk.TLC -syntax spec[.tla]
   *  2. Simulation of TLA+ specs: java tlatk.TLC -simulate spec[.tla]
   *  3. Model checking of TLA+ specs: java tlatk.TLC [-modelcheck] spec[.tla]
   *
   * The command line also provides the following options:
   *  o -config file: provide the config file.
   *    Defaults to spec.cfg if not provided
   *  o -deadlock: do not check for deadlock.
   *    Defaults to checking deadlock if not specified
   *  o -depth num: specify the depth of random simulation
   *    Defaults to 100 if not specified
   *  o -seed num: provide the seed for random simulation
   *    Defaults to a random seed if not specified
   *  o -aril num: Adjust the seed for random simulation
   *    Defaults to 0 if not specified
   *  o -recover path: recover from checkpoint in path
   *    Defaults to scratch run if not specified
   *  o -workers num: the number of TLC worker threads
   *    Defaults to 1
   *  o -cleanup: clean up the states directory
   *  o -dump file: dump all the states into file
   *  o -difftrace: when printing trace, show only
   *                the differences between successive states
   *    Defaults to printing full state descriptions if not specified
   *    (Added by Rajeev Joshi)
   *  o -terse: do not expand values in Print statement
   *    Defaults to expand value if not specified
   *  o -coverage seconds: collect coverage information on the spec,
   *                       print out the information every seconds
   *    Defaults to no coverage if not specified
   *  o -continue: continue running even when invariant is violated
   *    Defaults to not continuing if not specified
   *  o -nowarning: disable all the warnings
   *    Defaults to report warnings if not specified
   */
  public static void main(String[] args) {
    System.out.println("TLC " + TLCGlobals.versionOfTLC);

    String mainFile = null;
    String configFile = null;
    boolean deadlock = true;
    boolean cleanup = false;
    String dumpFile = null;    
    int traceDepth = 100;
    boolean noSeed = true;
    long seed = 0;
    long aril = 0;
    String fromChkpt = null;
    int typeOfCheck = 3;    // Default: model checking

    int index = 0;
    while (index < args.length) {
      if (args[index].equals("-syntax")) {
	typeOfCheck = 1;
	index++;
      }
      else if (args[index].equals("-simulate")) {
	if (typeOfCheck > 2) typeOfCheck = 2;
	index++;
      }
      else if (args[index].equals("-modelcheck")) {
	index++;
      }
      else if (args[index].equals("-config")) {
	index++;
	if (index < args.length) {
	  configFile = args[index];
	  int len = configFile.length();
	  if (configFile.startsWith(".cfg", len-4)) {
	    configFile = configFile.substring(0, len-4);
	  }
	  index++;
	}
	else {
	  printErrorMsg("Error: expect a file name for -config option.");
	  return;
	}
      }
      else if (args[index].equals("-difftrace")) {
 	index++;
 	TLCTrace.setPrintDiffsOnly() ;
      }
      else if (args[index].equals("-deadlock")) {
	index++;
	deadlock = false;
      }
      else if (args[index].equals("-cleanup")) {
	index++;
	cleanup = true;
      }
      else if (args[index].equals("-nowarning")) {
	index++;
	TLCGlobals.noWarning = true;
      }
      else if (args[index].equals("-dump")) {
	index++;
	if (index < args.length) {
	  dumpFile = args[index];
	  int len = dumpFile.length();
	  if (!(dumpFile.startsWith(".dump", len-5))) {
	    dumpFile = dumpFile + ".dump";
	  }
	  index++;
	}
	else {
	  printErrorMsg("Error: A file name for dumping states required.");
	  return;
	}
      }
      else if (args[index].equals("-dir")) {
	index++;
	if (index < args.length) {
	  TLCGlobals.metaRoot = args[index];
	  index++;
	}
	else {
	  printErrorMsg("Error: A directory name for checkpoints required.");
	  return;
	}
      }
      else if (args[index].equals("-depth")) {
	index++;
	if (index < args.length) {
	  try {
	    traceDepth = Integer.parseInt(args[index]);
	    index++;
	  }
	  catch (Exception e) {
	    printErrorMsg("Error: An integer for trace length required. But encountered " +
			  args[index]);
	    return;
	  }
	}
	else {
	  printErrorMsg("Error: trace length required.");
	  return;
	}
      }
      else if (args[index].equals("-seed")) {
        index++;
        if (index < args.length) {
          try {
            seed = Long.parseLong(args[index]);
            index++;
            noSeed = false;
          }
          catch (Exception e) {
            printErrorMsg("Error: An integer for seed required. But encountered " +
			  args[index]);
            return;
          }
        }
        else {
          printErrorMsg("Error: seed required.");
          return;
        }
      }
      else if (args[index].equals("-aril")) {
        index++;
        if (index < args.length) {
          try {
            aril = Long.parseLong(args[index]);
            index++;
          }
          catch (Exception e) {
            printErrorMsg("Error: An integer for aril required. But encountered " +
			  args[index]);
            return;
          }
        }
        else {
          printErrorMsg("Error: aril required.");
          return;
        }
      }
      else if (args[index].equals("-recover")) {
        index++;
        if (index < args.length) {
          fromChkpt = args[index++] + File.separator;
        }
        else {
	  printErrorMsg("Error: need to specify the metadata directory for recovery.");
          return;
        }
      }
      else if (args[index].equals("-workers")) {
        index++;
        if (index < args.length) {
          try {
            TLCGlobals.setNumWorkers(Integer.parseInt(args[index]));
            index++;
          }
          catch (Exception e) {
            printErrorMsg("Error: worker number required. But encountered " +
			  args[index]);
            return;
          }
          if (TLCGlobals.getNumWorkers() < 1) {
            printErrorMsg("Error: at least one worker required.");
            return;
          }
        }
        else {
          printErrorMsg("Error: expect an integer for -workers option.");
          return;
        }
      }
      else if (args[index].equals("-terse")) {
	index++;
	Value.expand = false;
      }
      else if (args[index].equals("-coverage")) {
	index++;
	TLCGlobals.coverage = true;
	if (index < args.length) {
	  try {
	    TLCGlobals.coverageInterval = Integer.parseInt(args[index]) * 60000;
	    index++;
	  }
	  catch (Exception e) {
	    printErrorMsg("Error: An integer for coverage report interval required." +
			  " But encountered " + args[index]);
	    return;
	  }
	}
	else {
	  printErrorMsg("Error: coverage report interval required.");
	  return;
	}
      }
      else if (args[index].equals("-continue")) {
	index++;
	TLCGlobals.continuation = true;
      }
      else {
        if (args[index].charAt(0) == '-') {
          printErrorMsg("Error: unrecognized option: " + args[index]);
          return;
        }
        if (mainFile != null) {
          printErrorMsg("Error: more than one input files: " + mainFile +
			" and " + args[index]);
          return;
        }
        mainFile = args[index++];
        int len = mainFile.length();
        if (mainFile.startsWith(".tla", len-4)) {
          mainFile = mainFile.substring(0, len-4);
        }
      }
    }
    if (mainFile == null) {
      printErrorMsg("Error: Missing input TLA+ module.");
      return;
    }
    if (configFile == null) configFile = mainFile;

    try {
      // Initialize:
      if (fromChkpt != null) {
        // We must recover the intern var table as early as possible
        Variable.internTbl.recover(fromChkpt);
      }
      if (cleanup && fromChkpt == null) {
        // clean up the states directory only when not recovering
        FileUtil.deleteDir(new File(TLCGlobals.metaRoot), true);
      }
      // Start checking:
      switch (typeOfCheck) {
      case 1:
	{
	  // syntax checking
	  System.out.println("Syntax-checking");
	  int lastSep = mainFile.lastIndexOf(File.separatorChar);
	  String specDir = (lastSep == -1) ? "" : mainFile.substring(0, lastSep+1);
	  String specFile = mainFile.substring(lastSep+1);
	  Spec spec = new Spec(specDir, specFile);
	  spec.parse();
	  break;
	}
      case 2:
        {
	  // simulation
	  RandomGenerator rng = new RandomGenerator();
	  if (noSeed) {
	    seed = rng.nextLong();
	    rng.setSeed(seed);
	  }
	  else {
	    rng.setSeed(seed, aril);
	  }
	  System.out.println("Running Random Simulation with seed " + seed + ".");
	  Simulator simulator = new Simulator(mainFile, configFile, deadlock,
					      traceDepth, rng, seed);
	  simulator.simulate();
	  break;
	}
      case 3:
        {
	  // model checking
	  System.out.println("Model-checking");
	  ModelChecker mc = new ModelChecker(mainFile, configFile, dumpFile,
					     deadlock, fromChkpt);
	  mc.modelCheck();
	  break;
	}
      }
    }
    catch (Throwable e) {
      System.gc();
      if (e instanceof StackOverflowError) {
        System.err.println("Error: This was a Java StackOverflowError. It was probably\n" +
                           "the result of an incorrect recursive function definition\n" +
                           "that caused TLC to enter an infinite loop when trying to\n" +
                           "compute the function or its application to an element in\n" +
                           "its putative domain.");
      }
      else if (e instanceof OutOfMemoryError) {
	System.err.println("Error: Java ran out of memory.  Running Java with a larger memory\n" +
			   "allocation pool (heap) may fix this.  But it won't help if some\n" +
			   "state has an enormous number of successor states, or if TLC must\n" +
			   "compute the value of a huge set.");
      }
      else {
	System.err.println("Error: " + e.getMessage());
      }
    }
    System.exit(0);    
  }

  private static void printErrorMsg(String msg) {
    System.err.println(msg);
    System.err.println("Usage: java tlatk.TLC [-option] inputfile");
  }

}