DSpinTrans.java Source File

00001 package edu.ksu.cis.bandera.dspin;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 1998, 1999   James Corbett (corbett@hawaii.edu)     *
00006  * All rights reserved.                                              *
00007  *                                                                   *
00008  * This work was done as a project in the SAnToS Laboratory,         *
00009  * Department of Computing and Information Sciences, Kansas State    *
00010  * University, USA (http://www.cis.ksu.edu/santos).                  *
00011  * It is understood that any modification not identified as such is  *
00012  * not covered by the preceding statement.                           *
00013  *                                                                   *
00014  * This work is free software; you can redistribute it and/or        *
00015  * modify it under the terms of the GNU Library General Public       *
00016  * License as published by the Free Software Foundation; either      *
00017  * version 2 of the License, or (at your option) any later version.  *
00018  *                                                                   *
00019  * This work is distributed in the hope that it will be useful,      *
00020  * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
00021  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
00022  * Library General Public License for more details.                  *
00023  *                                                                   *
00024  * You should have received a copy of the GNU Library General Public *
00025  * License along with this toolkit; if not, write to the             *
00026  * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
00027  * Boston, MA  02111-1307, USA.                                      *
00028  *                                                                   *
00029  * Java is a trademark of Sun Microsystems, Inc.                     *
00030  *                                                                   *
00031  * To submit a bug report, send a comment, or get the latest news on *
00032  * this project and other SAnToS projects, please visit the web-site *
00033  *                http://www.cis.ksu.edu/santos                      *
00034  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00035 import Bandera;
00036 import java.io.*;
00037 import java.util.Properties;
00038 import java.util.Vector;
00039 import java.util.StringTokenizer;
00040 import java.util.List;
00041 import java.util.LinkedList;
00042 
00043 import edu.ksu.cis.bandera.bir.*;
00044 import edu.ksu.cis.bandera.spin.*;
00045 import edu.ksu.cis.bandera.checker.*;
00046 
00047 /**
00048  * DSpinTrans is the main class of the dSPIN translator, which generates
00049  * PROMELA source representing a transition system.
00050  * <p>
00051  * The dSPIN translator is invoked on a transition system as follows:
00052  * <pre>
00053  * // Parameters 
00054  * TransSystem system = ...;   // the transition system
00055  * DSpinOptions options = new DSpinOptions();   // SPIN options
00056  * options.setMemoryLimit(256);            // set various options
00057  * ...
00058  * DSpinTrans spin = DSpinTrans.translate(system,options); // invoke translator
00059  * spin.runSpin();                           // Run SPIN on generated PROMELA
00060  * BirTrace trace = spin.parseOutput();      // Parse output as BIR trace
00061  * </pre>
00062  */
00063 
00064 public class DSpinTrans extends AbstractExprSwitch implements BirConstants, Checker
00065 {
00066     TransSystem system;
00067     PrintWriter out;
00068     DSpinTypeName namer;
00069     int indentLevel = 0;
00070     boolean inDefine = false;
00071     boolean newLine = true;
00072     boolean resetTemp = false;
00073     boolean resetNew = false;
00074     Transformation currentTrans;
00075     int actionNum;
00076     DSpinOptions options;
00077     boolean ranVerifier = false;
00078 
00079     static String ccName = "gcc";
00080     static String includeDir = "";
00081     static Runtime runtime = Runtime.getRuntime();
00082     public static final String normal = "NORMAL_CASE";
00083     
00084     static final int BUFSIZE = 50000;
00085     static byte [] buffer = new byte[BUFSIZE];
00086 
00087     static {
00088         /*
00089         includeDir = Bandera.getProperty("dspin.include");
00090         */
00091     }
00092     DSpinTrans(TransSystem system, DSpinOptions options, PrintWriter out) {
00093     this.system = system;
00094     this.out = out;
00095     this.namer = new DSpinTypeName();
00096     this.options = (options == null) ? new DSpinOptions() : options;
00097     }
00098     String actionId() {
00099     int locNum = currentTrans.getFromLoc().getId();
00100     int transNum = 
00101         currentTrans.getFromLoc().getOutTrans().indexOf(currentTrans);
00102     return locNum + " " + transNum + " " + actionNum;
00103     }
00104     String actionIdWithCommas() {
00105     int locNum = currentTrans.getFromLoc().getId();
00106     int transNum = 
00107         currentTrans.getFromLoc().getOutTrans().indexOf(currentTrans);
00108     return locNum + "," + transNum + "," + actionNum;
00109     }
00110     CaseNode applyTo(Expr expr) {
00111     expr.apply(this);
00112     return (CaseNode) getResult();
00113     }
00114     public void caseAddExpr(AddExpr expr)
00115     {
00116     translateBinaryOp(expr.getOp1(), expr.getOp2(), " + ");
00117     }
00118     public void caseAndExpr(AndExpr expr)
00119     {
00120     translateBinaryOp(expr.getOp1(), expr.getOp2(), " && ");
00121     }
00122     public void caseArrayExpr(ArrayExpr expr)
00123     {
00124     String ref = "";  // Need extra deref for arrays of Refs
00125     if (expr.getType().isKind(REF))
00126         ref = ".ref";
00127     TreeNode arrayTree = applyTo(expr.getArray());
00128     TreeNode indexTree = applyTo(expr.getIndex());
00129     TreeNode result = arrayTree.compose(indexTree,null);
00130     Vector leafCases = result.getLeafCases(new Vector());
00131     for (int i = 0; i < leafCases.size(); i++) {
00132         Case leafCase = (Case) leafCases.elementAt(i);
00133         ExprNode leaf = (ExprNode) leafCase.node;
00134         leafCase.insertTrap(leaf.expr2 + " >= " + leaf.expr1 + ".length",
00135                 "ArrayIndexOutOfBoundsException",true);
00136         leafCase.insertTrap(leaf.expr2 + " < 0",
00137                 "ArrayIndexOutOfBoundsException",true);
00138         leaf.update(leaf.expr1 + ".elements[" + leaf.expr2 + "]" + ref);
00139     }
00140     setResult(result);
00141     }
00142     public void caseAssertAction(AssertAction assertAction) {
00143     CaseNode condTree = (CaseNode) applyTo(assertAction.getCondition());
00144     Vector leaves = condTree.getLeaves(new Vector());
00145     for (int i = 0; i < leaves.size(); i++) {
00146         ExprNode leaf = (ExprNode) leaves.elementAt(i);
00147         leaf.update("assert(" + leaf.expr1 + ");");
00148     }
00149     printStatement(condTree.getCase(normal));
00150     }
00151     public void caseAssignAction(AssignAction assign) 
00152     {
00153     TreeNode rhsTree = applyTo(assign.getRhs());
00154     TreeNode lhsTree = applyTo(assign.getLhs());
00155     CaseNode result = (CaseNode) lhsTree.compose(rhsTree,null);
00156     Vector leafCases = result.getLeafCases(new Vector());
00157     for (int i = 0; i < leafCases.size(); i++) {
00158         Case leafCase = (Case) leafCases.elementAt(i);
00159         ExprNode leaf = (ExprNode) leafCase.node;
00160         Type rhsType = assign.getRhs().getType();
00161         Type lhsType = assign.getLhs().getType();
00162         // Make run-time checks on assignment
00163         if (! rhsType.isSubtypeOf(lhsType)) {
00164 
00165         // Check subrange
00166         if (lhsType.isKind(RANGE)
00167             && ! lhsType.containsValue(assign.getRhs())) {
00168             Range range = (Range) lhsType;
00169             leafCase.insertTrap(leaf.expr2 + " < " 
00170                     + range.getFromVal(),
00171                     "RangeLimitException", false);
00172             leafCase.insertTrap(leaf.expr2 + " > " 
00173                     + range.getToVal(),
00174                     "RangeLimitException", false);
00175         }
00176 
00177         // Check ref assignment
00178         if (lhsType.isKind(REF)
00179             && ! (assign.getRhs() instanceof NullExpr)) {
00180             String trapDesc = "ClassCastException";
00181             StateVarVector lhsTargets = ((Ref)lhsType).getTargets();
00182             StateVarVector rhsTargets = ((Ref)rhsType).getTargets();
00183             for (int j = 0; j < rhsTargets.size(); j++) 
00184             if (! lhsTargets.contains(rhsTargets.elementAt(j))) {
00185                 String check = leaf.expr2 + ".refIndex == " +
00186                 refIndex(rhsTargets.elementAt(j));
00187                 leafCase.insertTrap(check,
00188                         "ClassCastException",true);
00189             }
00190         }
00191         }
00192         leaf.update(leaf.expr1 + " = " + leaf.expr2 + ";");
00193     }       
00194     printStatement(result.getCase(normal));
00195     }
00196     public void caseBoolLit(BoolLit expr)
00197     {
00198     setResult(specialize("" + expr.getValue()));
00199     }
00200     public void caseChooseExpr(ChooseExpr expr)
00201     {
00202     Vector choices = expr.getChoices();
00203     println("if");
00204     for (int i = 0; i < choices.size(); i++) {
00205         Expr choice = (Expr) choices.elementAt(i);
00206         ExprNode leaf = (ExprNode) applyTo(choice).getCase(normal);
00207         println(":: _temp_ = " + leaf.expr1 + "; printf(\"BIR? " +
00208             actionNum + " " + i + "\\n\"); ");
00209     }
00210     println("fi;");
00211     resetTemp = true;
00212     setResult(specialize("_temp_"));        
00213     }
00214     public void caseConstant(Constant expr)
00215     {
00216     setResult(specialize(expr.getName()));
00217     }
00218     public void caseDerefExpr(DerefExpr expr)
00219     {
00220     TreeNode result = applyTo(expr.getTarget());
00221     StateVarVector targets = 
00222         ((Ref)expr.getTarget().getType()).getTargets();
00223     Vector leafCases = result.getLeafCases(new Vector());
00224     for (int i = 0; i < leafCases.size(); i++) {
00225         Case leafCase = (Case) leafCases.elementAt(i);
00226         ExprNode leaf = (ExprNode) leafCase.node;
00227         CaseNode caseNode = new CaseNode();
00228         String cond = "(" + leaf.expr1 + " != null)";
00229         caseNode.addCase(cond, leaf.expr1);
00230         cond = "(" + leaf.expr1 + " == null)";
00231         caseNode.addTrapCase(cond,"NullPointerException", true);
00232         leafCase.replace(caseNode);
00233     }
00234     setResult(result);
00235     }
00236     public void caseDivExpr(DivExpr expr)
00237     {   
00238     TreeNode e1Tree = applyTo(expr.getOp1());
00239     TreeNode e2Tree = applyTo(expr.getOp2());
00240     TreeNode result = e1Tree.compose(e2Tree,null);
00241     Vector leafCases = result.getLeafCases(new Vector());
00242     for (int i = 0; i < leafCases.size(); i++) {
00243         Case leafCase = (Case) leafCases.elementAt(i);
00244         ExprNode leaf = (ExprNode) leafCase.node;
00245         leafCase.insertTrap(leaf.expr2 + " == 0",
00246                 "ArithmeticException",true);
00247         leaf.update("(" + leaf.expr1 + " / " + leaf.expr2 + ")");
00248     }
00249     setResult(result);
00250     }
00251     public void caseEqExpr(EqExpr expr)
00252     {
00253         translateBinaryOp(expr.getOp1(), expr.getOp2(), " == ");
00254     }
00255     public void caseInstanceOfExpr(InstanceOfExpr expr)
00256     {
00257     TreeNode result = applyTo(expr.getRefExpr());
00258     StateVarVector targets = expr.getRefType().getTargets();
00259     Vector leafCases = result.getLeafCases(new Vector());
00260     for (int i = 0; i < leafCases.size(); i++) {
00261         Case leafCase = (Case) leafCases.elementAt(i);
00262         ExprNode leaf = (ExprNode) leafCase.node;
00263         CaseNode caseNode = new CaseNode();
00264         String elseCond = "! (";
00265         for (int j = 0; j < targets.size(); j++) {
00266         StateVar target = targets.elementAt(j);
00267         String cond = "(" + leaf.expr1 + ".refIndex == " 
00268             + refIndex(target) + ")";
00269         caseNode.addCase(cond,"1");
00270         if (j > 0) elseCond += " || ";
00271         elseCond += cond;
00272         }
00273         elseCond += ")";
00274         caseNode.addCase(elseCond,"0");
00275         leafCase.replace(caseNode);
00276     }
00277     setResult(result);
00278     }
00279     public void caseIntLit(IntLit expr)
00280     {
00281     setResult(specialize("" + expr.getValue()));
00282     }
00283     public void caseLeExpr(LeExpr expr)
00284     {
00285         translateBinaryOp(expr.getOp1(), expr.getOp2(), " <= ");
00286     }
00287     public void caseLengthExpr(LengthExpr expr)
00288     {
00289     TreeNode result = applyTo(expr.getArray());
00290     Vector leaves = result.getLeaves(new Vector());
00291     for (int i = 0; i < leaves.size(); i++) {
00292         ExprNode leaf = (ExprNode) leaves.elementAt(i);
00293         leaf.update(leaf.expr1 + ".length");
00294     }
00295     setResult(result);
00296     }
00297     public void caseLockAction(LockAction lockAction) 
00298     {
00299     CaseNode lockTree = (CaseNode) applyTo(lockAction.getLockExpr());
00300     String opName = "_" +  
00301         LockAction.operationName(lockAction.getOperation());
00302     if (lockAction.isWait())
00303         opName += "_" + lockAction.getThread().getId();
00304     Lock lockType = (Lock) lockAction.getLockExpr().getType();
00305     if (lockType.isReentrant() 
00306         && ! lockAction.isLockAction(NOTIFY|NOTIFYALL))
00307         opName += "_R";
00308     Vector leaves = lockTree.getLeaves(new Vector());
00309     for (int i = 0; i < leaves.size(); i++) {
00310         ExprNode leaf = (ExprNode) leaves.elementAt(i);
00311         leaf.update(opName + "(" + leaf.expr1 + "," +
00312             actionIdWithCommas() + ");");
00313     }
00314     printStatement(lockTree.getCase(normal));
00315     }
00316     public void caseLockTest(LockTest lockTest) {
00317     TreeNode lockTree;
00318     Vector leaves;
00319     switch (lockTest.getOperation()) {
00320     case LOCK_AVAILABLE:
00321         String opName = "_lockAvailable";
00322         if (((Lock)lockTest.getLockExpr().getType()).isReentrant())
00323         opName += "_R";
00324         lockTree = applyTo(lockTest.getLockExpr());
00325         leaves = lockTree.getLeaves(new Vector());
00326         for (int i = 0; i < leaves.size(); i++) {
00327         ExprNode leaf = (ExprNode) leaves.elementAt(i);
00328         leaf.update(opName + "(" + leaf.expr1 + ")");
00329         }
00330         setResult(lockTree);
00331         return;
00332     case HAS_LOCK:
00333         setResult(specialize("true"));
00334         return;
00335     case WAS_NOTIFIED:
00336         lockTree = applyTo(lockTest.getLockExpr());
00337         leaves = lockTree.getLeaves(new Vector());
00338         for (int i = 0; i < leaves.size(); i++) {
00339         ExprNode leaf = (ExprNode) leaves.elementAt(i);
00340         leaf.update("_wasNotified_" + lockTest.getThread().getId() 
00341                 + "(" + leaf.expr1 + ")");
00342         }
00343         setResult(lockTree);
00344         return;     
00345     }   
00346     }
00347     public void caseLtExpr(LtExpr expr)
00348     {
00349         translateBinaryOp(expr.getOp1(), expr.getOp2(), " < ");
00350     }
00351     public void caseMulExpr(MulExpr expr)
00352     {
00353     translateBinaryOp(expr.getOp1(), expr.getOp2(), " * ");
00354     }
00355     public void caseNeExpr(NeExpr expr)
00356     {
00357         translateBinaryOp(expr.getOp1(), expr.getOp2(), " != ");
00358     }
00359     public void caseNewArrayExpr(NewArrayExpr expr)
00360     {
00361     Collection colType =  (Collection)expr.getCollection().getType();
00362     Array arrayType = (Array)colType.getBaseType();
00363     String arrayTypeName = dSpinTypeName(arrayType,null);
00364     Type baseType = arrayType.getBaseType();
00365     String baseTypeName = dSpinTypeName(baseType,null);
00366     if (baseType.isKind(REF)) 
00367         baseTypeName = baseTypeName.substring(0,baseTypeName.length() - 4)
00368         + "_aref";
00369     int refIndex = refIndex(expr.getCollection());
00370     CaseNode setLength = applyTo(expr.getLength());
00371     Vector leafCases = setLength.getLeafCases(new Vector());
00372     for (int i = 0; i < leafCases.size(); i++) {
00373         Case leafCase = (Case) leafCases.elementAt(i);
00374         ExprNode leaf = (ExprNode) leafCase.node;
00375         leaf.update("_temp_ = " + leaf.expr1 + ";");
00376     }
00377     printStatement(setLength.getCase(normal));
00378     resetTemp = true;
00379     println("_new_ = new " + arrayTypeName + ";");
00380     println("_new_.refIndex = " + refIndex + ";");
00381     println("_new_.length = _temp_;");
00382     println("_new_.elements = new " + baseTypeName + "[_temp_];");
00383     println("printf(\"BIR? " + actionNum + " %d\\n\",_temp_); ");
00384     resetNew = true;
00385     setResult(specialize("_new_"));
00386     }
00387     public void caseNewExpr(NewExpr expr)
00388     {
00389     Type type = ((Collection)expr.getCollection().getType()).getBaseType();
00390     String typeName = dSpinTypeName(type,null);
00391     println("_new_ = new " + typeName + ";");
00392     println("_new_.refIndex = " + refIndex(expr.getCollection()) + ";");
00393     resetNew = true;
00394     setResult(specialize("_new_"));
00395     }
00396     public void caseNotExpr(NotExpr expr)
00397     {
00398     translateUnaryOp(expr.getOp(),"! ");
00399     }
00400     public void caseNullExpr(NullExpr expr)
00401     {
00402         setResult(specialize("null"));
00403     }
00404     public void caseOrExpr(OrExpr expr)
00405     {
00406     translateBinaryOp(expr.getOp1(), expr.getOp2(), " || ");
00407     }
00408     public void casePrintAction(PrintAction printAction) {
00409     // Perhaps remove this---get output from BIR trace instead
00410     if (printAction.getPrintItems().size() > 0) {
00411         String format = "BIR|";
00412         String params = "";
00413         Vector printItems = printAction.getPrintItems();
00414         for (int i = 0; i < printItems.size(); i++) {
00415         Object item = printItems.elementAt(i);
00416         if (item instanceof String)
00417             format += item;
00418         else {
00419             format += "%d";
00420             CaseNode varTree = (CaseNode) applyTo((Expr)item);
00421             params += "," + ((ExprNode)varTree.getCase(normal)).expr1;
00422         }
00423         }
00424         println("printf(\"" + format + "\\n\"" + params + "); ");
00425     }
00426     }
00427     public void caseRecordExpr(RecordExpr expr)
00428     {
00429     TreeNode result = applyTo(expr.getRecord());
00430     String field = expr.getField().getName();
00431     Vector leaves = result.getLeaves(new Vector());
00432     for (int i = 0; i < leaves.size(); i++) {
00433         ExprNode leaf = (ExprNode) leaves.elementAt(i);
00434         leaf.update(leaf.expr1 + "." + field);
00435     }
00436     setResult(result);
00437     }
00438     public void caseRefExpr(RefExpr expr)
00439     {
00440     setResult(specialize("& " + expr.getTarget().getName()));
00441     }
00442     public void caseRemExpr(RemExpr expr)
00443     {   
00444     TreeNode e1Tree = applyTo(expr.getOp1());
00445     TreeNode e2Tree = applyTo(expr.getOp2());
00446     TreeNode result = e1Tree.compose(e2Tree,null);
00447     Vector leafCases = result.getLeafCases(new Vector());
00448     for (int i = 0; i < leafCases.size(); i++) {
00449         Case leafCase = (Case) leafCases.elementAt(i);
00450         ExprNode leaf = (ExprNode) leafCase.node;
00451         leafCase.insertTrap(leaf.expr2 + " == 0",
00452                 "ArithmeticException",true);
00453         leaf.update("(" + leaf.expr1 + " % " + leaf.expr2 + ")");
00454     }
00455     setResult(result);
00456     }
00457     public void caseStateVar(StateVar expr)
00458     {
00459     setResult(specialize(expr.getName()));
00460     }
00461     public void caseSubExpr(SubExpr expr)
00462     {
00463     translateBinaryOp(expr.getOp1(), expr.getOp2(), " - ");
00464     }
00465     public void caseThreadAction(ThreadAction threadAction) 
00466     {
00467     String opName = 
00468         ThreadAction.operationName(threadAction.getOperation());
00469     int threadId = threadAction.getThreadArg().getId();
00470     println("_" + opName + "Thread_" + threadId + ";");
00471     }
00472     public void caseThreadLocTest(ThreadLocTest threadLocTest) {
00473     String threadName = threadLocTest.getThread().getName();
00474     int threadId = 1 + threadLocTest.getThread().getId();
00475     String locLabel = locLabel(threadLocTest.getLocation());
00476     String test = threadName + "[" + threadId + "]@" + locLabel;
00477     setResult(specialize(test));
00478     }
00479     public void caseThreadTest(ThreadTest threadTest) {
00480     switch (threadTest.getOperation()) {
00481     case THREAD_TERMINATED:
00482         String opName = 
00483         ThreadTest.operationName(threadTest.getOperation());
00484         int threadId = threadTest.getThreadArg().getId();
00485         String test = "_" + opName + "_" + threadId;
00486         setResult(specialize(test));
00487         return;
00488     }   
00489     }
00490     public String check() { return runSpin(); }
00491     static String currentDir() { return System.getProperty("user.dir"); }
00492     public void defaultCase(Object obj)
00493     {
00494     throw new RuntimeException("Trans type not handled: " + obj);
00495     }
00496     void definitions() {
00497     Vector definitions = system.getDefinitions();
00498     for (int i = 0; i < definitions.size(); i++) {
00499         Definition def = (Definition) definitions.elementAt(i);
00500         if (def instanceof Constant) 
00501         println("#define " + def.getName() + " " + def.getDef());
00502     }
00503     Vector types = system.getTypes();
00504     for (int i = 0; i < types.size(); i++) {
00505         Type type = (Type) types.elementAt(i);
00506         if (type.isKind(BOOL|RANGE|LOCK|ENUMERATED|REF)) {
00507         println("/* " + type.typeName() + " = " + type + " */");
00508         print("#define " + type.typeName() + " ");
00509         println(dSpinTypeName(type,this));
00510         if (type.isKind(ENUMERATED)) {
00511             Enumerated enum = (Enumerated) type;
00512             for (int j = 0; j < enum.getEnumeratedSize(); j++) {
00513             String name = enum.getNameOf(enum.getFirstElement()+j);
00514             if (name != null)
00515                 println("#define " + name + " " + 
00516                     (enum.getFirstElement()+j));
00517             }
00518         }
00519         println();
00520         }
00521         if (type.isKind(RECORD|ARRAY)) {
00522         println("typedef " + type.typeName() + ";");
00523         println();
00524         }
00525     }
00526     for (int i = 0; i < types.size(); i++) {
00527         Type type = (Type) types.elementAt(i);
00528         if (type.isKind(REF)) {
00529         String refRoot = 
00530             type.typeName().substring(0,type.typeName().length() - 4);
00531         println("typedef " + refRoot + "_aref { " +
00532             type.typeName() + " ref; }");
00533         println();
00534         }
00535     }
00536     for (int i = 0; i < types.size(); i++) {
00537         Type type = (Type) types.elementAt(i);
00538         if (! type.isKind(BOOL|RANGE|LOCK|ENUMERATED|REF|COLLECTION)) {
00539         println("/* " + type.typeName() + " = " + type + " */");
00540         print("typedef " + type.typeName() + " ");
00541         println(dSpinTypeName(type,this));
00542         println();
00543         }
00544     }
00545     println();
00546     }
00547     String dSpinTypeName(Type type, Object o) {
00548     type.apply(namer,o);
00549     return (String) namer.getResult();
00550     }
00551     String execAndWait(String command, boolean verbose) {
00552     try {
00553         if (verbose)
00554         System.out.println(command);
00555         Process p = runtime.exec(command);
00556         InputStream commandErr = p.getErrorStream();
00557         InputStream commandOut = p.getInputStream();
00558         int count = 0;       // total chars read
00559         int charsRead = 0;   // chars read on read
00560         int charsAvail = 0;  // chars available
00561         while ((count < BUFSIZE) && (charsRead >= 0)) {
00562         charsAvail = commandErr.available();
00563         if (charsAvail > 0) 
00564             count += commandErr.read(buffer,count,charsAvail);
00565         charsRead = commandOut.read(buffer,count,BUFSIZE - count);
00566         if (charsRead > 0)
00567             count += charsRead;
00568         }
00569         p.waitFor();
00570         String output = new String(buffer,0,count);
00571         if (verbose && count > 0)
00572         System.out.println(output);
00573         return output;
00574     }
00575     catch (Exception e) {
00576         throw new RuntimeException("exec of command '" + command
00577                        + "' was aborted: \n" + e);
00578     }
00579     }
00580 /**
00581  * getCounterExample method comment.
00582  */
00583 public List getCounterExample() {
00584     return null;
00585 }
00586     public DSpinOptions getDSpinOptions() { return options; }
00587     String getSimpleResult() {
00588     TreeNode result = ((CaseNode)getResult()).getCase(normal);
00589     if (result instanceof ExprNode) 
00590         return ((ExprNode)result).expr1;
00591     else
00592         throw new RuntimeException("Result not simple: " + result);
00593     }
00594     boolean guardPresent(Transformation trans) {
00595     Expr guard = trans.getGuard();
00596     if (guard == null)
00597         return false;
00598     if (guard instanceof BoolLit)
00599         return ! ((BoolLit)guard).getValue();
00600     if ((guard instanceof LockTest) 
00601         && ((LockTest)guard).getOperation() == HAS_LOCK)
00602         return false;
00603     return true;
00604     }
00605     void header() {
00606     ThreadVector threadVector = system.getThreads();
00607 
00608     println("/*  (dSPIN) Promela for transition system: " 
00609             + system.getName() + " */");
00610     println();
00611 
00612     // Lock types (R = reentrant, W = waiting)
00613     println("/* Lock operations */");
00614     println("typedef lock_ {\n  byte owner;\n};");
00615     println("typedef lock_W {\n  byte owner;\n  int waiting;\n};");
00616     println("typedef lock_R {\n  byte count;\n  byte owner;\n};");
00617     println("typedef lock_RW {\n  byte count;\n  byte owner;\n  int waiting;\n};");
00618 
00619         // Monitor operations - most have separate reentrant version (_R)
00620     println("#define _lock(sync,locNum,transNum,actionNum) \\");
00621     println("  sync.owner = _pid ");
00622     println("#define _lock_R(sync,locNum,transNum,actionNum) \\");
00623     println("  if \\");
00624         println("  :: sync.owner == _pid -> sync.count++; \\");
00625     println("  :: else -> sync.owner = _pid; \\");
00626     println("  fi ");
00627 
00628     println("#define _unlock(sync,locNum,transNum,actionNum) \\");
00629     println("  sync.owner = 0 ");
00630     println("#define _unlock_R(sync,locNum,transNum,actionNum) \\");
00631     println("  if \\");
00632         println("  :: sync.count > 0 -> sync.count--; \\");
00633     println("  :: else -> sync.owner = 0; \\");
00634     println("  fi ");
00635 
00636     println("#define _lockAvailable(sync) \\");
00637     println("  (sync.owner == 0)");
00638     println("#define _lockAvailable_R(sync) \\");
00639     println("  (sync.owner == 0 || sync.owner == _pid) ");
00640 
00641     println("#define _unwait(sync,locNum,transNum,actionNum) \\");
00642     println("  sync.owner = _pid ");
00643     println("#define _unwait_R(sync,locNum,transNum,actionNum) \\");
00644     println("  sync.owner = _pid; sync.count = _temp_; _temp_ = 0 ");
00645 
00646     println("#define _notifyAll(sync,locNum,transNum,actionNum) \\");
00647     println("  if \\");
00648         println("  :: sync.owner == _pid -> sync.waiting = 0; \\");
00649     println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\"); assert(0); \\");
00650     println("  fi ");
00651 
00652     println("#define _notify(sync,locNum,transNum,actionNum) \\");
00653     println("  if \\");
00654     for (int i = 0; i < threadVector.size(); i++) {
00655         int thread = (1 << i);
00656         println("  :: (sync.owner == _pid) && (sync.waiting & " + thread + ") -> sync.waiting = sync.waiting & " + ~ thread + " ; printf(\"BIR? %d " + i + "\",actionNum); \\");
00657     }
00658     println("  :: (sync.owner == _pid) && (sync.waiting == 0) -> printf(\"BIR? %d " + threadVector.size() + "\\n\",actionNum); \\");
00659     println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\"); assert(0); \\");
00660     println("  fi  ");
00661 
00662     for (int i = 0; i < threadVector.size(); i++) {
00663         int thread = (1 << i);
00664 
00665         println("#define _wait_" + i + "(sync,locNum,transNum,actionNum) \\");
00666         println("  if \\");
00667         println("  :: sync.owner == _pid -> sync.waiting = sync.waiting | " + thread + ";  \\");
00668         println("       sync.owner = 0; \\");
00669         println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\"); assert(0); \\");
00670         println("  fi ");
00671         println("#define _wait_" + i + "_R(sync,locNum,transNum,actionNum) \\");
00672         println("  if \\");
00673         println("  :: sync.owner == _pid -> sync.waiting = sync.waiting | " + thread + ";  \\");
00674         println("       _temp_ = sync.count; sync.count = 0; sync.owner = 0; \\");
00675         println("  :: else -> printf(\"BIR: locNum transNum actionNum IllegalMonitorStateException\"); assert(0); \\");
00676         println("  fi ");
00677 
00678         println("#define _wasNotified_" + i + "(sync) \\");
00679         println("  !(sync.waiting & " + thread + ") ");
00680         
00681         if (! threadVector.elementAt(i).isMain()) {
00682         println("#define _startThread_" + i + " \\");
00683         println("  _threadActive_" + i + " = 1; _threadStart_" + 
00684                 i + "!ready");
00685         println("#define _beginThread_" + i + " \\");
00686         println("  _threadStart_" + i + "?ready");
00687         println("#define _joinThread_" + i + " \\");
00688         println("  skip");
00689         println("#define _exitThread_" + i + " \\");
00690         println("  _threadActive_" + i + " = 0; goto endtop_"  + i);
00691         println("#define _threadTerminated_" + i + " \\");
00692         println("  (_threadActive_" + i + " == 0)");
00693         }
00694     }
00695     
00696     println("typedef object {\n  byte refIndex;\n  byte length; object& elements\n};");
00697     println("#define TRAP 1");
00698     println("mtype { ready };");
00699     println();
00700     }
00701     void initBlock() {
00702     ThreadVector threadVector = system.getThreads();
00703     println("init {");
00704     indentLevel = 2;
00705     println("atomic {");
00706     indentLevel++;
00707     StateVarVector stateVarVector = system.getStateVars();
00708     DSpinTypeInit initializer = new DSpinTypeInit(this,out);
00709     for (int i = 0; i < stateVarVector.size(); i++) {
00710         StateVar var = stateVarVector.elementAt(i);
00711         var.getType().apply(initializer,var);
00712     }
00713     for (int i = 0; i < threadVector.size(); i++) {
00714         BirThread thread = threadVector.elementAt(i);
00715         println("assert(run " + thread.getName() + "() == " +
00716             (1 + thread.getId()) + ");");
00717     }
00718     indentLevel--;
00719     println("}");
00720     println("assert(! limit_exception);");
00721     indentLevel = 0;
00722     println("}");
00723     }
00724     boolean isIfBranch(TransVector outTrans) {
00725     if (outTrans.size() != 2) 
00726         return false;
00727     Expr guard1 = outTrans.elementAt(0).getGuard();
00728     Expr guard2 = outTrans.elementAt(1).getGuard();
00729     if (guard1 == null || guard2 == null) 
00730         return false;
00731     if ((guard1 instanceof NotExpr) 
00732         && ((NotExpr)guard1).getOp().equals(guard2))
00733         return true;
00734     if ((guard2 instanceof NotExpr) 
00735         && ((NotExpr)guard2).getOp().equals(guard1))
00736         return true;
00737     return false;
00738     }
00739     static String locLabel(Location loc) {
00740     if (loc.getOutTrans().size() == 0)
00741         return "endloc_" + loc.getId();
00742     else
00743         return "loc_" + loc.getId();
00744     }
00745     static String locLabel(Location loc1, int branch, Location loc2) {
00746     return "loc_" + loc1.getId() + "_" + branch + "_" + loc2.getId();
00747     }
00748     boolean nonNegative(Expr expr) {
00749     if (expr instanceof ConstExpr) 
00750         return ((ConstExpr)expr).getValue() >= 0;
00751     if (expr.getType() instanceof Range) {
00752         Range type = (Range) expr.getType();
00753         return (type.getFromVal().getValue() >= 0);
00754     }
00755     return false;
00756     }
00757     static int parseInt(String s) {
00758     try {
00759         int result = Integer.parseInt(s);
00760         return result;
00761     } catch (NumberFormatException e) {
00762         throw new RuntimeException("Integer didn't parse: " + s);
00763     }
00764     }
00765     void parseLine(String line, BirTrace trace) {
00766     int pos = line.indexOf("BIR:");
00767     if (pos >= 0) {
00768         StringTokenizer st = 
00769         new StringTokenizer(line.substring(pos + 4));
00770         int locId = parseInt(st.nextToken());
00771         int transNum = parseInt(st.nextToken());
00772         int actionNum = parseInt(st.nextToken());
00773         String status = st.nextToken();
00774         Location loc = system.getLocation(locId);
00775         Transformation trans = 
00776         loc.getOutTrans().elementAt(transNum);
00777         if (status.equals("OK")) {
00778         if (actionNum == 1)
00779             trace.addTrans(trans);
00780         }
00781         else
00782         trace.setTrap(status,trans,actionNum);
00783         return;
00784     }
00785     pos = line.indexOf("BIR?");
00786     if (pos >= 0) {
00787         StringTokenizer st = 
00788         new StringTokenizer(line.substring(pos + 4));
00789         int actionNum = parseInt(st.nextToken());
00790         int choiceNum = parseInt(st.nextToken());
00791         trace.setChoice(actionNum,choiceNum);
00792     }
00793     }
00794     /**
00795      * Parse the output of 'pan' and interpret it as either a violation 
00796      * (sequence of transformations) or as a error-free analysis.
00797      * <p>
00798      * @return a vector of transformations (if there was an error found), or null (otherwise)
00799      */
00800 
00801     public BirTrace parseOutput() {
00802     if (! ranVerifier) 
00803         throw new RuntimeException("Did not run verifier on input");
00804     try {
00805             File sourceFile = new File(currentDir(), 
00806                        system.getName() + ".dprom");
00807             File trailFile = new File(currentDir(), 
00808                       system.getName() + ".dprom.trail");
00809         BirTrace trace = new BirTrace(system);
00810         // We use the presence of the trail file to detect success/failure
00811         if (! trailFile.exists()) {
00812         trace.setVerified(true);   // property verified
00813         return trace;
00814         }
00815         String output = 
00816         execAndWait("dspin -t " + sourceFile.getAbsolutePath(), true);
00817         BufferedReader reader = 
00818         new BufferedReader(new StringReader(output));
00819         String line = reader.readLine();
00820         while (line != null) {
00821         parseLine(line,trace);
00822         line = reader.readLine();
00823         }
00824         trace.done();
00825         trace.setVerified(false);
00826         return trace;
00827         } catch(IOException e) {
00828             throw new RuntimeException("Error parsing dSPIN output: \n" + e);
00829         }   
00830     }
00831     void predicates() {
00832     println("/* Predicates */");
00833     Vector preds = system.getPredicates();
00834     for (int i = 0; i < preds.size(); i++) {
00835         Expr pred = (Expr) preds.elementAt(i);
00836         String name = system.predicateName(pred);
00837         inDefine = true;
00838         println("#define " + name + " ");
00839         indentLevel = 1;
00840         printGuard(applyTo(pred).getCase(normal));
00841         inDefine = false;
00842         println("");
00843         indentLevel = 0;
00844     }
00845     println("");
00846     }
00847     void print(String s) {
00848     if (newLine) {
00849         for (int i = 0; i < indentLevel; i++)
00850         out.print("   ");
00851         newLine = false;
00852     }
00853     out.print(s);
00854     }
00855     void printGuard(TreeNode tree) {
00856     if (tree instanceof ExprNode) {
00857         ExprNode node = (ExprNode) tree;
00858         print(node.expr1);
00859     }
00860     else if (tree instanceof TrapNode) {
00861         TrapNode node = (TrapNode) tree;
00862         print("TRAP");
00863     }
00864     else {
00865         CaseNode node = (CaseNode) tree;
00866         print("(  ");
00867         for (int i = 0; i < node.size(); i++) {
00868         Case c = node.elementAt(i);
00869         indentLevel++;
00870         println("(  " + c.cond);
00871         print("&& ");
00872         indentLevel++;
00873         printGuard(c.node);
00874         indentLevel--;
00875         print(" )");
00876         indentLevel--;
00877         if (i < node.size() - 1) {
00878             println();
00879             print("|| ");
00880         }
00881         }
00882         println(" )");
00883     }
00884     }
00885     void println() {
00886     if (inDefine)
00887         out.print("\\");
00888     out.println();
00889     newLine = true;
00890     }
00891     void println(String s) {
00892     print(s);
00893     println();
00894     }
00895     void printStatement(TreeNode tree) {
00896     if (tree instanceof ExprNode) {
00897         ExprNode node = (ExprNode) tree;
00898         println(node.expr1);
00899     }
00900     else if (tree instanceof TrapNode) {
00901         TrapNode node = (TrapNode) tree;
00902         print("   printf(\"BIR: " + actionId() 
00903           + " " + node.desc + "\\n\"); ");
00904         if (node.fatal)
00905         println("assert(0);");
00906         else
00907         println("limit_exception = 1; goto endtrap;");
00908     }
00909     else {
00910         CaseNode node = (CaseNode) tree;
00911         println("if ");
00912         for (int i = 0; i < node.size(); i++) {
00913         Case c = node.elementAt(i);
00914         String cond = (i < node.size() - 1) ? c.cond : "else";
00915         println(":: " + cond + " -> ");
00916         indentLevel++;
00917         printStatement(c.node);
00918         indentLevel--;
00919         }
00920         println("fi; ");
00921     }   
00922     }
00923     void property() {
00924     if (options.ApplyNeverClaim)
00925         println("#include \"" + system.getName() + ".never\"");
00926     }
00927     int refIndex(StateVar target) {
00928     return 1 + system.refAnyType().getTargets().indexOf(target);
00929     }
00930     void resetDeadVariables(Location fromLoc, Location toLoc) {
00931     StateVarVector liveBefore = fromLoc.getLiveVars();
00932     StateVarVector liveAfter = toLoc.getLiveVars();
00933     if (liveBefore != null && liveAfter!= null) 
00934         for (int i = 0; i < liveBefore.size(); i++) 
00935         if (liveAfter.indexOf(liveBefore.elementAt(i)) == -1) {
00936             // var was live, now is not---reset it
00937             StateVar var = liveBefore.elementAt(i);
00938             var.apply(this);
00939             print(getSimpleResult() + " = ");
00940             var.getInitVal().apply(this);
00941             println(getSimpleResult() + ";");
00942         }
00943     }
00944     DSpinTrans run() {
00945     header();
00946     definitions();
00947     stateVariables();
00948     transitions();
00949     predicates();
00950     property();
00951     return this;
00952     }
00953     /**
00954      * Run SPIN to generate an analyzer (pan), and then run the analyzer.
00955      * <p>
00956      * The translator must have been executed for the transition system
00957      * (the file NAME.dprom must exist and contain the translated PROMELA).
00958      * @return the output of 'pan' (as a String)
00959      */
00960 
00961     public String runSpin() {
00962     try {
00963         if (options.ApplyNeverClaim) {
00964         File ltlFile = new File(currentDir(), 
00965                        system.getName() + ".spin.ltl");
00966         if (! ltlFile.exists())
00967             throw new RuntimeException("Cannot find LTL file: " +
00968                            ltlFile.getAbsolutePath());
00969         String neverClaim = 
00970             execAndWait("spin -F " + ltlFile.getAbsolutePath(), true);
00971         File neverFile = new File(currentDir(), 
00972                       system.getName() + ".never");
00973         FileOutputStream streamOut = new FileOutputStream(neverFile);
00974         PrintWriter writerOut = new PrintWriter(streamOut);
00975         writerOut.println(neverClaim);
00976         writerOut.close();
00977         }
00978             File sourceFile = new File(currentDir(), 
00979                        system.getName() + ".dprom");
00980         if (! sourceFile.exists())
00981         throw new RuntimeException("Cannot find dSPIN source file: " +
00982                        sourceFile.getAbsolutePath());
00983             File trailFile = new File(currentDir(), 
00984                       system.getName() + ".dprom.trail");
00985         if (trailFile.exists())
00986         trailFile.delete();
00987         File panFile = new File(currentDir(), 
00988                     "pan.exe");
00989         execAndWait("dspin -a " + sourceFile.getAbsolutePath(), true);
00990         execAndWait(ccName + " " + options.compileOptions() +
00991             " -o pan.exe -I " + includeDir + " pan.c", true);
00992         ranVerifier = true;
00993         return execAndWait(panFile.getCanonicalPath() + " " +
00994                    options.panOptions(), true);
00995         
00996         } catch(Exception e)
00997         {
00998             throw new RuntimeException("Could not produce SPIN file (" + e + ")");
00999         }   
01000     }
01001     TreeNode specialize(String expr) {
01002     return new CaseNode(new Case(normal, new ExprNode(expr)));
01003     }
01004     void stateVariables() {
01005     println("bool limit_exception = 0;");
01006     println("byte _i_ = 0;");
01007     println("object& _new_;");
01008     ThreadVector threads = system.getThreads();
01009     for (int i = 0; i < threads.size(); i++) {
01010         if (! threads.elementAt(i).isMain()) {
01011         println("chan _threadStart_" + i + " = [1] of { bit };");
01012         println("bit _threadActive_" + i + ";");
01013         }
01014     }
01015     println();
01016     StateVarVector stateVarVector = system.getStateVars();
01017     for (int i = 0; i < stateVarVector.size(); i++) {
01018         StateVar var = stateVarVector.elementAt(i);
01019         String refIndex = "   ";
01020         if (var.getType().isKind(COLLECTION)) 
01021         println("/* Collection: " + var.getName() + ", ref index = "
01022             + refIndex(var) + " */");
01023         else {
01024         if (var.getType().isKind(RECORD|ARRAY))
01025             refIndex += "/*  ref index = " + refIndex(var) + " */";
01026         println(dSpinTypeName(var.getType(),null) + " " 
01027             + var.getName() + ";" + refIndex);
01028         }
01029     }
01030     println();
01031     }
01032     void transitions() {
01033     ThreadVector threadVector = system.getThreads();
01034     for (int i = 0; i < threadVector.size(); i++) {
01035         BirThread thread = threadVector.elementAt(i);
01036         println("proctype " + thread.getName() + "() { ");
01037         println("  int _temp_;");
01038         if (! thread.isMain()) 
01039         println("endtop_" + i + ":\n   _beginThread_" + i + ";");
01040         LocVector threadLocVector = thread.getLocations();
01041         for (int j = 0; j < threadLocVector.size(); j++) 
01042         translateLocation(threadLocVector.elementAt(j));
01043         println("endtrap:");
01044         println("  0;");
01045         println("}");
01046         println();
01047     }
01048     initBlock();
01049     }
01050     /**
01051      * Generate PROMELA source representing a transition system.
01052      * <p>
01053      * As above, but with default options.
01054      * @param system the transition system
01055      * @return the DSpinTrans control object
01056      */
01057 
01058     public static DSpinTrans translate(TransSystem system) {
01059     return translate(system,null);
01060     }
01061     /**
01062      * Generate PROMELA source representing a transition system.
01063      * <p>
01064      * The PROMELA is written to a file NAME.dprom where NAME
01065      * is the name of the transition system.  A set of
01066      * options can be provided in a DSpinOptions object.
01067      * @param system the transition system
01068      * @param options the SPIN verifier options
01069      * @return the SpinTrans control object
01070      */
01071 
01072     public static DSpinTrans translate(TransSystem system, 
01073                        DSpinOptions options) {
01074     try {
01075             File sourceFile = new File(currentDir(), 
01076                        system.getName() + ".dprom");
01077 
01078             FileOutputStream streamOut = new FileOutputStream(sourceFile);
01079             PrintWriter writerOut = new PrintWriter(streamOut);
01080         DSpinTrans result = translate(system, options, writerOut);
01081             writerOut.close();
01082         return result;
01083         } catch(IOException e)
01084         {
01085             throw new RuntimeException("Could not produce dSPIN file: " + e);
01086         }
01087     }
01088     /**
01089      * Generate PROMELA source representing a transition system.
01090      * <p>
01091      * As above, but the PROMELA is written to the PrintWriter provided.
01092      * @param system the transition system
01093      * @param out the PrintWriter to write the PROMELA to
01094      * @return the DSpinTrans control object
01095      */
01096 
01097     public static DSpinTrans translate(TransSystem system, 
01098                        DSpinOptions options,
01099                        PrintWriter out) {
01100     return (new DSpinTrans(system,options,out)).run();
01101     }
01102     void translateBinaryOp(Expr e1, Expr e2, String op) {
01103     TreeNode e1Tree = applyTo(e1);
01104     TreeNode e2Tree = applyTo(e2);
01105     TreeNode result = e1Tree.compose(e2Tree,null);
01106     Vector leaves = result.getLeaves(new Vector());
01107     for (int i = 0; i < leaves.size(); i++) {
01108         ExprNode leaf = (ExprNode) leaves.elementAt(i);
01109         leaf.update("(" + leaf.expr1 + op + leaf.expr2 + ")");
01110     }
01111     setResult(result);
01112     }
01113     public void translateLocation(Location loc)
01114     {
01115     if (! loc.isVisible())
01116         return;
01117     println(locLabel(loc) + ":");
01118     indentLevel++;
01119     TransVector outTrans = loc.getOutTrans();
01120     if (outTrans.size() == 1) 
01121         translateSequence(outTrans.elementAt(0),0);
01122     else if (outTrans.size() == 0)  
01123         println("0;");
01124     else {
01125         println("if");
01126         for (int i = 0;  i < outTrans.size(); i++) {
01127         print(":: ");
01128         indentLevel++;
01129         translateSequence(outTrans.elementAt(i),i);
01130         indentLevel--;
01131         }
01132         println("fi;");
01133     }
01134     indentLevel--;
01135     }
01136     void translateSeq(LocVector locSet, Transformation trans, 
01137               int branch, boolean supressGuard) {
01138     translateTrans(trans, supressGuard);
01139     if (trans.getToLoc().isVisible()) {
01140         resetDeadVariables(locSet.firstElement(), trans.getToLoc());
01141         println("goto " + locLabel(trans.getToLoc()) + ";");
01142     }
01143     else if (locSet.contains(trans.getToLoc()))
01144         println("goto " + 
01145             locLabel(locSet.firstElement(),branch,trans.getToLoc()) 
01146             + ";");
01147     else {
01148         locSet.addElement(trans.getToLoc());
01149         if (trans.getToLoc().getInTrans().size() > 1)
01150         println(locLabel(locSet.firstElement(),branch,trans.getToLoc())
01151             + ":");
01152         TransVector successors = trans.getToLoc().getOutTrans();
01153         if (successors.size() == 1) 
01154         translateSeq(locSet, successors.elementAt(0), branch,false);
01155         else if (isIfBranch(successors)) {
01156         println("if");
01157         print(":: ");
01158         indentLevel++;
01159         translateSeq(locSet, successors.elementAt(0), branch, false);
01160         indentLevel--;
01161         print(":: else -> ");
01162         indentLevel++;
01163         translateSeq(locSet, successors.elementAt(1), branch, true);
01164         indentLevel--;
01165         println("fi;");
01166         }
01167         else {
01168         println("if");
01169         for (int i = 0; i < successors.size(); i++) {
01170             print(":: ");
01171             indentLevel++;
01172             translateSeq(locSet, successors.elementAt(i),branch,false);
01173             indentLevel--;
01174         }
01175         println("fi;");
01176         }       
01177     }
01178     }
01179     void translateSequence(Transformation trans, int branch) {
01180     Location startLoc = trans.getFromLoc();
01181         println("atomic { ");
01182     indentLevel++;
01183     translateSeq(new LocVector(startLoc), trans, branch, false);
01184     indentLevel--;
01185     println("}");
01186     }
01187     void translateTrans(Transformation trans, boolean supressGuard)
01188     {
01189     currentTrans = trans;
01190     actionNum = 0;
01191     if (! supressGuard && guardPresent(trans)) {
01192         printGuard(applyTo(trans.getGuard()).getCase(normal));
01193         println("-> ");
01194     }
01195     ActionVector actions = trans.getActions();
01196     for (int i = 0; i < actions.size(); i++) {
01197         actionNum = i + 1;
01198         println("printf(\"BIR: " + actionId() + " OK\\n\"); ");
01199         actions.elementAt(i).apply(this);
01200     }
01201     if (resetTemp) {
01202         println("_temp_ = 0;");
01203         resetTemp = false;
01204     }
01205     if (resetNew) {
01206         println("_new_ = null;");
01207         resetNew = false;
01208     }
01209     }
01210     void translateUnaryOp(Expr e, String op) {
01211     TreeNode result = applyTo(e);
01212     Vector leaves = result.getLeaves(new Vector());
01213     for (int i = 0; i < leaves.size(); i++) {
01214         ExprNode leaf = (ExprNode) leaves.elementAt(i);
01215         leaf.update("(" + op + leaf.expr1 + ")");
01216     }
01217     setResult(result);
01218     }
01219 }