---

SpinTrans.java

package edu.ksu.cis.bandera.spin;

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Bandera, a Java(TM) analysis and transformation toolkit           *
 * Copyright (C) 1998, 1999   James Corbett (corbett@hawaii.edu)     *
 * All rights reserved.                                              *
 *                                                                   *
 * This work was done as a project in the SAnToS Laboratory,         *
 * Department of Computing and Information Sciences, Kansas State    *
 * University, USA (http://www.cis.ksu.edu/santos).                  *
 * It is understood that any modification not identified as such is  *
 * not covered by the preceding statement.                           *
 *                                                                   *
 * This work is free software; you can redistribute it and/or        *
 * modify it under the terms of the GNU Library General Public       *
 * License as published by the Free Software Foundation; either      *
 * version 2 of the License, or (at your option) any later version.  *
 *                                                                   *
 * This work is distributed in the hope that it will be useful,      *
 * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
 * Library General Public License for more details.                  *
 *                                                                   *
 * You should have received a copy of the GNU Library General Public *
 * License along with this toolkit; if not, write to the             *
 * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
 * Boston, MA  02111-1307, USA.                                      *
 *                                                                   *
 * Java is a trademark of Sun Microsystems, Inc.                     *
 *                                                                   *
 * To submit a bug report, send a comment, or get the latest news on *
 * this project and other SAnToS projects, please visit the web-site *
 *                http://www.cis.ksu.edu/santos                      *
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
import java.io.*;
import java.util.Vector;
import java.util.StringTokenizer;
import java.util.List;
import java.util.LinkedList;

import edu.ksu.cis.bandera.bir.*;
import edu.ksu.cis.bandera.checker.*;
import edu.ksu.cis.bandera.util.*;

/**
 * SpinTrans is the main class of the SPIN translator, which generates
 * PROMELA source representing a transition system.
 * <p>
 * The SPIN translator is invoked on a transition system as follows:
 * <pre>
 * // Parameters
 * TransSystem system = ...;   // the transition system
 * SpinOptions options = new SpinOptions();   // SPIN options
 * options.setMemoryLimit(256);            // set various options
 * ...
 * SpinTrans spin = SpinTrans.translate(system,options);  // invoke translator
 * spin.runSpin();                           // Run SPIN on generated PROMELA
 * BirTrace trace = spin.parseOutput();      // Parse output as BIR trace
 * </pre>
 */

public class SpinTrans extends AbstractExprSwitch implements BirConstants, Checker {
  TransSystem system;
  PrintWriter out; // Dest for translator output
  SpinTypeName namer; // Helper class to name types

  // Print control flags
  int indentLevel = 0; // indentation level
  boolean inDefine = false; // inside #define (must end line with \)
  boolean newLine = true; // at beginning of line (must indent)

  boolean resetTemp = false; // temp used during trans---reset it at end
  Transformation currentTrans; // Current trans being translated
  int actionNum; // Action number of current trans

  SpinOptions options;
  boolean ranVerifier = false;
  String panOutput;

  static String ccName = "gcc";

  // This is a special case name that is present in all case trees
  public static final String normal = "NORMAL_CASE";

    //private static boolean isWindows = System.getProperty("os.name").indexOf("Windows") >= 0;

    // Robbyjo's patch
    private boolean isVerbose = true;
    private String outputDir = "."+File.separator;
  SpinTrans(TransSystem system, SpinOptions options, PrintWriter out) {
    this.system = system;
    this.out = out;
    this.namer = new SpinTypeName();
    this.options = (options == null) ? new SpinOptions() : options;
  }  
  /**
   * Get action ID of current action = loc_num trans_index action_index
   */

  String actionId() {
    int locNum = currentTrans.getFromLoc().getId();
    int transNum = currentTrans.getFromLoc().getOutTrans().indexOf(
                     currentTrans);
    return locNum + " " + transNum + " " + actionNum;
  }  
  /**
   * Get action ID of current action, but comma seperated.
   */

  String actionIdWithCommas() {
    int locNum = currentTrans.getFromLoc().getId();
    int transNum = currentTrans.getFromLoc().getOutTrans().indexOf(
                     currentTrans);
    return locNum + "," + transNum + "," + actionNum;
  }  
  /**
   * Apply translator to BIR Expr, return case tree.
   */

  CaseNode applyTo(Expr expr) {
    expr.apply(this);
    return (CaseNode) getResult();
  }  
  public void caseAddExpr(AddExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " + ");
  }  
  public void caseAndExpr(AndExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " && ");
  }  
  /**
   * Translate array expression.
   * <p>
   * Must insert traps for array out of bounds.
   */

  public void caseArrayExpr(ArrayExpr expr) {
    TreeNode arrayTree = applyTo(expr.getArray());
    TreeNode indexTree = applyTo(expr.getIndex());
    TreeNode result = arrayTree.compose(indexTree, null);
    Vector leafCases = result.getLeafCases(new Vector());
    for (int i = 0; i < leafCases.size(); i++) {
      Case leafCase = (Case) leafCases.elementAt(i);
      ExprNode leaf = (ExprNode) leafCase.node;
      // expr1 is array name, expr2 is index
      leafCase.insertTrap(leaf.expr2 + " >= " + leaf.expr1 + ".length",
                          "ArrayIndexOutOfBoundsException",true);
      if (! nonNegative(expr.getIndex()))
        leafCase.insertTrap(leaf.expr2 + " < 0", "ArrayIndexOutOfBoundsException",
                            true);
      leaf.update(leaf.expr1 + ".element[" + leaf.expr2 + "]");
    }
    setResult(result);
  }  
  /**
   * Translate assert action.
   */

  public void caseAssertAction(AssertAction assertAction) {
    CaseNode condTree = (CaseNode) applyTo(assertAction.getCondition());
    Vector leaves = condTree.getLeaves(new Vector());
    // Assert each leaf is true
    for (int i = 0; i < leaves.size(); i++) {
      ExprNode leaf = (ExprNode) leaves.elementAt(i);
      leaf.update("assert(" + leaf.expr1 + ");");
    }
    printStatement(condTree.getCase(normal));
  }  
  /**
   * Translate a BIR assignment action.
   */

  public void caseAssignAction(AssignAction assign) {
    TreeNode rhsTree = applyTo(assign.getRhs());
    TreeNode lhsTree = applyTo(assign.getLhs());
    CaseNode result = (CaseNode) lhsTree.compose(rhsTree, null);
    Vector leafCases = result.getLeafCases(new Vector());
    for (int i = 0; i < leafCases.size(); i++) {
      Case leafCase = (Case) leafCases.elementAt(i);
      ExprNode leaf = (ExprNode) leafCase.node;
      Type rhsType = assign.getRhs().getType();
      Type lhsType = assign.getLhs().getType();
      // Make run-time checks on assignment if not subtype
      if (! rhsType.isSubtypeOf(lhsType)) {

        // Check subrange for limit exception
        if (lhsType.isKind(RANGE) &&
            ! lhsType.containsValue(assign.getRhs())) {
          Range range = (Range) lhsType;
          leafCase.insertTrap(leaf.expr2 + " < " +
                              range.getFromVal(), "RangeLimitException",
                              false);
          leafCase.insertTrap(leaf.expr2 + " > " +
                              range.getToVal(), "RangeLimitException", false);
        }

        // Check ref assignment for class cast exception
        if (lhsType.isKind(REF) &&
            ! (assign.getRhs() instanceof NullExpr)) {
          String trapDesc = "ClassCastException";
          StateVarVector lhsTargets =
            ((Ref) lhsType).getTargets();
          StateVarVector rhsTargets =
            ((Ref) rhsType).getTargets();
          for (int j = 0; j < rhsTargets.size(); j++)
            if (! lhsTargets.contains(
                  rhsTargets.elementAt(j))) {
              String check =
                "_collect(" + leaf.expr2 + ") == " +
                refIndex(rhsTargets.elementAt(j));
              leafCase.insertTrap(check, "ClassCastException",
                                  true);
            }
        }
      }
      leaf.update(leaf.expr1 + " = " + leaf.expr2 + ";");
    }
    printStatement(result.getCase(normal));
  }  
  public void caseBoolLit(BoolLit expr) {
    setResult(specialize("" + expr.getValue()));
  }  
  /**
   * Translate choose expression.
   * <p>
   * As in NexExpr, we spit out code (in this case a nondeterministic
   * if statement) that sets the _temp_ variable of the process.
   * We then return _temp_ as the value of the expression.
   * Once again, this is safe because a choose() must appear
   * alone on the RHS of an assign action.
   */

  public void caseChooseExpr(ChooseExpr expr) {
    Vector choices = expr.getChoices();
    println("if");
    for (int i = 0; i < choices.size(); i++) {
      Expr choice = (Expr) choices.elementAt(i);
      ExprNode leaf = (ExprNode) applyTo(choice).getCase(normal);
      println(":: _temp_ = " + leaf.expr1 + "; printf(\"BIR? " +
              actionNum + " " + i + "\\n\"); ");
    }
    println("fi;");
    resetTemp = true;
    setResult(specialize("_temp_"));
  }  
  public void caseConstant(Constant expr) {
    setResult(specialize(expr.getName()));
  }  
  /**
   * Translate dereference.
   * <p>
   * This is the case that creates most of the CaseNodes in
   * a case tree.  We need to branch based on the collection
   * of the target.
   */

  public void caseDerefExpr(DerefExpr expr) {
    TreeNode result = applyTo(expr.getTarget());
    StateVarVector targets =
      ((Ref) expr.getTarget().getType()).getTargets();
    Vector leafCases = result.getLeafCases(new Vector());
    for (int i = 0; i < leafCases.size(); i++) {
      Case leafCase = (Case) leafCases.elementAt(i);
      ExprNode leaf = (ExprNode) leafCase.node;
      CaseNode caseNode = new CaseNode();
      // Loop through the possible targets, making a case for each
      for (int j = 0; j < targets.size(); j++) {
        StateVar target = targets.elementAt(j);
        String prom = target.getName();
        // For collections, add the instance selection
        if (target.getType().isKind(COLLECTION))
          prom += ".instance[_index(" + leaf.expr1 + ")]";
        String cond = "(_collect(" + leaf.expr1 + ") == " +
                      refIndex(target) + ")";
        caseNode.addCase(cond, prom);
      }
      // Collection 0 is the null pointer
      String cond = "(_collect(" + leaf.expr1 + ") == 0)";
      caseNode.addTrapCase(cond, "NullPointerException", true);
      leafCase.replace(caseNode);
    }
    setResult(result);
  }  
  /**
   * Translate division.
   * <p>
   * DivExpr and RemExpr require special handling because they
   * can cause a ArithmeticException if the second arg is zero.
   */

  public void caseDivExpr(DivExpr expr) {
    TreeNode e1Tree = applyTo(expr.getOp1());
    TreeNode e2Tree = applyTo(expr.getOp2());
    TreeNode result = e1Tree.compose(e2Tree, null);
    Vector leafCases = result.getLeafCases(new Vector());
    for (int i = 0; i < leafCases.size(); i++) {
      Case leafCase = (Case) leafCases.elementAt(i);
      ExprNode leaf = (ExprNode) leafCase.node;
      leafCase.insertTrap(leaf.expr2 + " == 0", "ArithmeticException",
                          true);
      leaf.update("(" + leaf.expr1 + " / " + leaf.expr2 + ")");
    }
    setResult(result);
  }  
  public void caseEqExpr(EqExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " == ");
  }  
  /**
   * Translate instanceof expression (basically a big disjunction to
   * test the refIndex for all possible targets).
   */

  public void caseInstanceOfExpr(InstanceOfExpr expr) {
    TreeNode result = applyTo(expr.getRefExpr());
    StateVarVector targets = expr.getRefType().getTargets();
    Vector leafCases = result.getLeafCases(new Vector());
    for (int i = 0; i < leafCases.size(); i++) {
      Case leafCase = (Case) leafCases.elementAt(i);
      ExprNode leaf = (ExprNode) leafCase.node;
      CaseNode caseNode = new CaseNode();
      String elseCond = "! (";
      for (int j = 0; j < targets.size(); j++) {
        StateVar target = targets.elementAt(j);
        String cond = "(_collect(" + leaf.expr1 + ") == " +
                      refIndex(target) + ")";
        caseNode.addCase(cond, "1");
        if (j > 0)
          elseCond += " || ";
        elseCond += cond;
      }
      elseCond += ")";
      caseNode.addCase(elseCond, "0");
      leafCase.replace(caseNode);
    }
    setResult(result);
  }  
  public void caseIntLit(IntLit expr) {
    setResult(specialize("" + expr.getValue()));
  }  
  public void caseLeExpr(LeExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " <= ");
  }  
  /**
   * Translate array length expression.
   */

  public void caseLengthExpr(LengthExpr expr) {
    TreeNode result = applyTo(expr.getArray());
    Vector leaves = result.getLeaves(new Vector());
    for (int i = 0; i < leaves.size(); i++) {
      ExprNode leaf = (ExprNode) leaves.elementAt(i);
      leaf.update(leaf.expr1 + ".length");
    }
    setResult(result);
  }  
  /**
   * Translate lock action.
   */

  public void caseLockAction(LockAction lockAction) {
    CaseNode lockTree = (CaseNode) applyTo(lockAction.getLockExpr());
    String opName =
      "_" + LockAction.operationName(lockAction.getOperation());
    // Wait action requires specific thread id
    if (lockAction.isWait())
      opName += "_" + lockAction.getThread().getId();
    Lock lockType = (Lock) lockAction.getLockExpr().getType();
    // Reentrant locks require _R versions of operations (except notify)
    if (lockType.isReentrant() &&
        ! lockAction.isLockAction(NOTIFY | NOTIFYALL))
      opName += "_R";
    Vector leaves = lockTree.getLeaves(new Vector());
    for (int i = 0; i < leaves.size(); i++) {
      ExprNode leaf = (ExprNode) leaves.elementAt(i);
      // Apply op to each leaf expr
      leaf.update(opName + "(" + leaf.expr1 + "," +
                  actionIdWithCommas() + ");");
    }
    printStatement(lockTree.getCase(normal));
  }  
  /**
   * Translate lock test.
   */

  public void caseLockTest(LockTest lockTest) {
    TreeNode lockTree;
    Vector leaves;
    switch (lockTest.getOperation()) {
      case LOCK_AVAILABLE:
        String opName = "_lockAvailable";
        // Reentrant locks require special _R versions of operations
        if (((Lock) lockTest.getLockExpr().getType()).isReentrant())
          opName += "_R";
        lockTree = applyTo(lockTest.getLockExpr());
        leaves = lockTree.getLeaves(new Vector());
        for (int i = 0; i < leaves.size(); i++) {
          ExprNode leaf = (ExprNode) leaves.elementAt(i);
          leaf.update(opName + "(" + leaf.expr1 + ")");
        }
        setResult(lockTree);
        return;
      case HAS_LOCK:
        // We don't use this test (it's always true)
        setResult(specialize("true"));
        return;
      case WAS_NOTIFIED:
        lockTree = applyTo(lockTest.getLockExpr());
        leaves = lockTree.getLeaves(new Vector());
        for (int i = 0; i < leaves.size(); i++) {
          ExprNode leaf = (ExprNode) leaves.elementAt(i);
          leaf.update("_wasNotified_" +
                      lockTest.getThread().getId() + "(" +
                      leaf.expr1 + ")");
        }
        setResult(lockTree);
        return;
    }
  }  
  public void caseLtExpr(LtExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " < ");
  }  
  public void caseMulExpr(MulExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " * ");
  }  
  public void caseNeExpr(NeExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " != ");
  }  
  /**
   * Translate array allocator.
   * <p>
   * Similar to NewExpr (above), except that we need to set (and check)
   * the supplied length.
   */

  public void caseNewArrayExpr(NewArrayExpr expr) {
    StateVar target = expr.getCollection();
    int size = ((Collection) target.getType()).getSize().getValue();
    int locNum = currentTrans.getFromLoc().getId();
    int transNum = currentTrans.getFromLoc().getOutTrans().indexOf(
                     currentTrans);
    // Call macro _allocate(collection,refindex,size,locNum,transNum,actionNum)
    println("_allocate(" + target.getName() + "," +
            refIndex(target) + "," + size + "," + locNum + "," +
            transNum + "," + actionNum + ");");
    Array type = (Array)((Collection) target.getType()).getBaseType();
    int maxLength = type.getSize().getValue();
    // Translate the length expression, then update each leaf to
    // (a) check that the length is less than the max for this type
    // (b) if so, assign the supplied length to the .length field
    //     of the array instance just allocated (_temp_).
    CaseNode setLength = applyTo(expr.getLength());
    Vector leafCases = setLength.getLeafCases(new Vector());
    for (int i = 0; i < leafCases.size(); i++) {
      Case leafCase = (Case) leafCases.elementAt(i);
      ExprNode leaf = (ExprNode) leafCase.node;
      leafCase.insertTrap(leaf.expr1 + " > " + maxLength, "ArraySizeLimitException",
                          false);
      leaf.update(target.getName() +
                  ".instance[_index(_temp_)].length = " +
                  leaf.expr1 + "; printf(\"BIR? " + actionNum +
                  " %d\\n\"," + leaf.expr1 + ");");
    }
    // Generate the code that sets the array length
    printStatement(setLength.getCase(normal));
    resetTemp = true;
    setResult(specialize("_temp_"));
  }  
  /**
   * Translate an allocator.
   * <p>
   * When we translate the allocator expression, we spit out a
   * call to the _allocate() macro, which selects a free instance
   * of the collection and assigns the instance index to _temp_.
   * We then just return "_temp_" as the value of this expression
   * (this is OK since allocators must appear alone on the RHS
   * of an assignment action).
   */

  public void caseNewExpr(NewExpr expr) {
    StateVar target = expr.getCollection();
    int size = ((Collection) target.getType()).getSize().getValue();
    int locNum = currentTrans.getFromLoc().getId();
    int transNum = currentTrans.getFromLoc().getOutTrans().indexOf(
                     currentTrans);
    // Call macro _allocate(collection,refindex,size,locNum,transNum,actionNum)
    println("_allocate(" + target.getName() + "," +
            refIndex(target) + "," + size + "," + locNum + "," +
            transNum + "," + actionNum + ");");
    resetTemp = true;
    setResult(specialize("_temp_"));
  }  
  public void caseNotExpr(NotExpr expr) {
    translateUnaryOp(expr.getOp(), "! ");
  }  
  public void caseNullExpr(NullExpr expr) {
    setResult(specialize("0"));
  }  
  public void caseOrExpr(OrExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " || ");
  }  
  /**
   * Translate BIR Print action.
   * <p>
   * Perhaps remove this---easier to just get output from BIR trace instead.
   */

  public void casePrintAction(PrintAction printAction) {
    if (printAction.getPrintItems().size() > 0) {
      String format = "BIR|";
      String params = "";
      Vector printItems = printAction.getPrintItems();
      for (int i = 0; i < printItems.size(); i++) {
        Object item = printItems.elementAt(i);
        if (item instanceof String)
          format += item;
        else {
          format += "%d";
          CaseNode varTree = (CaseNode) applyTo((Expr) item);
          params +=
            "," + ((ExprNode) varTree.getCase(normal)).expr1;
        }
      }
      println("printf(\"" + format + "\\n\"" + params + "); ");
    }
  }  
  /**
   * Translate field selector.
   */

  public void caseRecordExpr(RecordExpr expr) {
    TreeNode result = applyTo(expr.getRecord());
    String field = expr.getField().getName();
    Vector leaves = result.getLeaves(new Vector());
    for (int i = 0; i < leaves.size(); i++) {
      ExprNode leaf = (ExprNode) leaves.elementAt(i);
      leaf.update(leaf.expr1 + "." + field);
    }
    setResult(result);
  }  
  public void caseRefExpr(RefExpr expr) {
    setResult(specialize("_ref(" + refIndex(expr.getTarget()) + ",0)"));
  }  
  public void caseRemExpr(RemExpr expr) {
    TreeNode e1Tree = applyTo(expr.getOp1());
    TreeNode e2Tree = applyTo(expr.getOp2());
    TreeNode result = e1Tree.compose(e2Tree, null);
    Vector leafCases = result.getLeafCases(new Vector());
    for (int i = 0; i < leafCases.size(); i++) {
      Case leafCase = (Case) leafCases.elementAt(i);
      ExprNode leaf = (ExprNode) leafCase.node;
      leafCase.insertTrap(leaf.expr2 + " == 0", "ArithmeticException",
                          true);
      leaf.update("(" + leaf.expr1 + " % " + leaf.expr2 + ")");
    }
    setResult(result);
  }  
  public void caseStateVar(StateVar expr) {
    setResult(specialize(expr.getName()));
  }  
  public void caseSubExpr(SubExpr expr) {
    translateBinaryOp(expr.getOp1(), expr.getOp2(), " - ");
  }  
  /**
   * Translate thread action.
   */

  public void caseThreadAction(ThreadAction threadAction) {
    String opName =
      ThreadAction.operationName(threadAction.getOperation());
    int threadId = threadAction.getThreadArg().getId();
    println("_" + opName + "Thread_" + threadId + ";");
  }  
  /**
   * Translate thread location test.
   */

  public void caseThreadLocTest(ThreadLocTest threadLocTest) {
    String threadName = threadLocTest.getThread().getName();
    int threadId = 1 + threadLocTest.getThread().getId();
    String locLabel = locLabel(threadLocTest.getLocation());
    // PROMELA syntax:  thread[pid]@labal
    String test = threadName + "[" + threadId + "]@" + locLabel;
    setResult(specialize(test));
  }  
  /**
   * Translate thread test.
   */

  public void caseThreadTest(ThreadTest threadTest) {
    switch (threadTest.getOperation()) {
      case THREAD_TERMINATED:
        String opName = ThreadTest.operationName(
                          threadTest.getOperation());
        int threadId = threadTest.getThreadArg().getId();
        // Just call the #define'd macro for this thread
        String test = "_" + opName + "_" + threadId;
        setResult(specialize(test));
        return;
    }
  }  
