gov.nasa.jpf.util.event

Class TestEventTree

java.lang.Object

gov.nasa.jpf.util.event.EventTree

gov.nasa.jpf.util.event.TestEventTree

All Implemented Interfaces:

EventConstructor

public class TestEventTree
extends EventTree

EventTree that can check traces and coverage against expected traces for testing purposes. This has little purpose except of keeping tree spec and expected traces together in the same native class, so that we can check paths ad hoc from regression tests without having to create expected path strings in the JPF part of the test, only to translate them into native strings

Field Summary

Fields

Modifier and Type	Field and Description
protected java.lang.String[]	expected

Fields inherited from class gov.nasa.jpf.util.event.EventTree

CONFIG_KEY, root

Constructor Summary

Constructors

Constructor and Description
TestEventTree()
TestEventTree(Event root)

Method Summary

Modifier and Type	Method and Description
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.
float	getPathCoverage(java.lang.String[] expected)
boolean	isCompletelyCovered() override this if the concrete model can keep track of coverage call at the end of execution
boolean	isCompletelyCovered(java.lang.String[] expected)

Methods inherited from class gov.nasa.jpf.util.event.EventTree

addPath, checkPath, createRoot, getMaxDepth, getPathCoverage, getRoot, interleave, interleave, printPaths, printTree, removeSource, 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

expected

protected java.lang.String[] expected

Constructor Detail

TestEventTree

public TestEventTree()

TestEventTree

public TestEventTree(Event root)

Method Detail

checkPath

public boolean checkPath(Event lastEvent)

Description copied from class: EventTree

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

Overrides:

checkPath in class EventTree

isCompletelyCovered

public boolean isCompletelyCovered()

Description copied from class: EventTree

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

Overrides:

isCompletelyCovered in class EventTree

isCompletelyCovered

public boolean isCompletelyCovered(java.lang.String[] expected)

getPathCoverage

public float getPathCoverage(java.lang.String[] expected)