---

DSpinTrans Class Reference

Inheritance diagram for DSpinTrans:[legend]Collaboration diagram for DSpinTrans:[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 ()
DSpinOptions	getDSpinOptions ()
BirTrace	parseOutput ()
String	runSpin ()
void	translateLocation (Location loc)
Static Public Methods
DSpinTrans	translate (TransSystem system)
DSpinTrans	translate (TransSystem system, DSpinOptions options)
DSpinTrans	translate (TransSystem system, DSpinOptions options, PrintWriter out)
Static Public Attributes
final String	normal = "NORMAL_CASE"
Private Methods
String	actionId ()
String	actionIdWithCommas ()
CaseNode	applyTo (Expr expr)
void	definitions ()
String	dSpinTypeName (Type type, Object o)
String	execAndWait (String command, boolean verbose)
String	getSimpleResult ()
boolean	guardPresent (Transformation trans)
void	header ()
void	initBlock ()
boolean	isIfBranch (TransVector outTrans)
boolean	nonNegative (Expr expr)
void	parseLine (String line, BirTrace trace)
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)
DSpinTrans	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
	DSpinTrans (TransSystem system, DSpinOptions options, PrintWriter out)
String	currentDir ()
String	locLabel (Location loc)
String	locLabel (Location loc1, int branch, Location loc2)
int	parseInt (String s)
Private Attributes
TransSystem	system
PrintWriter	out
DSpinTypeName	namer
int	indentLevel = 0
boolean	inDefine = false
boolean	newLine = true
boolean	resetTemp = false
boolean	resetNew = false
Transformation	currentTrans
int	actionNum
DSpinOptions	options
boolean	ranVerifier = false
Static Private Attributes
String	ccName = "gcc"
String	includeDir = ""
Runtime	runtime = Runtime.getRuntime()
final int	BUFSIZE = 50000
byte[]	buffer = new byte[BUFSIZE]

---

Detailed Description

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

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

 // Parameters 
 TransSystem system = ...;   // the transition system 
 DSpinOptions options = new DSpinOptions();   // SPIN options 
 options.setMemoryLimit(256);            // set various options 
 ... 
 DSpinTrans spin = DSpinTrans.translate(system,options); // invoke translator 
 spin.runSpin();                           // Run SPIN on generated PROMELA 
 BirTrace trace = spin.parseOutput();      // Parse output as BIR trace 
 

Definition at line 64 of file DSpinTrans.java.

---

Member Function Documentation

List DSpinTrans::getCounterExample (    )  [inline]

getCounterExample method comment. Definition at line 583 of file DSpinTrans.java.

BirTrace DSpinTrans::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 801 of file DSpinTrans.java.

String DSpinTrans::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.dprom must exist and contain the translated PROMELA). Returns: the output of 'pan' (as a String) Definition at line 961 of file DSpinTrans.java.

DSpinTrans DSpinTrans::translate (  TransSystem   system, DSpinOptions   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 DSpinTrans control object Definition at line 1097 of file DSpinTrans.java.

DSpinTrans DSpinTrans::translate (  TransSystem   system, DSpinOptions   options )  [inline, static]

Generate PROMELA source representing a transition system. The PROMELA is written to a file NAME.dprom where NAME is the name of the transition system. A set of options can be provided in a DSpinOptions object. Parameters: system   the transition system options   the SPIN verifier options Returns: the SpinTrans control object Definition at line 1072 of file DSpinTrans.java.

DSpinTrans DSpinTrans::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 DSpinTrans control object Definition at line 1058 of file DSpinTrans.java.

---

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

• DSpinTrans.java

---