---

SmvTrans Class Reference

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

Public Methods
void	caseAddExpr (AddExpr expr)
void	caseAndExpr (AndExpr expr)
void	caseArrayExpr (ArrayExpr expr)
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	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	caseRecordExpr (RecordExpr expr)
void	caseRefExpr (RefExpr expr)
void	caseRemExpr (RemExpr expr)
void	caseStateVar (StateVar expr)
void	caseSubExpr (SubExpr expr)
void	caseThreadLocTest (ThreadLocTest threadLocTest)
void	caseThreadTest (ThreadTest threadTest)
String	check ()
SmvVar	declareVar (String name, String smvType, StateVar source, String initValue, SmvVar aggregate, boolean constrained, SmvVar deadFlag)
void	defaultCase (Object obj)
List	getCounterExample ()
BirTrace	parseOutput ()
String	runSmv ()
Static Public Methods
SmvTrans	translate (TransSystem system, SmvOptions options)
SmvTrans	translate (TransSystem system, SmvOptions options, PrintWriter out)
Private Methods
	SmvTrans (TransSystem system, SmvOptions options, PrintWriter out)
String	activeVar (BirThread thread)
SmvNaryExpr	addConditionalContext (SmvNaryExpr expr, SmvCase context)
SmvExpr	and (SmvExpr expr1, SmvExpr expr2)
String	blockedVar (BirThread thread)
SmvExpr	buildTransExpr (Transformation trans, StateVarVector locals, SmvVar locVar)
void	checkAssign (StateVar lhs, Expr rhs, SmvVar var, SmvExpr value)
String	countVar (String var)
void	declareVariables ()
void	definitions ()
String	elementVar (String var, int i)
SmvExpr	equal (SmvExpr expr1, SmvExpr expr2)
String	execAndWait (String command, boolean verbose)
void	fairness ()
String	fieldVar (String var, Field type)
AssignAction	findLocalAssign (Transformation trans)
TransSystem	getSystem ()
String	getThreadType ()
SmvVar	getVar (String name)
SmvExpr	greaterThan (SmvExpr expr1, SmvExpr expr2)
void	header ()
String	idleVar (BirThread thread)
void	indent (int delta)
void	init ()
void	initAllComponents (SmvVar var, SmvExpr cond)
String	instanceVar (String var, int i)
String	instNumVar (String var)
String	inUseVar (String var, int i)
String	lengthVar (String var)
SmvExpr	lessThan (SmvExpr expr1, SmvExpr expr2)
String	locName (Location loc)
String	locVar (BirThread thread)
SmvExpr	minus1 (SmvExpr expr)
SmvExpr	not (SmvExpr expr)
SmvExpr	or (SmvExpr expr1, SmvExpr expr2)
String	ownerVar (String var)
void	parseLine (String line, BirTrace trace)
void	parseThreadStep (String line, BirTrace trace)
void	parseTrap (String line, BirTrace trace)
SmvExpr	plus1 (SmvExpr expr)
void	prepareParse ()
void	print (String s)
void	println ()
void	println (String s)
void	printVariableDecls ()
void	property ()
void	recordGlobalVarAssignments (SmvExpr lhs, SmvExpr rhs, SmvCase context)
void	recordGlobalVarUpdates ()
void	recordLockStatusUpdates (LockAction action)
void	recordThreadStatusUpdates (ThreadAction action)
int	refIndex (StateVar target)
String	refIndexVar (String var)
SmvLit	refValue (int refIndex, int instNum)
SmvTrans	run ()
void	stateVariables ()
String	tempVar (BirThread thread)
String	terminatedVar (BirThread thread)
SmvExpr	threadBlockedExpr (BirThread thread)
SmvExpr	threadTerminatedExpr (BirThread thread)
SmvNaryExpr	transCouldBeTakenExpr (Transformation trans)
void	transitions ()
SmvExpr	translate (Expr expr)
void	translateBinaryOp (Expr e1, Expr e2, String op)
SmvExpr	translateGlobal (SmvVar var)
SmvExpr	translateThread (BirThread thread)
void	translateUnaryOp (Expr e, String op)
SmvNaryExpr	transTakenExpr (Transformation trans)
String	waitVar (String var, BirThread thread)
Static Private Methods
SmvExpr	becomes (SmvVar var, SmvExpr expr)
String	currentDir ()
int	parseInt (String s)
Private Attributes
TransSystem	system
PrintWriter	out
boolean	ranVerifier
SmvOptions	options
boolean	liveness
boolean	ctlproperty
boolean	interleaving
int	indentLevel = 0
boolean	newLine = true
Hashtable	varTable = new Hashtable()
Vector	varList = new Vector()
Hashtable	guardTable = new Hashtable()
int	maxCollectionSize
String	threadType
Transformation	currentTrans
SmvExpr	currentGuard
SmvVar	choiceVar
SmvVar	trapVar
SmvVar	runningVar
boolean	doneParsing
boolean	foundFalse
boolean	foundTrace
int	stateCount
Location[]	threadLocs
Transformation	lastTrans
Hashtable	threadTable
Static Private Attributes
final SmvLit	ZERO = new SmvLit("0")
final SmvLit	ONE = new SmvLit("1")
final SmvLit	NOTHREAD = new SmvLit("NoThread")
final String	TRAP_TYPE
final String	LOCK_COUNT_TYPE = "0 .. 3"
Runtime	runtime = Runtime.getRuntime()
final int	BUFSIZE = 50000
byte[]	buffer = new byte[BUFSIZE]

