Main Page   Packages   Class Hierarchy   Alphabetical List   Compound List   File List   Compound Members  

SpinTrans Class Reference

Inheritance diagram for SpinTrans:
[legend]
Collaboration diagram for SpinTrans:
[legend]
List of all members.

Public Methods

void caseAddExpr (AddExpr expr)
void caseAndExpr (AndExpr expr)
void caseArrayExpr (ArrayExpr expr)
void caseAssertAction (AssertAction assertAction)
void caseAssignAction (AssignAction assign)
void caseBoolLit (BoolLit expr)
void caseChooseExpr (ChooseExpr expr)
void caseConstant (Constant expr)
void caseDerefExpr (DerefExpr expr)
void caseDivExpr (DivExpr expr)
void caseEqExpr (EqExpr expr)
void caseInstanceOfExpr (InstanceOfExpr expr)
void caseIntLit (IntLit expr)
void caseLeExpr (LeExpr expr)
void caseLengthExpr (LengthExpr expr)
void caseLockAction (LockAction lockAction)
void caseLockTest (LockTest lockTest)
void caseLtExpr (LtExpr expr)
void caseMulExpr (MulExpr expr)
void caseNeExpr (NeExpr expr)
void caseNewArrayExpr (NewArrayExpr expr)
void caseNewExpr (NewExpr expr)
void caseNotExpr (NotExpr expr)
void caseNullExpr (NullExpr expr)
void caseOrExpr (OrExpr expr)
void casePrintAction (PrintAction printAction)
void caseRecordExpr (RecordExpr expr)
void caseRefExpr (RefExpr expr)
void caseRemExpr (RemExpr expr)
void caseStateVar (StateVar expr)
void caseSubExpr (SubExpr expr)
void caseThreadAction (ThreadAction threadAction)
void caseThreadLocTest (ThreadLocTest threadLocTest)
void caseThreadTest (ThreadTest threadTest)
String check ()
void defaultCase (Object obj)
List getCounterExample ()
SpinOptions getSpinOptions ()
boolean isVerbose ()
BirTrace parseOutput ()
String runSpin ()
void setVerbose (boolean v)
void translateLocation (Location loc)

Static Public Methods

SpinTrans translate (TransSystem system)
SpinTrans translate (TransSystem system, SpinOptions options)
SpinTrans translate (TransSystem system, SpinOptions options, PrintWriter out)
SpinTrans translate (TransSystem system, SpinOptions options, String outputDir)

Static Public Attributes

final String normal = "NORMAL_CASE"

Private Methods

 SpinTrans (TransSystem system, SpinOptions options, PrintWriter out)
String actionId ()
String actionIdWithCommas ()
CaseNode applyTo (Expr expr)
void cleanMess ()
void definitions ()
String getSimpleResult ()
boolean guardPresent (Transformation trans)
void header ()
void initBlock ()
boolean isIfBranch (TransVector outTrans)
boolean nonNegative (Expr expr)
void predicates ()
void print (String s)
void printGuard (TreeNode tree)
void println ()
void println (String s)
void printStatement (TreeNode tree)
void property ()
int refIndex (StateVar target)
void resetDeadVariables (Location fromLoc, Location toLoc)
SpinTrans run ()
TreeNode specialize (String expr)
void stateVariables ()
void transitions ()
void translateBinaryOp (Expr e1, Expr e2, String op)
void translateSeq (LocVector locSet, Transformation trans, int branch, boolean supressGuard)
void translateSequence (Transformation trans, int branch)
void translateTrans (Transformation trans, boolean supressGuard)
void translateUnaryOp (Expr e, String op)

Static Private Methods

String currentDir ()
String locLabel (Location loc)
String locLabel (Location loc1, int branch, Location loc2)
int parseInt (String s)

Private Attributes

TransSystem system
PrintWriter out
SpinTypeName namer
int indentLevel = 0
boolean inDefine = false
boolean newLine = true
boolean resetTemp = false
Transformation currentTrans
int actionNum
SpinOptions options
boolean ranVerifier = false
String panOutput
boolean isVerbose = true
String outputDir = "."+File.separator

Static Private Attributes

String ccName = "gcc"

Detailed Description

SpinTrans is the main class of the SPIN translator, which generates PROMELA source representing a transition system.