public String check() {
    String systemName = system.getName();
    String promFilename = systemName + ".prom";
    String trailFilename = promFilename + ".trail";

    if (options.ApplyNeverClaim) {
        // Translate LTL into never claim
        String ltlFilename = systemName + ".ltl";
        File ltlFile = new File(ltlFilename);
        if (!ltlFile.exists())
            throw new RuntimeException("Cannot find LTL file: "+ltlFile.getAbsolutePath());

        try {
            String neverClaim = BanderaUtil.exec("spin -F " + ltlFilename, true);
            PrintWriter pw = new PrintWriter(new FileWriter(systemName + ".nvr"));
            pw.print(neverClaim);
            pw.flush();
            pw.close();
        } catch (Exception e)
        {
            throw new RuntimeException("Cannot produce file '"+systemName+"',");
        }
    }

    File sourceFile = new File(promFilename);
    if (!sourceFile.exists())
        throw new RuntimeException("Cannot find SPIN source file: " + sourceFile.getAbsolutePath());

    /* // Execute cpp
    execAndWait("cpp -P " + promFilename + " tmp", true);
    File promFile = new File(promFilename);
    if (!promFile.delete() || !new File("tmp").renameTo(promFile))
        throw new RuntimeException("Could not rename tmp to " + promFilename);
    */

    StringBuffer output = new StringBuffer();

    try {
        output.append(BanderaUtil.exec("spin -a " + promFilename, isVerbose));
        if (!(new File("pan.c")).exists()) throw new RuntimeException();
    } catch (Exception e) {
        cleanMess();
        throw new RuntimeException("Could not produce pan.c file!");
    }

    try {
        output.append(BanderaUtil.exec(ccName + " -O3 " + options.compileOptions2() + " -o pan.exe pan.c", isVerbose));
        if (!(new File("pan.exe")).exists()) throw new RuntimeException();
    } catch (Exception e) {
        cleanMess();
        throw new RuntimeException("Could not compile pan.c!");
    }

    String panOutput;
    try {
        // Return output of 'pan'
        panOutput = BanderaUtil.exec("pan.exe " + options.panOptions(), isVerbose);
        output.append(panOutput);
    } catch (Exception e)
    {
         try {
                cleanMess();
         } catch (Exception exx){}
        throw new RuntimeException("Failed to run pan.exe!");
    }
    cleanMess();

    if (panOutput.indexOf("error : max search depth too small") >= 0) {
        throw new RuntimeException("Verifier search depth exceeded!");
    } else if (panOutput.indexOf("error : out of memory") >= 0) {
        throw new RuntimeException("Verifier ran out of memory!");
    } else if (panOutput.indexOf("error : VECTORSZ is too small") >= 0) {
        throw new RuntimeException("Verifier vector exceeded!");
    } else if (panOutput.indexOf("Search not completed") >= 0 && panOutput.indexOf("pan: wrote") < 0) {
         // Search not complete, but it doesn't write any counter example trail
        throw new RuntimeException("Verifier cannot complete its run:"+System.getProperty("line.separator")+panOutput);
    }

    try {
        BanderaUtil.moveFile(trailFilename, outputDir);
    } catch (Exception e)
    {
        throw new RuntimeException("Cannot move the counter example trail into the output directory!");
    }

    return output.toString();
}
private void cleanMess()
{
    // Sweep
    String systemName = system.getName();
    String ltlFilename = systemName + ".ltl";
    String nvrFilename = systemName + ".nvr";
    String promFilename = systemName + ".prom";
    String birFilename = systemName + ".bir";
    String trailFilename = promFilename + ".trail";

    if (!".".equals(outputDir) && !("."+File.separator).equals(outputDir))
    {
        new File(outputDir+birFilename).delete();
        new File(outputDir+ltlFilename).delete();
        new File(outputDir+nvrFilename).delete();
        new File(outputDir+promFilename).delete();
        new File(outputDir+trailFilename).delete();
        new File(outputDir+"pan.exe").delete();
        new File(outputDir+"pan.b").delete();
        new File(outputDir+"pan.c").delete();
        new File(outputDir+"pan.h").delete();
        new File(outputDir+"pan.m").delete();
        new File(outputDir+"pan.t").delete();
    }
    BanderaUtil.moveFile(birFilename, outputDir);
    BanderaUtil.moveFile(ltlFilename, outputDir);
    BanderaUtil.moveFile(nvrFilename, outputDir);
    BanderaUtil.moveFile(promFilename, outputDir);
    BanderaUtil.moveFile(trailFilename, outputDir);
    BanderaUtil.moveFile("pan.exe", outputDir);
    BanderaUtil.moveFile("pan.b", outputDir);
    BanderaUtil.moveFile("pan.c", outputDir);
    BanderaUtil.moveFile("pan.h", outputDir);
    BanderaUtil.moveFile("pan.m", outputDir);
    BanderaUtil.moveFile("pan.t", outputDir);
}

  static String currentDir() {
    return System.getProperty("user.dir");
  }  
  public void defaultCase(Object obj) {
    throw new RuntimeException("Trans type not handled: " + obj);
  }  
  /**
   * Generate constant and type definitions (using type namer).
   */

  void definitions() {
    Vector definitions = system.getDefinitions();

    // For each Constant, generate a #define
    for (int i = 0; i < definitions.size(); i++) {
      Definition def = (Definition) definitions.elementAt(i);
      if (def instanceof Constant)
        println("#define " + def.getName() + " " + def.getDef());
    }

    Vector types = system.getTypes();
    for (int i = 0; i < types.size(); i++) {
      Type type = (Type) types.elementAt(i);
      // For non-composite types, generate a #define for the type name
      if (type.isKind(BOOL | RANGE | LOCK | ENUMERATED | REF)) {
        println("/* " + type.typeName() + " = " + type + " */");
        print("#define " + type.typeName() + " ");
        type.apply(namer, this);
        println((String) namer.getResult());
        // For enumerated types, also #define the named constants
        if (type.isKind(ENUMERATED)) {
          Enumerated enum = (Enumerated) type;
          for (int j = 0; j < enum.getEnumeratedSize(); j++) {
            String name = enum.getNameOf(
                            enum.getFirstElement() + j);
            if (name != null)
              println("#define " + name + " " +
                      (enum.getFirstElement() + j));
          }
        }
      }
    }

    // For composite types (record, array, collection), generate
    // a typedef (struct).
    for (int i = 0; i < types.size(); i++) {
      Type type = (Type) types.elementAt(i);
      if (! type.isKind(BOOL | RANGE | LOCK | ENUMERATED | REF)) {
        println("/* " + type.typeName() + " = " + type + " */");
        print("typedef " + type.typeName() + " ");
        type.apply(namer, this);
        println((String) namer.getResult());
      }
    }
    println();
  }  
