---

BirTrace Class Reference

List of all members.

Public Methods
	BirTrace (TransSystem system)
	BirTrace (TransSystem system, java.util.List l)
void	addTrans (Transformation trans)
void	done ()
String	evalExpr (Expr expr, int stateIndex)
int	getNumActions ()
BirState	getState (int stateIndex)
TransSystem	getTransSystem ()
TransVector	getTransVector ()
Action	getTrapAction ()
String	getTrapName ()
Transformation	getTrapTrans ()
boolean	isComplete ()
boolean	isDepthExceeded ()
boolean	isLimitViolation ()
boolean	isOutOfMemory ()
boolean	isVectorExceeded ()
boolean	isVerified ()
void	print (boolean showStates)
void	setChoice (int actionNum, int choiceNum)
void	setDepthExceeded ()
void	setOutOfMemory ()
void	setTrap (String trapName, Transformation trapTrans, int actionNum)
void	setVectorExceeded ()
void	setVerified (boolean verified)
Private Methods
void	processTrail (java.util.List l)
Private Attributes
boolean	verified
boolean	completed
boolean	limitviolation
boolean	outofmemory
boolean	depthexceeded
boolean	vectorexceeded
TransSystem	system
TransVector	transVector = new TransVector()
Vector	choiceVector = new Vector()
String	trapName
Transformation	currentTrans
Transformation	trapTrans
int	trapActionNum
int	numActions = 0
BirState[]	state

---

Detailed Description

A BIR Trace, which represents either a counterexample to a property, a positive result (i.e., property holds), or a reason for an incomplete model check.

A BIR trace is constructed by a translator after parsing the output of a verifier and interpretting it as a sequence of transitions through the BIR transition system. The trace may end with a trap (e.g., NullPointerException).

Traps indicate run-time errors in the program or that fixed resource bounds on the model have been exceeded. There are three such traps :

• RangeLimitException : integer value is out of specified range
• ArraySizeLimitException : attempt to allocate an array bigger than the defined limit
• CollectionSizeLimitException : attempt to allocate more than the defined maximum number of instances

In addition to the transformations, the constructor of the trace must specify certain CHOICES made by actions in the trace:

• If an AssignAction performs a nondeterministic assignment, the specific value assigned must be recorded as the CHOICE for that action.
• If an AssignAction executes an allocator, the instance number allocated must be recorded as the CHOICE for that action (this is not used for dSPIN).

Once all the transformations and choices have been added, invoking the done() method will run the BIR simulator and generate the BIR states for the trace (a state is generated for each action in the trace).

The trace can be queried to determine if the check:

• Verified the property (isVerified())
• Failed to verify the property (!isVerified())
• Failed due to a model resource bounds violation (isLimitViolation())
• Failed due to a checker problem, e.g., insufficient memory (!isComplete())

Definition at line 85 of file BirTrace.java.

---

Member Function Documentation

void BirTrace::addTrans (  Transformation   trans )  [inline]

Add a transformation to the end of the trace. Definition at line 119 of file BirTrace.java. Referenced by SmvTrans::parseThreadStep(), and processTrail().

void BirTrace::done (    )  [inline]

Run simulator to complete construction of trace. Definition at line 130 of file BirTrace.java. Referenced by SmvTrans::parseOutput(), DSpinTrans::parseOutput(), and processTrail().

void BirTrace::processTrail (  java.util.List   l )  [inline, private]

Parse a line of the spin simulator output, possibly adding a transform to the trace. Most of the lines (generated by spin) we ignore, but the PROMELA contains special print statements that generate lines containing the strings "BIR: L T A S" or "BIR? A C". The string "BIR: L T A S" is printed when executing an action: L is the location number, T is the index of the transform out of that location, A is the index of the action in the transform (0 is the guard, the actions begin with 1), and S is the status of the action (usually OK, but may be a trap name). The string "BIR? A C" is printed when an action makes a choice (e.g., choose expression): A is the action index (the transformation is assumed to be the last one for which a "BIR: ..." was seen), and C is an integer representing the choice. Definition at line 229 of file BirTrace.java.

void BirTrace::setChoice (  int   actionNum, int   choiceNum )  [inline]

Set the choice number of the given action of the current transformation. Definition at line 276 of file BirTrace.java. Referenced by processTrail().

void BirTrace::setTrap (  String   trapName, Transformation   trapTrans, int   actionNum )  [inline]

Set the trap info for the trace. Definition at line 295 of file BirTrace.java. Referenced by SmvTrans::parseTrap(), and processTrail().

---

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

• BirTrace.java

---