The SPIN translator is invoked on a transition system as follows: 

 // 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

Definition at line 62 of file SpinTrans.java.

Member Function Documentation

String SpinTrans::actionId (    )  [inline, private]
 

Get action ID of current action = loc_num trans_index action_index

Definition at line 100 of file SpinTrans.java.

String SpinTrans::actionIdWithCommas (    )  [inline, private]
 

Get action ID of current action, but comma seperated.

Definition at line 110 of file SpinTrans.java.

CaseNode SpinTrans::applyTo (  Expr   expr )  [inline, private]
 

Apply translator to BIR Expr, return case tree.

Definition at line 120 of file SpinTrans.java.

void SpinTrans::caseArrayExpr (  ArrayExpr   expr )  [inline, virtual]
 

Translate array expression.

Must insert traps for array out of bounds.

Reimplemented from ExprSwitch.

Definition at line 136 of file SpinTrans.java.

void SpinTrans::caseAssertAction (  AssertAction   assertAction )  [inline, virtual]
 

Translate assert action.

Reimplemented from ExprSwitch.

Definition at line 158 of file SpinTrans.java.

void SpinTrans::caseAssignAction (  AssignAction   assign )  [inline, virtual]
 

Translate a BIR assignment action.

Reimplemented from ExprSwitch.

Definition at line 172 of file SpinTrans.java.

void SpinTrans::caseChooseExpr (  ChooseExpr   expr )  [inline, virtual]
 

Translate choose expression.

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.

Reimplemented from ExprSwitch.

Definition at line 232 of file SpinTrans.java.

void SpinTrans::caseDerefExpr (  DerefExpr   expr )  [inline, virtual]
 

Translate dereference.

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.

Reimplemented from ExprSwitch.

Definition at line 256 of file SpinTrans.java.

void SpinTrans::caseDivExpr (  DivExpr   expr )  [inline, virtual]
 

Translate division.

DivExpr and RemExpr require special handling because they can cause a ArithmeticException if the second arg is zero.

Reimplemented from ExprSwitch.

Definition at line 290 of file SpinTrans.java.

void SpinTrans::caseInstanceOfExpr (  InstanceOfExpr   expr )  [inline, virtual]
 

Translate instanceof expression (basically a big disjunction to test the refIndex for all possible targets).

Reimplemented from ExprSwitch.

Definition at line 312 of file SpinTrans.java.

void SpinTrans::caseLengthExpr (  LengthExpr   expr )  [inline, virtual]
 

Translate array length expression.

Reimplemented from ExprSwitch.

Definition at line 346 of file SpinTrans.java.

void SpinTrans::caseLockAction (  LockAction   lockAction )  [inline, virtual]
 

Translate lock action.

Reimplemented from ExprSwitch.

Definition at line 359 of file SpinTrans.java.

void SpinTrans::caseLockTest (  LockTest   lockTest )  [inline, virtual]
 

Translate lock test.

Reimplemented from ExprSwitch.

Definition at line 384 of file SpinTrans.java.

void SpinTrans::caseNewArrayExpr (  NewArrayExpr   expr )  [inline, virtual]
 

Translate array allocator.

Similar to NewExpr (above), except that we need to set (and check) the supplied length.

Reimplemented from ExprSwitch.

Definition at line 434 of file SpinTrans.java.

void SpinTrans::caseNewExpr (  NewExpr   expr )  [inline, virtual]
 

Translate an allocator.

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).

Reimplemented from ExprSwitch.

Definition at line 478 of file SpinTrans.java.

void SpinTrans::casePrintAction (  PrintAction   printAction )  [inline, virtual]
 

Translate BIR Print action.

Perhaps remove this---easier to just get output from BIR trace instead.

Reimplemented from ExprSwitch.

Definition at line 506 of file SpinTrans.java.

void SpinTrans::caseRecordExpr (  RecordExpr   expr )  [inline, virtual]
 

Translate field selector.

Reimplemented from ExprSwitch.

Definition at line 529 of file SpinTrans.java.

void SpinTrans::caseThreadAction (  ThreadAction   threadAction )  [inline, virtual]
 

Translate thread action.

Reimplemented from ExprSwitch.

Definition at line 566 of file SpinTrans.java.

