SimpleDot (JPF API)

java.lang.Object
- gov.nasa.jpf.ListenerAdapter
- - gov.nasa.jpf.listener.SimpleDot

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, VMListener
```
public class SimpleDot
extends ListenerAdapter
```
an alternative Graphviz dot-file generator for simple,educational state graphs except of creating funny wallpapers, it doesn't help much in real life if the state count gets > 50, but for the small ones it's actually quite readable. Good for papers. normal states are labeled with their numeric ids, end states are double circled. start, end and error states are color filled edges have two labels: the choice value at the beginning and the CG cause at the end. Only the first incoming edge into a state shows the CG cause we only render one backtrack edge per from-state <2do> GraphViz doesn't seem to handle color or fontname for head/tail labels correctly

Field Summary

Fields
Modifier and Type	Field and Description
`protected String`	`app`
`protected String`	`backtrackEdgeAttrs`
`protected String`	`endNodeAttrs`
`protected String`	`errorNodeAttrs`
`protected File`	`file`
`protected String`	`genericEdgeAttrs`
`protected String`	`genericNodeAttrs`
`protected String`	`graphAttrs`
`protected ElementInfo`	`lastEi`
`protected String`	`lastErrorId`
`protected int`	`lastId`
`protected ThreadInfo`	`lastTi`
`protected String`	`newEdgeAttrs`
`protected boolean`	`printFile`
`protected PrintWriter`	`pw`
`protected String`	`restoreEdgeAttrs`
`protected boolean`	`showTarget`
`protected String`	`startNodeAttrs`
`protected String`	`visitedEdgeAttrs`
`protected VM`	`vm`

Constructor Summary

Constructors
Constructor and Description

SimpleDot(Config config, JPF jpf)

Constructors
Constructor and Description
`SimpleDot(Config config, JPF jpf)`

Method Summary

Methods
Modifier and Type	Method and Description
`protected static String`	`getClassObjectRef(int ref)`
`protected String`	`getError(Search search)`
`protected String`	`getFieldAccessCG(FieldInstruction insn)`
`protected static String`	`getInstanceRef(int ref)`
`protected String`	`getInvokeCG(InvokeInstruction insn)`
`protected String`	`getLastChoice()`
`protected String`	`getLockCG(LockInstruction insn)`
`protected String`	`getNativeExecCG(EXECUTENATIVE insn)`
`protected String`	`getNextCG()`
`protected String`	`getStateId(int id)`
`void`	`objectWait(VM vm, ThreadInfo ti, ElementInfo ei)` notify if a wait() is executed
`protected void`	`printBacktrack(String fromState, String toState)`
`protected void`	`printEndState(String stateId)`
`protected void`	`printErrorState(String error)`
`protected void`	`printHeader()`
`protected void`	`printRestored(String fromState, String toState)`
`protected void`	`printStartState(String stateId)`
`protected void`	`printTransition(String fromState, String toState, String choiceVal, String cgCause)`
`void`	`publishFinished(Publisher publisher)`
`void`	`searchFinished(Search search)` we're done, either with or without a preceeding error
`void`	`searchStarted(Search search)` we get this after we enter the search loop, but BEFORE the first forward
`void`	`stateAdvanced(Search search)` got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set
`void`	`stateBacktracked(Search search)` state was backtracked one step
`void`	`stateRestored(Search search)` a previously generated state was restored (can be on a completely different path)
`void`	`threadStarted(VM vm, ThreadInfo ti)` new Thread entered run() method

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

graphAttrs
```
protected String graphAttrs
```

genericNodeAttrs
```
protected String genericNodeAttrs
```

genericEdgeAttrs
```
protected String genericEdgeAttrs
```

startNodeAttrs
```
protected String startNodeAttrs
```

endNodeAttrs
```
protected String endNodeAttrs
```

errorNodeAttrs
```
protected String errorNodeAttrs
```

newEdgeAttrs
```
protected String newEdgeAttrs
```

visitedEdgeAttrs
```
protected String visitedEdgeAttrs
```

backtrackEdgeAttrs
```
protected String backtrackEdgeAttrs
```

restoreEdgeAttrs
```
protected String restoreEdgeAttrs
```

showTarget
```
protected boolean showTarget
```

printFile
```
protected boolean printFile
```

vm
```
protected VM vm
```

app
```
protected String app
```

file
```
protected File file
```

pw
```
protected PrintWriter pw
```

lastId
```
protected int lastId
```

lastErrorId
```
protected String lastErrorId
```

lastEi
```
protected ElementInfo lastEi
```

lastTi
```
protected ThreadInfo lastTi
```