---

Detailed Description

SmvTrans is the main class of the SMV translator, which generates SMV source representing a transition system.

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

 // Parameters 
 TransSystem system = ...;   // the transition system 
 SmvOptions options = new SmvOptions();        // Options 
 options.setSafety(true);          // Safety property 
 options.setInterleaving(true);    // Interleaving (vs. simulataneous) model 
 SmvTrans smv = SmvTrans.translate(sys,options);   // Generate input 
 smv.runSmv();   // Run nusmv 
 BirTrace trace = smv.parseOutput();   // Parse the output 
 

Definition at line 60 of file SmvTrans.java.

---

Member Function Documentation

SmvNaryExpr SmvTrans::addConditionalContext (  SmvNaryExpr   expr, SmvCase   context )  [inline, private]

Add the conditional context to an N-ary AND-expression. The context passed is an SmvCase that is part of a case tree. The condition on every ancestor of the conext is added to the AND-expression. The context can be null, in which case nothing is added. Definition at line 143 of file SmvTrans.java.

SmvExpr SmvTrans::becomes (  SmvVar   var, SmvExpr   expr )  [inline, static, private]

Generate SMV expression that says var becomes expr in next state. To simplify reference assignments (from one var to another), we test to see if the var is an aggregate (which means its a reference) and if the expr is also a variable---in which case we generate a conjunction saying each component is equal (this avoid the multiplication that would otherwise be generated to view the reference as a single value). Definition at line 165 of file SmvTrans.java.

SmvExpr SmvTrans::buildTransExpr (  Transformation   trans, StateVarVector   locals, SmvVar   locVar )  [inline, private]

Build an expression for a given transformation. Definition at line 183 of file SmvTrans.java.

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

Build an SMV expression for a BIR array selection. Reimplemented from ExprSwitch. Definition at line 240 of file SmvTrans.java.

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

Build an SMV expression for a choose() operation. Given choices C0, C1, ..., CN, we generate: case choiceVar = 0 : C0; choiceVar = 1 : C1; ... 1 : CN; esac where choiceVar is an unconstrained variable. Reimplemented from ExprSwitch. Definition at line 293 of file SmvTrans.java.

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

Generate an SMV expression for a BIR dereference. Reimplemented from ExprSwitch. Definition at line 313 of file SmvTrans.java.

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

Build SMV expr to check if object is instanceof class. We use an SMV set expression to test if the refIndex var of the reference is "in" the set of refIndexes of the class/interface. Reimplemented from ExprSwitch. Definition at line 370 of file SmvTrans.java.

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

Build SMV expr to retrieve array length. Reimplemented from ExprSwitch. Definition at line 400 of file SmvTrans.java.

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

Build an SMV expression for a lock test. Reimplemented from ExprSwitch. Definition at line 423 of file SmvTrans.java.

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

Build SMV expression for array allocator. Similar to NewExpr, but must initialize length/contents of array. Reimplemented from ExprSwitch. Definition at line 478 of file SmvTrans.java.

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

Build SMV expression for allocator. Reimplemented from ExprSwitch. Definition at line 525 of file SmvTrans.java.

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

Build SMV expression for record field selection. Reimplemented from ExprSwitch. Definition at line 580 of file SmvTrans.java.

void SmvTrans::checkAssign (  StateVar   lhs, Expr   rhs, SmvVar   var, SmvExpr   value )  [inline, private]

