gov.nasa.jpf.util.event

Class EventTree

java.lang.Object

gov.nasa.jpf.util.event.EventTree

All Implemented Interfaces:

EventConstructor

Direct Known Subclasses:

EventForest, TestEventTree

public class EventTree
extends java.lang.Object
implements EventConstructor

an abstract class that creates Event trees While there is no need to provide specialized Event types or additional event constructors, concrete subclasses have to provide a createRoot() implementation. A typical implementation looks like this class MyTree extends EventTree {

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	CONFIG_KEY
protected Event	root

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	EventTree()
protected	EventTree(Event root)

Method Summary

Modifier and Type	Method and Description
void	addPath(Event... path) extend this tree with a new path
boolean	checkPath(Event lastEvent) this should be overridden in case we want to check if this is an expected trace The generic form can only check if this is a valid end event.
boolean	checkPath(Event lastEvent, java.lang.String[] pathSpecs)
Event	createRoot() this is our purpose in life, which has to be provided by concrete subclasses
int	getMaxDepth()
float	getPathCoverage() override this if the concrete model keeps track of coverage
Event	getRoot()
Event	interleave(Event... otherTrees)
EventTree	interleave(EventTree... otherTrees)
boolean	isCompletelyCovered() override this if the concrete model can keep track of coverage call at the end of execution
void	printPaths()
void	printTree()
Event	removeSource(java.lang.Object source)
java.util.List<Event>	visibleEndEvents()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface gov.nasa.jpf.util.event.EventConstructor

alternatives, anyCombination, anyPermutation, event, event, generatePermutation, iteration, sequence

Field Detail

CONFIG_KEY

public static final java.lang.String CONFIG_KEY

See Also:

Constant Field Values

root

protected Event root

Constructor Detail

EventTree

protected EventTree()

EventTree

protected EventTree(Event root)

Method Detail

createRoot

public Event createRoot()

this is our purpose in life, which has to be provided by concrete subclasses

getRoot

public Event getRoot()

visibleEndEvents

public java.util.List<Event> visibleEndEvents()

printPaths

public void printPaths()

printTree

public void printTree()

checkPath

public boolean checkPath(Event lastEvent)

this should be overridden in case we want to check if this is an expected trace The generic form can only check if this is a valid end event. To check for a whole trace, implementors should keep some sort of expected event specs

checkPath

public boolean checkPath(Event lastEvent,
                         java.lang.String[] pathSpecs)

getPathCoverage

public float getPathCoverage()

override this if the concrete model keeps track of coverage

Returns:

[0.0..1.0]

isCompletelyCovered

public boolean isCompletelyCovered()

override this if the concrete model can keep track of coverage call at the end of execution

addPath

public void addPath(Event... path)

extend this tree with a new path

interleave

public Event interleave(Event... otherTrees)

interleave

public EventTree interleave(EventTree... otherTrees)

removeSource

public Event removeSource(java.lang.Object source)

getMaxDepth

public int getMaxDepth()