gov.nasa.jpf.util.event

Class CheckEvent

java.lang.Object

gov.nasa.jpf.util.event.Event

gov.nasa.jpf.util.event.SystemEvent

gov.nasa.jpf.util.event.CheckEvent

All Implemented Interfaces:

java.lang.Cloneable

public abstract class CheckEvent
extends SystemEvent

a pseudo event that encapsulates a (possibly composed) check This event type uses 'alt' for disjunction and 'next' for conjunction if they point to CheckEvents

Field Summary

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

alt, arguments, name, next, prev, source

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	CheckEvent(java.lang.String name, java.lang.Object... arguments)

Method Summary

Modifier and Type	Method and Description
CheckEvent	and(CheckEvent andCheck)
boolean	check(MJIEnv env, int objRef) conjunctions and disjunctions of this check event
abstract boolean	evaluate(MJIEnv env, int objRef) this is the single check condition for this event
java.lang.String	getExpression()
CheckEvent	or(CheckEvent orCheck)
void	process(MJIEnv env, int objRef) generic check evaluation that throws assertions if failed

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

isSystemEvent

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

addAlternative, addNext, addPath, clone, collectEndEvents, collectTrace, createClonedSequence, deepClone, endEvent, endEvents, equals, getAlt, getAlternatives, getArgument, getArguments, getLastAlt, getMaxDepth, getName, getNext, getNumberOfAlternatives, getPath, getPathLength, getPathString, getPrev, getSource, hasAlternatives, hashCode, interleave, isEndOfTrace, isNoEvent, printPath, printTree, process, removeSource, replaceWith, replaceWithAlternativesFrom, replaceWithSequenceFrom, setAlt, setLinksFrom, setNext, setPrev, setProcessed, setSource, toString, unlinkedClone, visibleEndEvents

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

CheckEvent

protected CheckEvent(java.lang.String name,
                     java.lang.Object... arguments)

Method Detail

evaluate

public abstract boolean evaluate(MJIEnv env,
                                 int objRef)

this is the single check condition for this event

check

public boolean check(MJIEnv env,
                     int objRef)

conjunctions and disjunctions of this check event

process

public void process(MJIEnv env,
                    int objRef)

generic check evaluation that throws assertions if failed

Overrides:

process in class SystemEvent

or

public CheckEvent or(CheckEvent orCheck)

and

public CheckEvent and(CheckEvent andCheck)

getExpression

public java.lang.String getExpression()