Constructor Detail

SimpleDot

public SimpleDot(Config config,
         JPF jpf)

Method Detail
- searchStarted
```
public void searchStarted(Search search)
```
  Description copied from interface: SearchListener
  
  we get this after we enter the search loop, but BEFORE the first forward
  
  Specified by:
  
  searchStarted in interface SearchListener
  
  Overrides:
  
  searchStarted in class ListenerAdapter
- stateAdvanced
```
public void stateAdvanced(Search search)
```
  Description copied from interface: SearchListener
  
  got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set
  
  Specified by:
  
  stateAdvanced in interface SearchListener
  
  Overrides:
  
  stateAdvanced in class ListenerAdapter
- stateBacktracked
```
public void stateBacktracked(Search search)
```
  Description copied from interface: SearchListener
  
  state was backtracked one step
  
  Specified by:
  
  stateBacktracked in interface SearchListener
  
  Overrides:
  
  stateBacktracked in class ListenerAdapter
- stateRestored
```
public void stateRestored(Search search)
```
  Description copied from interface: SearchListener
  
  a previously generated state was restored (can be on a completely different path)
  
  Specified by:
  
  stateRestored in interface SearchListener
  
  Overrides:
  
  stateRestored in class ListenerAdapter
- searchFinished
```
public void searchFinished(Search search)
```
  Description copied from interface: SearchListener
  
  we're done, either with or without a preceeding error
  
  Specified by:
  
  searchFinished in interface SearchListener
  
  Overrides:
  
  searchFinished in class ListenerAdapter
- threadStarted
```
public void threadStarted(VM vm,
                 ThreadInfo ti)
```
  Description copied from interface: VMListener
  
  new Thread entered run() method
  
  Specified by:
  
  threadStarted in interface VMListener
  
  Overrides:
  
  threadStarted in class ListenerAdapter
- objectWait
```
public void objectWait(VM vm,
              ThreadInfo ti,
              ElementInfo ei)
```
  Description copied from interface: VMListener
  
  notify if a wait() is executed
  
  Specified by:
  
  objectWait in interface VMListener
  
  Overrides:
  
  objectWait in class ListenerAdapter
- publishFinished
```
public void publishFinished(Publisher publisher)
```
  Specified by:
  
  publishFinished in interface PublisherExtension
  
  Overrides:
  
  publishFinished in class ListenerAdapter
- getStateId
```
protected String getStateId(int id)
```
- getLastChoice
```
protected String getLastChoice()
```
- getNextCG
```
protected String getNextCG()
```
- getNativeExecCG
```
protected String getNativeExecCG(EXECUTENATIVE insn)
```
- getFieldAccessCG
```
protected String getFieldAccessCG(FieldInstruction insn)
```
- getLockCG
```
protected String getLockCG(LockInstruction insn)
```
- getInvokeCG
```
protected String getInvokeCG(InvokeInstruction insn)
```
- getError
```
protected String getError(Search search)
```
- getInstanceRef
```
protected static String getInstanceRef(int ref)
```
- getClassObjectRef
```
protected static String getClassObjectRef(int ref)
```
- printHeader
```
protected void printHeader()
```
- printTransition
```
protected void printTransition(String fromState,
                   String toState,
                   String choiceVal,
                   String cgCause)
```
- printBacktrack
```
protected void printBacktrack(String fromState,
                  String toState)
```
- printRestored
```
protected void printRestored(String fromState,
                 String toState)
```
- printStartState
```
protected void printStartState(String stateId)
```
- printEndState
```
protected void printEndState(String stateId)
```
- printErrorState
```
protected void printErrorState(String error)
```

Class SimpleDot

Field Summary

Constructor Summary

Method Summary

Methods inherited from class gov.nasa.jpf.ListenerAdapter

Methods inherited from class java.lang.Object

Field Detail

graphAttrs

genericNodeAttrs

genericEdgeAttrs

startNodeAttrs

endNodeAttrs

errorNodeAttrs

newEdgeAttrs

visitedEdgeAttrs

backtrackEdgeAttrs

restoreEdgeAttrs

showTarget

printFile

vm

app

file

pw

lastId

lastErrorId

lastEi

lastTi

Constructor Detail

SimpleDot

Method Detail

searchStarted

stateAdvanced

stateBacktracked

stateRestored

searchFinished

threadStarted

objectWait

publishFinished

getStateId

getLastChoice

getNextCG

getNativeExecCG

getFieldAccessCG

getLockCG

getInvokeCG

getError

getInstanceRef

getClassObjectRef

printHeader

printTransition

printBacktrack

printRestored

printStartState

printEndState

printErrorState