/**
 * getCounterExample method comment.
 */
public List getCounterExample() {
    String systemName = system.getName();
    String baseName = outputDir + systemName;
    String promFilename = baseName + ".prom";
    String trailFilename = promFilename + ".trail";

    File trail = new File(trailFilename);
    if (!trail.exists())
    {
         return null;
/*       trail = new File(outputDir+"."+systemName+".prom.trail");
         if (!trail.exists()) return null;
         trail.renameTo(new File(trailFilename));
*/
    }

    String output = BanderaUtil.exec("spin -t " + promFilename, true);
    BufferedReader reader = new BufferedReader(new StringReader(output));
    LinkedList ll = new LinkedList();
    String ln = System.getProperty("line.separator");
    try {
        String line;
        do {
            line = reader.readLine();
            if (line != null && line.trim().startsWith("BIR")) ll.add(line.trim());
        } while (line != null);
    } catch (Exception e)
    {
    }
    return ll;
}
  /**
   * Retrieve simple result from translator, flag error if not simple.
   * <p>
   * A simple result is a case tree with only a single expression
   * node under the NORMAL case.
   */

  String getSimpleResult() {
    TreeNode result = ((CaseNode) getResult()).getCase(normal);
    if (result instanceof ExprNode)
      return ((ExprNode) result).expr1;
    else
      throw new RuntimeException("Result not simple: " + result);
  }  
  public SpinOptions getSpinOptions() {
    return options;
  }  
  /**
   * Test if guard is present.
   * <p>
   * If the guard is TRUE (BoolLit) or the HAS_LOCK test (which we
   * don't use), claim there is no guard.
   */

  boolean guardPresent(Transformation trans) {
    Expr guard = trans.getGuard();
    if (guard == null)
      return false;
    if (guard instanceof BoolLit)
      return ! ((BoolLit) guard).getValue();
    if ((guard instanceof LockTest) &&
        ((LockTest) guard).getOperation() == HAS_LOCK)
      return false;
    return true;
  }  
  /**
   * Generate the header for all PROMELA files
   */

  void header() {
    ThreadVector threadVector = system.getThreads();

    println("/*  Promela for transition system: " +
            system.getName() + " */");
    println();

    // Lock types (R = reentrant, W = waiting)
    println("/* Lock operations */");
    println("#define LOCK 0");
    println("typedef lock_ {\n  chan lock = [1] of { bit };\n  byte owner;\n};");
    println("typedef lock_RW {\n  chan lock = [1] of { bit };\n  byte owner;\n  int waiting;\n  byte count;\n};");
    println("typedef lock_W {\n  chan lock = [1] of { bit };\n  byte owner;\n  int waiting;\n};");
    println("typedef lock_R {\n  chan lock = [1] of { bit };\n  byte owner;\n  byte count;\n};");

    // Monitor operations - most have separate reentrant version (_R)
    println("#define _lock(sync,locNum,transNum,actionNum) \\");
    println("  sync.lock?LOCK; sync.owner = _pid ");
    println("#define _lock_R(sync,locNum,transNum,actionNum) \\");
    println("  if \\");
    println("  :: sync.owner == _pid -> sync.count++; \\");
    println("  :: else -> sync.lock?LOCK; sync.owner = _pid; \\");
    println("  fi ");

    println("#define _unlock(sync,locNum,transNum,actionNum) \\");
    println("  sync.owner = 0; sync.lock!LOCK ");
    println("#define _unlock_R(sync,locNum,transNum,actionNum) \\");
    println("  if \\");
    println("  :: sync.count > 0 -> sync.count--; \\");
    println("  :: else -> sync.owner = 0; sync.lock!LOCK; \\");
    println("  fi ");

    println("#define _lockAvailable(sync) \\");
    println("  nempty(sync.lock)");
    println("#define _lockAvailable_R(sync) \\");
    println("  (nempty(sync.lock) || sync.owner == _pid) ");

    println("#define _unwait(sync,locNum,transNum,actionNum) \\");
    println("  sync.lock?LOCK; sync.owner = _pid ");
    println("#define _unwait_R(sync,locNum,transNum,actionNum) \\");
    println("  sync.lock?LOCK; sync.owner = _pid; sync.count = _temp_; _temp_ = 0 ");

    println("#define _notifyAll(sync,locNum,transNum,actionNum) \\");
    println("  if \\");
    println("  :: sync.owner == _pid -> sync.waiting = 0; \\");
    println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\\n\"); assert(0); \\");
    println("  fi ");

    println("#define _notify(sync,locNum,transNum,actionNum) \\");
    println("  if \\");
    for (int i = 0; i < threadVector.size(); i++) {
      int thread = (1 << i);
      println("  :: (sync.owner == _pid) && (sync.waiting & " +
              thread + ") -> sync.waiting = sync.waiting & " +
              ~ thread + " ; printf(\"BIR? %d " + i + "\",actionNum); \\");
    }
    println(
      "  :: (sync.owner == _pid) && (sync.waiting == 0) -> printf(\"BIR? %d " +
      threadVector.size() + "\\n\",actionNum); \\");
    println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\\n\"); assert(0); \\");
    println("  fi  ");

    for (int i = 0; i < threadVector.size(); i++) {
      int thread = (1 << i);

      println("#define _wait_" + i + "(sync,locNum,transNum,actionNum) \\");
      println("  if \\");
      println(
        "  :: sync.owner == _pid -> sync.waiting = sync.waiting | " +
        thread + ";  \\");
      println("       sync.owner = 0; sync.lock!LOCK; \\");
      println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\\n\"); assert(0); \\");
      println("  fi ");
      println("#define _wait_" + i + "_R(sync,locNum,transNum,actionNum) \\");
      println("  if \\");
      println(
        "  :: sync.owner == _pid -> sync.waiting = sync.waiting | " +
        thread + ";  \\");
      println("       _temp_ = sync.count; sync.count = 0; sync.owner = 0; sync.lock!LOCK; \\");
      println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\\n\"); assert(0); \\");
      println("  fi ");

      println("#define _wasNotified_" + i + "(sync) \\");
      println("  !(sync.waiting & " + thread + ") ");

      // Thread operations
      if (! threadVector.elementAt(i).isMain()) {
        println("#define _startThread_" + i + " \\");
        println("  _threadActive_" + i +
                " = true; _threadStart_" + i + "!LOCK");
        println("#define _beginThread_" + i + " \\");
        println("  _threadStart_" + i + "?LOCK");
        println("#define _joinThread_" + i + " \\");
        println("  skip");
        println("#define _exitThread_" + i + " \\");
        println("  _threadActive_" + i + " = 0; goto endtop_" + i);
        println("#define _threadTerminated_" + i + " \\");
        println("  (_threadActive_" + i + " == 0)");
      }
    }

    // Reference macros
    println();
    println("/* Reference operations */");
    println("#define _collect(r) (r >> 8)");
    println("#define _index(r) (r & 255)");
    println("#define _ref(c,i) ((c << 8) | i)");

    // Allocator macro
    //   _i_ is always zero outside of this macro
    println("#define _allocate(collection,refindex,maxsize,locNum,transNum,actionNum) \\");
    println("  do \\");
    println("  :: collection.inuse[_i_] -> \\");
    println("     _i_ = _i_ + 1; \\");
    println("     if  \\");
    println("     :: _i_ == maxsize -> printf(\"BIR: locNum transNum actionNum  CollectionSizeLimitException\\n\"); limit_exception = 1; _i_ = 0; goto endtrap; \\");
    println("     :: else \\");
    println("     fi; \\");
    println("  :: else -> \\");
    println("     collection.inuse[_i_] = 1; \\");
    println("     _temp_ = _ref(refindex,_i_);  \\");
    println("     _i_ = 0;  \\");
    println("     break;  \\");
    println("  od ");
    println();
    println("#define TRAP 1");
    println();
  }  
  /**
   * Generate init {} block to initializae variables and start threads.
   */

  void initBlock() {
    ThreadVector threadVector = system.getThreads();
    println("init {");
    indentLevel = 2;
    println("atomic {");
    indentLevel++;
    StateVarVector stateVarVector = system.getStateVars();

    // Use variable initializer to init each state var
    SpinTypeInit initializer = new SpinTypeInit(this, out);
    for (int i = 0; i < stateVarVector.size(); i++) {
      StateVar var = stateVarVector.elementAt(i);
      var.getType().apply(initializer, var);
    }

    // Start each thread proctype (making sure its ID is
    // what we think it should be---else the location tests will fail).
    for (int i = 0; i < threadVector.size(); i++) {
      BirThread thread = threadVector.elementAt(i);
      println("assert(run " + thread.getName() + "() == " +
              (1 + thread.getId()) + ");");
    }
    indentLevel--;
    println("}");

    // Afterwards, just hang out asserting that there is no limit
    // exception (i.e., a limit exception will cause a counterexmaple).
    // This statement is not emitted in the PROMELA if
    // the user wants to do a resource bounded check.
    if (!options.getResourceBounded())
      println("assert(! limit_exception);");
    indentLevel = 0;
    println("}");

  }  
  /**
   * Test if the out transitions of a location model an 'if' branch,
   * i.e., there are exactly two transitions, and one guard is
   * the negation of the other.
   */

  boolean isIfBranch(TransVector outTrans) {
    if (outTrans.size() != 2)
      return false;
    Expr guard1 = outTrans.elementAt(0).getGuard();
    Expr guard2 = outTrans.elementAt(1).getGuard();
    if (guard1 == null || guard2 == null)
      return false;
    if ((guard1 instanceof NotExpr) &&
        ((NotExpr) guard1).getOp().equals(guard2))
      return true;
    if ((guard2 instanceof NotExpr) &&
        ((NotExpr) guard2).getOp().equals(guard1))
      return true;
    return false;
  }  
    public boolean isVerbose() { return isVerbose; }
  /**
   * Get PROMELA label for BIR location.
   * <p>
   * If location has no out transitions (i.e., is end location of thread),
   * make the label an end-label (does not count for deadlock).
   */

  static String locLabel(Location loc) {
    if (loc.getOutTrans().size() == 0)
      return "endloc_" + loc.getId();
    else
      return "loc_" + loc.getId();
  }  
  /**
   * Get PROMELA label of location encountered during coarsening.
   * <p>
   * Since we may encounter the same location along several
   * collapsed paths, we must have a unique label for each.
   */

  static String locLabel(Location loc1, int branch, Location loc2) {
    return "loc_" + loc1.getId() + "_" + branch + "_" + loc2.getId();
  }  
  /**
   * Test if an expression is statically nonnegative (either a constant
   * or in a range type that is nonnegative).
   */

  boolean nonNegative(Expr expr) {
    if (expr instanceof ConstExpr)
      return ((ConstExpr) expr).getValue() >= 0;
    if (expr.getType() instanceof Range) {
      Range type = (Range) expr.getType();
      return (type.getFromVal().getValue() >= 0);
    }
    return false;
  }  
  static int parseInt(String s) {
    try {
      int result = Integer.parseInt(s);
      return result;
    } catch (NumberFormatException e) {
      throw new RuntimeException("Integer didn't parse: " + s);
    }
  }  

  /**
    * Parse the output of 'pan' and interpret it as either a violation
    * (sequence of transformations) or as a error-free analysis.
    * <p>
    * @return a vector of transformations (if there was an error found), or null (otherwise)
    */

  public BirTrace parseOutput() {
    return new BirTrace(system, getCounterExample());
  }          
  /**
   * Generate the predicate definitions.
   * <p>
   * Note that these are at the bottom so they can refer to
   * any variable or code location.
   */

  void predicates() {
    println("/* Predicates */");
    Vector preds = system.getPredicates();
    for (int i = 0; i < preds.size(); i++) {
      Expr pred = (Expr) preds.elementAt(i);
      String name = system.predicateName(pred);
      inDefine = true;
      println("#define " + name + " ");
      indentLevel = 1;
      // Print the PROMELA expression
      printGuard(applyTo(pred).getCase(normal));
      inDefine = false;
      println("");
      indentLevel = 0;
    }
    println("");
  }  
  /**
   * Support for printing things nicely indented.
   */

  void print(String s) {
    if (newLine) { // at start of line---indent
      for (int i = 0; i < indentLevel; i++)
        out.print("   ");
      newLine = false;
    }
    out.print(s);
  }  
  /**
   * Print a case tree as an expression to represent a guard.
   * <p>
   * We take advantage of the short-curcuit evaluation in PROMELA
   * to express a case tree as one large boolean expression.
   * A case node:
   * <pre>
   * (cond1 => expr1, cond2 => expr2, ...)
   * </pre>
   * is translated as
   * <pre>
   * ((cond1 && expr1) || (cond2 && expr2) || ... )
   * </pre>
   * We consider traps as always enabled, so they evaluate to
   * the constant TRAP (#defined to be 1).
   */

  void printGuard(TreeNode tree) {
    if (tree instanceof ExprNode) {
      ExprNode node = (ExprNode) tree;
      print(node.expr1);
    } else if (tree instanceof TrapNode) {
      TrapNode node = (TrapNode) tree;
      print("TRAP");
    } else {
      CaseNode node = (CaseNode) tree;
      print("(  ");
      for (int i = 0; i < node.size(); i++) {
        Case c = node.elementAt(i);
        indentLevel++;
        println("(  " + c.cond);
        print("&& ");
        indentLevel++;
        printGuard(c.node);
        indentLevel--;
        print(" )");
        indentLevel--;
        if (i < node.size() - 1) {
          println();
          print("|| ");
        }
      }
      println(" )");
    }
  }  
  void println() {
    if (inDefine)
      out.print("\\"); // must use line continuation in #define
    out.println();
    newLine = true;
  }  
  void println(String s) {
    print(s);
    println();
  }  
  /**
   * Print a case tree as a statement.
   * <p>
   * A case node:
   * <pre>
   * (cond1 => expr1, cond2 => expr2, ..., condN => exprN)
   * </pre>
   * is translated as
   * <pre>
   * if
   * :: cond1 -> expr1
   * :: cond2 -> expr2
   * ...
   * else -> exprN
   * fi
   * </pre>
   */

  void printStatement(TreeNode tree) {
    if (tree instanceof ExprNode) {
      ExprNode node = (ExprNode) tree;
      println(node.expr1);
    } else if (tree instanceof TrapNode) {
      TrapNode node = (TrapNode) tree;
      print("   printf(\"BIR: " + actionId() + " " + node.desc +
            "\\n\"); ");
      // If fatal trap, flag error, else just branch to end label
      if (node.fatal)
        println("assert(0);");
      else
        println("limit_exception = 1; goto endtrap;");
    } else {
      CaseNode node = (CaseNode) tree;
      println("if ");
      for (int i = 0; i < node.size(); i++) {
        Case c = node.elementAt(i);
        // Use "else" for last alternative
        String cond = (i < node.size() - 1) ? c.cond : "else";
        println(":: " + cond + " -> ");
        indentLevel++;
        printStatement(c.node);
        indentLevel--;
      }
      println("fi; ");
    }
  }  
  /**
   * Generate the #include for the never claim
   */

  void property() {
    if (options.ApplyNeverClaim)
      println("#include \"" + system.getName() + ".nvr\"");
  }  
  /**
   * Return the refIndex of a state variable (it's index in the
   * universal reference type refAny).
   */

  int refIndex(StateVar target) {
    return 1 + system.refAnyType().getTargets().indexOf(target);
  }  
  /**
   * Reset any variables that have become dead between locations.
   * <p>
   * In particular, we reset a variable if it was live at fromLoc and
   * is not live at toLoc.
   */

  void resetDeadVariables(Location fromLoc, Location toLoc) {
    StateVarVector liveBefore = fromLoc.getLiveVars();
    StateVarVector liveAfter = toLoc.getLiveVars();
    if (liveBefore != null && liveAfter != null)
      for (int i = 0; i < liveBefore.size(); i++)
        if (liveAfter.indexOf(liveBefore.elementAt(i)) == -1) {
          // var was live, now is not---reset it
          StateVar var = liveBefore.elementAt(i);
          var.apply(this);
          print(getSimpleResult() + " = ");
          var.getInitVal().apply(this);
          println(getSimpleResult() + ";");
        }
  }  
  /**
   * Run translator: generate header, definitions, state variables,
   * transitions (processes), predicates, and the LTL property.
   */

  SpinTrans run() {
    header();
    definitions();
    stateVariables();
    transitions();
    predicates();
    property();
    return this;
  }  
  /**
    * Run SPIN to generate an analyzer (pan), and then run the analyzer.
    * <p>
    * The translator must have been executed for the transition system
    * (the file NAME.prom must exist and contain the translated PROMELA).
    * @return the output of 'pan' (as a String)
    */