void SpinTrans::caseThreadLocTest (  ThreadLocTest   threadLocTest )  [inline, virtual]
 

Translate thread location test.

Reimplemented from ExprSwitch.

Definition at line 576 of file SpinTrans.java.

void SpinTrans::caseThreadTest (  ThreadTest   threadTest )  [inline, virtual]
 

Translate thread test.

Reimplemented from ExprSwitch.

Definition at line 588 of file SpinTrans.java.

void SpinTrans::definitions (    )  [inline, private]
 

Generate constant and type definitions (using type namer).

Definition at line 734 of file SpinTrans.java.

List SpinTrans::getCounterExample (    )  [inline]
 

getCounterExample method comment.

Definition at line 783 of file SpinTrans.java.

String SpinTrans::getSimpleResult (    )  [inline, private]
 

Retrieve simple result from translator, flag error if not simple.

A simple result is a case tree with only a single expression node under the NORMAL case.

Definition at line 821 of file SpinTrans.java.

boolean SpinTrans::guardPresent (  Transformation   trans )  [inline, private]
 

Test if guard is present.

If the guard is TRUE (BoolLit) or the HAS_LOCK test (which we don't use), claim there is no guard.

Definition at line 838 of file SpinTrans.java.

void SpinTrans::header (    )  [inline, private]
 

Generate the header for all PROMELA files

Definition at line 853 of file SpinTrans.java.

void SpinTrans::initBlock (    )  [inline, private]
 

Generate init {} block to initializae variables and start threads.

Definition at line 985 of file SpinTrans.java.

boolean SpinTrans::isIfBranch (  TransVector   outTrans )  [inline, private]
 

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.

Definition at line 1026 of file SpinTrans.java.

String SpinTrans::locLabel (  Location   loc1,
int   branch,
Location   loc2
)  [inline, static, private]
 

Get PROMELA label of location encountered during coarsening.

Since we may encounter the same location along several collapsed paths, we must have a unique label for each.

Definition at line 1062 of file SpinTrans.java.

String SpinTrans::locLabel (  Location   loc )  [inline, static, private]
 

Get PROMELA label for BIR location.

If location has no out transitions (i.e., is end location of thread), make the label an end-label (does not count for deadlock).

Definition at line 1049 of file SpinTrans.java.

boolean SpinTrans::nonNegative (  Expr   expr )  [inline, private]
 

Test if an expression is statically nonnegative (either a constant or in a range type that is nonnegative).

Definition at line 1070 of file SpinTrans.java.

BirTrace SpinTrans::parseOutput (    )  [inline]
 

Parse the output of 'pan' and interpret it as either a violation (sequence of transformations) or as a error-free analysis.

Returns:
a vector of transformations (if there was an error found), or null (otherwise)

Definition at line 1095 of file SpinTrans.java.

void SpinTrans::predicates (    )  [inline, private]
 

Generate the predicate definitions.

Note that these are at the bottom so they can refer to any variable or code location.

Definition at line 1105 of file SpinTrans.java.

void SpinTrans::print (  String   s )  [inline, private]
 

Support for printing things nicely indented.

Definition at line 1126 of file SpinTrans.java.

void SpinTrans::printGuard (  TreeNode   tree )  [inline, private]
 

Print a case tree as an expression to represent a guard.

We take advantage of the short-curcuit evaluation in PROMELA to express a case tree as one large boolean expression. A case node: 

 (cond1 => expr1, cond2 => expr2, ...)
is translated as 
 ((cond1 && expr1) || (cond2 && expr2) || ... )
We consider traps as always enabled, so they evaluate to the constant TRAP (defined to be 1).

Definition at line 1151 of file SpinTrans.java.

void SpinTrans::printStatement (  TreeNode   tree )  [inline, private]
 

Print a case tree as a statement.

A case node: 

 (cond1 => expr1, cond2 => expr2, ..., condN => exprN)
is translated as 
 if 
 :: cond1 -> expr1 
 :: cond2 -> expr2 
 ... 
 else -> exprN 
 fi

Definition at line 1207 of file SpinTrans.java.

void SpinTrans::property (    )  [inline, private]
 

Generate the include for the never claim

Definition at line 1239 of file SpinTrans.java.

int SpinTrans::refIndex (  StateVar   target )  [inline, private]
 

Return the refIndex of a state variable (it's index in the universal reference type refAny).

Definition at line 1248 of file SpinTrans.java.

void SpinTrans::resetDeadVariables (  Location   fromLoc,
Location   toLoc
)  [inline, private]
 

Reset any variables that have become dead between locations.

In particular, we reset a variable if it was live at fromLoc and is not live at toLoc.

Definition at line 1258 of file SpinTrans.java.

SpinTrans SpinTrans::run (    )  [inline, private]
 

Run translator: generate header, definitions, state variables, transitions (processes), predicates, and the LTL property.

Definition at line 1277 of file SpinTrans.java.

String SpinTrans::runSpin (    )  [inline]
 

Run SPIN to generate an analyzer (pan), and then run the analyzer.

The translator must have been executed for the transition system (the file NAME.prom must exist and contain the translated PROMELA).

Returns:
the output of 'pan' (as a String)

Definition at line 1294 of file SpinTrans.java.

TreeNode SpinTrans::specialize (  String   expr )  [inline, private]
 

Build a trivial case tree with one ExprNode holding the string.

Definition at line 1354 of file SpinTrans.java.

void SpinTrans::stateVariables (    )  [inline, private]
 

Declare the state variables.

Definition at line 1361 of file SpinTrans.java.

void SpinTrans::transitions (    )  [inline, private]
 

Generate the threads.

Each thread is a PROMELA proctype with a label for each (visible) location and an if-case for each transformation out of that location.

Definition at line 1400 of file SpinTrans.java.

SpinTrans SpinTrans::translate (  TransSystem   system,
SpinOptions   options,
PrintWriter   out
)  [inline, static]
 

Generate PROMELA source representing a transition system.

As above, but the PROMELA is written to the PrintWriter provided.

Parameters:
system   the transition system
out   the PrintWriter to write the PROMELA to
Returns:
the SpinTrans control object

Definition at line 1468 of file SpinTrans.java.

SpinTrans SpinTrans::translate (  TransSystem   system,
SpinOptions   options
)  [inline, static]
 

Generate PROMELA source representing a transition system.

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.

Parameters:
system   the transition system
options   the SPIN verifier options
Returns:
the SpinTrans control object

Definition at line 1456 of file SpinTrans.java.

SpinTrans SpinTrans::translate (  TransSystem   system )  [inline, static]
 

Generate PROMELA source representing a transition system.

As above, but with default options.

Parameters:
system   the transition system
Returns:
the SpinTrans control object

Definition at line 1442 of file SpinTrans.java.

void SpinTrans::translateBinaryOp (  Expr   e1,
Expr   e2,
String   op
)  [inline, private]
 

Translate binary op

Definition at line 1492 of file SpinTrans.java.

void SpinTrans::translateLocation (  Location   loc )  [inline]
 

Generate PROMELA for visible BIR location.

Definition at line 1508 of file SpinTrans.java.

void SpinTrans::translateSeq (  LocVector   locSet,
Transformation   trans,
int   branch,
boolean   supressGuard
)  [inline, private]
 

Translate a sequence of transformations starting with the given one, continuing until we hit a visible transformation.

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.

If we transition to a visible location, we always generate a goto to the top-level location label for that location.

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).

Definition at line 1550 of file SpinTrans.java.

void SpinTrans::translateSequence (  Transformation   trans,
int   branch
)  [inline, private]
 

Translate a sequence of transformations, continuing until we hit a visible transformation. Make the sequence atomic.

The 'branch' parameter is used to generate location labels that are local to this atomic block.

Definition at line 1619 of file SpinTrans.java.

void SpinTrans::translateTrans (  Transformation   trans,
boolean   supressGuard
)  [inline, private]
 

Generate code for a single transformation (possibly suppressing the code for the guard expression).

Definition at line 1632 of file SpinTrans.java.

void SpinTrans::translateUnaryOp (  Expr   e,
String   op
)  [inline, private]
 

Translate unary op

Definition at line 1658 of file SpinTrans.java.

The documentation for this class was generated from the following file:
Generated at Thu Feb 7 07:21:56 2002 for Bandera by doxygen1.2.10 written by Dimitri van Heesch, © 1997-2001