Check an assignment for ClassCastExceptions (updating trapVar). Check an assignment for IntLimitExceptions (updating trapVar). Definition at line 635 of file SmvTrans.java.

SmvVar SmvTrans::declareVar (  String   name, String   smvType, StateVar   source, String   initValue, SmvVar   aggregate, boolean   constrained, SmvVar   deadFlag )  [inline]

Declare an SMV state variable Parameters: name   of variable its   SMV type (or null if it's an aggregate) the   BIR StateVar it represents (a part of) its   initial value (or null if it has none) the   aggregate SmvVar it is nested within (or null) flag   indicating whether var is constrained (has TRANS formula) an   SmvVar that, if false, indicates this variable is dead Definition at line 694 of file SmvTrans.java. Referenced by SmvTypeDecl::caseArray(), SmvTypeDecl::caseBool(), SmvTypeDecl::caseCollection(), SmvTypeDecl::caseEnumerated(), SmvTypeDecl::caseLock(), SmvTypeDecl::caseRange(), SmvTypeDecl::caseRecord(), and SmvTypeDecl::caseRef().

void SmvTrans::declareVariables (    )  [inline, private]

Declare all variables using SmvTypeDecl to walk down through composite types. Definition at line 715 of file SmvTrans.java.

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

Generate DEFINE sectoin, which defines the following symbols: MAX_COLLECT_SIZE Enumeration and constant names T_blocked for each thread T T_terminated for each thread T Definition at line 795 of file SmvTrans.java.

void SmvTrans::fairness (    )  [inline, private]

Generate FAIRNESS clause for each thread T of the form: ! T_idle | T_blocked | T_terminated Definition at line 897 of file SmvTrans.java.

AssignAction SmvTrans::findLocalAssign (  Transformation   trans )  [inline, private]

Finds an assignment to a local variable in the transformation (or returns null if not found). Definition at line 918 of file SmvTrans.java.

List SmvTrans::getCounterExample (    )  [inline]

getCounterExample method comment. Definition at line 937 of file SmvTrans.java.

SmvVar SmvTrans::getVar (  String   name )  [inline, private]

Get SmvVar with given name. Definition at line 946 of file SmvTrans.java.

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

Generate SMV header Definition at line 957 of file SmvTrans.java.

void SmvTrans::init (    )  [inline, private]

Generate INIT formula that sets each non-aggregate variable with an initial value to that value. Reimplemented from Analysis. Definition at line 974 of file SmvTrans.java.

void SmvTrans::initAllComponents (  SmvVar   var, SmvExpr   cond )  [inline, private]

Initialize all components in an SmvVar if indicated condition is true. Definition at line 994 of file SmvTrans.java.

String SmvTrans::locName (  Location   loc )  [inline, private]

Name of location. Definition at line 1027 of file SmvTrans.java.

void SmvTrans::parseLine (  String   line, BirTrace   trace )  [inline, private]

Parse one line of the SMV output file, updating the trace. Definition at line 1064 of file SmvTrans.java.

BirTrace SmvTrans::parseOutput (    )  [inline]

Parse the output of SMV and interpret it as either a violation (sequence of transformations) or as a error-free analysis. Returns: a BirTrace Definition at line 1109 of file SmvTrans.java.

void SmvTrans::parseThreadStep (  String   line, BirTrace   trace )  [inline, private]

Parse line containing update to thread location. Find transformation taken and add to trace. Line of form: threadName_loc = locXXX where XXX is a number. Definition at line 1145 of file SmvTrans.java.

void SmvTrans::parseTrap (  String   line, BirTrace   trace )  [inline, private]

Parse line updating trap variable---record trap name. Definition at line 1174 of file SmvTrans.java.

void SmvTrans::prepareParse (    )  [inline, private]

Prepare to parse SMV output file Definition at line 1187 of file SmvTrans.java.

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

Support for printing things nicely indented. Definition at line 1205 of file SmvTrans.java.

void SmvTrans::printVariableDecls (    )  [inline, private]

Print variable declarations Aggregate variables (e.g., arrays, records, collections, refs) have a null type and are printed as comments. Definition at line 1230 of file SmvTrans.java.

void SmvTrans::recordGlobalVarAssignments (  SmvExpr   lhs, SmvExpr   rhs, SmvCase   context )  [inline, private]

Records updates to globals made by an assignment. If the LHS may reference more than one variable (e.g., contains a pointer deref or array indexing) then the LHS expression will be an SmvCase whose leaves are all the possible updated variables. In this case, we recurse through all cases of the tree until we reach a leaf (SmvVar). When an SmvVar is finally reached, we add a conditional update to that variable to the value given by the RHS expression on that condition that the current trans is taken *and* the specific case context is true (i.e., all conditions for all cases we're contained in are true). Definition at line 1330 of file SmvTrans.java.

void SmvTrans::recordGlobalVarUpdates (    )  [inline, private]

Records updates to global variables made by the current trans. Definition at line 1361 of file SmvTrans.java.

void SmvTrans::recordLockStatusUpdates (  LockAction   action )  [inline, private]

Record updates to the lock variables by a lock action. Definition at line 1380 of file SmvTrans.java.

void SmvTrans::recordThreadStatusUpdates (  ThreadAction   action )  [inline, private]

Records updates to the status of the threads. A start action for a thread changes its T_active var to 1. Definition at line 1519 of file SmvTrans.java.

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

Return the refIndex of a BIR state variable (i.e., its position in the universal reference type refAny). Definition at line 1532 of file SmvTrans.java.

SmvLit SmvTrans::refValue (  int   refIndex, int   instNum )  [inline, private]

Build SMV reference value from refIndex and instNum values. Definition at line 1542 of file SmvTrans.java.

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

Run SMV translator, generate each part of the output in turn. Definition at line 1550 of file SmvTrans.java.

String SmvTrans::runSmv (    )  [inline]

Run SMV. The translator must have been executed for the transition system (the file NAME.trans must exist and contain the translated input). Returns: the output of SMV (as a String) Definition at line 1569 of file SmvTrans.java.

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

Generate SMV variables Definition at line 1596 of file SmvTrans.java.

SmvExpr SmvTrans::threadBlockedExpr (  BirThread   thread )  [inline, private]

Build an expression that is true if the thread is blocked. The thread is blocked if it is in a location and the guards for all transforms out of that location are false. If there are no transforms out of the location, the thread is considered terminated, not blocked. Definition at line 1615 of file SmvTrans.java.

SmvExpr SmvTrans::threadTerminatedExpr (  BirThread   thread )  [inline, private]

Build expression that is true if a thread is terminated. A thread is terminated if it is in a location with no out transformations. Definition at line 1651 of file SmvTrans.java.

SmvNaryExpr SmvTrans::transCouldBeTakenExpr (  Transformation   trans )  [inline, private]

Generate an expression that is true if a transformation could be taken. Similar to transTakenExpr, except we do not require the location be updated or the thread be running. Definition at line 1669 of file SmvTrans.java.

SmvNaryExpr SmvTrans::transTakenExpr (  Transformation   trans )  [inline, private]

Build an expression that is true if a given transformation is taken. Definition at line 1812 of file SmvTrans.java.

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

Generate a TRANS formula for each thread and global variable. Definition at line 1688 of file SmvTrans.java.

SmvTrans SmvTrans::translate (  TransSystem   system, SmvOptions   options, PrintWriter   out )  [inline, static]

Generate SMV source representing a transition system. As above, but the SMV is written to the PrintWriter provided. Parameters: system   the transition system out   the PrintWriter to write the SMV to Returns: the SmvTrans control object Definition at line 1754 of file SmvTrans.java.

SmvTrans SmvTrans::translate (  TransSystem   system, SmvOptions   options )  [inline, static]

Generate SMV source representing a transition system. The SMV input is written to a file NAME.trans where NAME is the name of the transition system. A set of options can be provided in a SmvOptions object. Parameters: system   the transition system options   the SMV verifier options Returns: the SmvTrans control object Definition at line 1730 of file SmvTrans.java.

SmvExpr SmvTrans::translate (  Expr   expr )  [inline, private]

Translate a BIR expression to an SmvExpr Definition at line 1715 of file SmvTrans.java.

SmvExpr SmvTrans::translateGlobal (  SmvVar   var )  [inline, private]

Return update expression for global variable (most work done in SmvVar). Definition at line 1765 of file SmvTrans.java.

SmvExpr SmvTrans::translateThread (  BirThread   thread )  [inline, private]

Build the TRANS expression for a thread. Definition at line 1773 of file SmvTrans.java.

---

Member Data Documentation

final String SmvTrans::TRAP_TYPE [static, private]

Initial value: "{ None, NullPointerException, ArrayBoundsException, ClassCastException, RangeLimitException, CollectionLimitException, ArrayLimitException }" Definition at line 95 of file SmvTrans.java.

---

The documentation for this class was generated from the following file:

• SmvTrans.java

---