public String runSpin() {
    return check();
/*
    String systemName = system.getName();
    try {
      if (options.ApplyNeverClaim) {
    // Translate LTL into never claim
    String ltlFilename = systemName + ".ltl";
    File ltlFile = new File(ltlFilename);
    if (!ltlFile.exists())
      throw new RuntimeException( "Cannot find LTL file: " +
                      ltlFile.getAbsolutePath());
    String neverClaim =
      execAndWait("spin -F " + ltlFilename, true);
    PrintWriter pw =
      new PrintWriter(new FileWriter(systemName + ".nvr"));
    pw.print(neverClaim);
    pw.flush();
    pw.close();
      }
      String promFilename =
    isWindows ? systemName : systemName + ".prom";
      File sourceFile = new File(promFilename);
      if (!sourceFile.exists())
    throw new RuntimeException(
                   "Cannot find SPIN source file: " +
                   sourceFile.getAbsolutePath());

      { // Remove any old trail & pan.exe files
    new File(isWindows ? systemName + ".prom.trail" :
         systemName + ".tra").delete();
    new File("pan.exe").delete();
      }
      //      { // Execute cpp
      //        execAndWait("cpp -P " + promFilename + " tmp", true);
      //        File promFile = new File(promFilename);
      //      if (!promFile.delete() ||
      //            !new File("tmp").renameTo(promFile))
      //          throw new RuntimeException(
      //            "Could not rename tmp to " + promFilename);
      //        }
      execAndWait("spin -a " + promFilename, true);
      execAndWait(ccName + " " + options.compileOptions2() + " -o pan.exe pan.c",
          true);
      ranVerifier = true;
      // Return output of 'pan'
      return panOutput = execAndWait(isWindows ?
                     "pan.exe -ttra " + options.panOptions() :
                     "pan.exe " + options.panOptions(), true);
    } catch (Exception e) {
      throw new RuntimeException(
                 "Could not produce SPIN file (" + e + ")");
    }
*/
}            
    public void setVerbose(boolean v) { isVerbose = v; }
  /**
   * Build a trivial case tree with one ExprNode holding the string.
   */

  TreeNode specialize(String expr) {
    return new CaseNode(new Case(normal, new ExprNode(expr)));
  }  
  /**
   * Declare the state variables.
   */

  void stateVariables() {
    // limit_exeption is set on a BIR limit exception
    // _i_ is used as a temporary in the _allocate macro
    println("bool limit_exception = 0;");
    println("byte _i_ = 0;");

    // For each (non-main) thread, declare channel to block on for starting
    // the thread and a boolean indicating whether the thread is active
    ThreadVector threads = system.getThreads();
    for (int i = 0; i < threads.size(); i++) {
      if (! threads.elementAt(i).isMain()) {
        println("chan _threadStart_" + i + " = [1] of { bit };");
        println("bit _threadActive_" + i + ";");
      }
    }
    println();

    // For each state variable, declare it with its type.
    StateVarVector stateVarVector = system.getStateVars();
    for (int i = 0; i < stateVarVector.size(); i++) {
      StateVar var = stateVarVector.elementAt(i);
      var.getType().apply(namer, null);
      String refIndex = "   ";
      // Print ref index for composites to help reader
      if (var.getType().isKind(RECORD | ARRAY | COLLECTION))
        refIndex += "/*  ref index = " + refIndex(var) + " */";
      println((String) namer.getResult() + " " + var.getName() +
              ";" + refIndex);
    }
    println();
  }  
  /**
   * Generate the threads.
   * <p>
   * Each thread is a PROMELA proctype with a label for each
   * (visible) location and an if-case for each transformation
   * out of that location.
   */

  void transitions() {
    ThreadVector threadVector = system.getThreads();
    for (int i = 0; i < threadVector.size(); i++) {
      BirThread thread = threadVector.elementAt(i);
      println("proctype " + thread.getName() + "() { ");
      // Temp for thread
      println("  int _temp_;");
      // For non-main threads, insert code to block until started
      if (! thread.isMain())
        println("endtop_" + i + ":\n   _beginThread_" + i + ";");

      // Generate label/trans for each location
      LocVector threadLocVector = thread.getLocations();
      for (int j = 0; j < threadLocVector.size(); j++)
        translateLocation(threadLocVector.elementAt(j));

      // Special end location (accepting)
      println("endtrap:");
      // For resource bounded searches we cause the model checker to go into
      // an infinite loop when a limit resource execption has been raised.
      // Otherwise we simply denote a Promela end state (with a 0).
      if (options.getResourceBounded()) {
        println("   if");
        println("   :: limit_exception -> goto endtrap;");
        println("   :: !limit_exception -> 0;");
        println("   fi;");
      } else {
        println(" 0;");
      }
      println("}");
      println();
    }
    initBlock();
  }  
  /**
   * Generate PROMELA source representing a transition system.
   * <p>
   * As above, but with default options.
   * @param system the transition system
   * @return the SpinTrans control object
   */

  public static SpinTrans translate(TransSystem system) {
    return translate(system, null);
  }  
  /**
   * Generate PROMELA source representing a transition system.
   * <p>
   * The PROMELA is written to a file NAME.prom where NAME
   * is the name of the transition system.  A set of
   * options can be provided in a SpinOptions object.
   * @param system the transition system
   * @param options the SPIN verifier options
   * @return the SpinTrans control object
   */

  public static SpinTrans translate(TransSystem system, SpinOptions options) {
    return translate(system, options, ".");
  }      
  /**
   * Generate PROMELA source representing a transition system.
   * <p>
   * As above, but the PROMELA is written to the PrintWriter provided.
   * @param system the transition system
   * @param out the PrintWriter to write the PROMELA to
   * @return the SpinTrans control object
   */

public static SpinTrans translate(TransSystem system, SpinOptions options, PrintWriter out) {
    return (new SpinTrans(system, options, out)).run();
}
public static SpinTrans translate(TransSystem system, SpinOptions options, String outputDir) {
    try {
        if (outputDir == null || "".equals(outputDir)) outputDir = "."+File.separator; else
            if (!outputDir.endsWith(File.separator)) outputDir = outputDir + File.separator;

        // File sourceFile = new File(isWindows ? system.getName() : system.getName() + ".prom");
        File sourceFile = new File(system.getName() + ".prom");
        FileOutputStream streamOut = new FileOutputStream(sourceFile);
        PrintWriter writerOut = new PrintWriter(streamOut);
        SpinTrans result = translate(system, options, writerOut);
        result.outputDir = outputDir;
        writerOut.close();
        return result;
    } catch (IOException e) {
        throw new RuntimeException("Could not produce SPIN file: " + e);
    }
}  
  /**
   * Translate binary op
   */

  void translateBinaryOp(Expr e1, Expr e2, String op) {
    TreeNode e1Tree = applyTo(e1);
    TreeNode e2Tree = applyTo(e2);
    // Compose argument trees and then update each leaf
    TreeNode result = e1Tree.compose(e2Tree, null);
    Vector leaves = result.getLeaves(new Vector());
    for (int i = 0; i < leaves.size(); i++) {
      ExprNode leaf = (ExprNode) leaves.elementAt(i);
      leaf.update("(" + leaf.expr1 + op + leaf.expr2 + ")");
    }
    setResult(result);
  }  
  /**
   * Generate PROMELA for visible BIR location.
   */

  public void translateLocation(Location loc) {
    if (! loc.isVisible())
      return;
    println(locLabel(loc) + ":");
    indentLevel++;
    TransVector outTrans = loc.getOutTrans();
    // Don't both with 'if' when there's only one transition
    if (outTrans.size() == 1)
      translateSequence(outTrans.elementAt(0), 0);
    else if (outTrans.size() == 0)
      println("0;");
    else {
      println("if");
      for (int i = 0; i < outTrans.size(); i++) {
        print(":: ");
        indentLevel++;
        translateSequence(outTrans.elementAt(i), i);
        indentLevel--;
      }
      println("fi;");
    }
    indentLevel--;
  }  
  /**
   * Translate a sequence of transformations starting with the given one,
   * continuing until we hit a visible transformation.
   * <p>
   * The locSet param keeps track of the locations we've encountered
   * in this branch (i.e., this atomic block).  If we transition to
   * an invisible location in this set, we just generate a goto to the local
   * label for that location, otherwise we recursively call translateSeq
   * to continue following the sequence.
   * <p>
   * If we transition to a visible location, we always generate a goto
   * to the top-level location label for that location.
   * <p>
   * The guard of the transformation may be supressed by setting
   * param supressGuard.  This is used when an 'if' branch pattern
   * is detected (two transitions, one on expression E, the other
   * on expression !E).
   */

  void translateSeq(LocVector locSet, Transformation trans,
                    int branch, boolean supressGuard) {
    // Generate code for one transformation (possibly without the guard)
    translateTrans(trans, supressGuard);

    // If the target location is visible, reset the dead variables
    // and branch to the code for that location
    if (trans.getToLoc().isVisible()) {
      resetDeadVariables(locSet.firstElement(), trans.getToLoc());
      println("goto " + locLabel(trans.getToLoc()) + ";");
    }

    // If the target location is invisible, but we've already
    // generated code for it in this atomic block, branch to
    // the local label for that location.
    else if (locSet.contains(trans.getToLoc()))
      println("goto " + locLabel(locSet.firstElement(), branch,
                                 trans.getToLoc()) + ";");

    // Otherwise, continue following the sequence
    else {
      locSet.addElement(trans.getToLoc());

      // If there's more than one way into this location, we
      // may branch back to it from within the atomic block, so
      // generate a local label for the location.
      if (trans.getToLoc().getInTrans().size() > 1)
        println( locLabel(locSet.firstElement(), branch,
                          trans.getToLoc()) + ":");
      TransVector successors = trans.getToLoc().getOutTrans();
      // For one sucessor, don't bother with an 'if'
      if (successors.size() == 1)
        translateSeq(locSet, successors.elementAt(0), branch,
                     false);
      // For 'if' branches, use a PROMELA 'else' for efficiency
      else if (isIfBranch(successors)) {
        println("if");
        print(":: ");
        indentLevel++;
        translateSeq(locSet, successors.elementAt(0), branch,
                     false);
        indentLevel--;
        print(":: else -> ");
        indentLevel++;
        translateSeq(locSet, successors.elementAt(1), branch, true);
        indentLevel--;
        println("fi;");
      } else { // general case
        println("if");
        for (int i = 0; i < successors.size(); i++) {
          print(":: ");
          indentLevel++;
          translateSeq(locSet, successors.elementAt(i),
                       branch, false);
          indentLevel--;
        }
        println("fi;");
      }
    }
  }  
  /**
   * Translate a sequence of transformations, continuing until
   * we hit a visible transformation.  Make the sequence
   * atomic.
   * <p>
   * The 'branch' parameter is used to generate location
   * labels that are local to this atomic block.
   */

  void translateSequence(Transformation trans, int branch) {
    Location startLoc = trans.getFromLoc();
    println("atomic { ");
    indentLevel++;
    translateSeq(new LocVector(startLoc), trans, branch, false);
    indentLevel--;
    println("}");
  }  
  /**
   * Generate code for a single transformation (possibly suppressing
   * the code for the guard expression).
   */

  void translateTrans(Transformation trans, boolean supressGuard) {
    // Set this trans as the context (for action ID generation)
    currentTrans = trans;
    actionNum = 0;
    // Translate and print the guard if present and not supressed
    if (! supressGuard && guardPresent(trans)) {
      printGuard(applyTo(trans.getGuard()).getCase(normal));
      println("-> ");
    }
    ActionVector actions = trans.getActions();
    // Translate each action
    for (int i = 0; i < actions.size(); i++) {
      actionNum = i + 1;
      println("printf(\"BIR: " + actionId() + " OK\\n\"); ");
      actions.elementAt(i).apply(this);
    }
    // If we used _temp_, reset it
    if (resetTemp) {
      println("_temp_ = 0;");
      resetTemp = false;
    }
  }  
  /**
   * Translate unary op
   */

  void translateUnaryOp(Expr e, String op) {
    TreeNode result = applyTo(e);
    Vector leaves = result.getLeaves(new Vector());
    // Translate argument and then apply to each leaf
    for (int i = 0; i < leaves.size(); i++) {
      ExprNode leaf = (ExprNode) leaves.elementAt(i);
      leaf.update("(" + op + leaf.expr1 + ")");
    }
    setResult(result);
  }  
}

---