gov.nasa.jpf.util.event

Class EventChoiceGenerator

java.lang.Object

gov.nasa.jpf.vm.ChoiceGeneratorBase<Event>

gov.nasa.jpf.util.event.EventChoiceGenerator

All Implemented Interfaces:

ChoiceGenerator<Event>, java.lang.Cloneable

public class EventChoiceGenerator
extends ChoiceGeneratorBase<Event>

ChoiceGenerator for Events. This is basically just a pointer into the event tree

Field Summary

Fields

Modifier and Type	Field and Description
protected Event	base
protected EventContext	ctx
protected Event	cur
protected int	nProcessed

Fields inherited from class gov.nasa.jpf.vm.ChoiceGeneratorBase

attr, id, idRef, insn, isCascaded, isDone, MARKER, prev, random, stateId, ti

Constructor Summary

Constructors

Constructor and Description
EventChoiceGenerator(java.lang.String id, Event base)
EventChoiceGenerator(java.lang.String id, Event base, EventContext ctx)

Method Summary

Modifier and Type	Method and Description
void	addChoice(Event newEvent)
void	advance() advance to the next choice.
boolean	containsMatchingChoice(Predicate<Event> predicate)
Event[]	getAllChoices()
Event	getChoice(int idx) explicit choice enumeration.
java.lang.Class<Event>	getChoiceType()
protected Event[]	getFirstNChoices(int n)
static EventChoiceGenerator	getNext(SystemState ss, java.lang.String id, Event base, EventContext ctx) convenience method to get successors from current CG chain
Event	getNextChoice()
Event[]	getProcessedChoices()
int	getProcessedNumberOfChoices()
EventChoiceGenerator	getSuccessor(java.lang.String id)
EventChoiceGenerator	getSuccessor(java.lang.String id, EventContext ctx)
int	getTotalNumberOfChoices()
Event[]	getUnprocessedChoices()
boolean	hasMoreChoices()
void	reset() this has to reset the CG to its initial state, which includes resetting 'isDone'
void	setContextExpander(EventContext ctx)
java.lang.String	toString()

Methods inherited from class gov.nasa.jpf.vm.ChoiceGeneratorBase

addAttr, advance, attrIterator, attrIterator, clone, deepClone, getAll, getAllOfType, getAttr, getAttr, getCascade, getCascadedParent, getId, getIdRef, getInsn, getNextAttr, getNumberOfParents, getPreviousChoiceGenerator, getPreviousChoiceGeneratorOfType, getSourceLocation, getStateId, getThreadInfo, hasAttr, hasAttr, hasAttrValue, init, isCascaded, isDone, isProcessed, isSchedulingPoint, randomize, removeAttr, reorder, replaceAttr, select, setAttr, setCascaded, setContext, setCurrent, setDone, setId, setIdRef, setInsn, setPreviousChoiceGenerator, setStateId, setThreadInfo, supportsReordering, useRandomization

Methods inherited from class java.lang.Object

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

Field Detail

base

protected Event base

cur

protected Event cur

nProcessed

protected int nProcessed

ctx

protected EventContext ctx

Constructor Detail

EventChoiceGenerator

public EventChoiceGenerator(java.lang.String id,
                            Event base)

EventChoiceGenerator

public EventChoiceGenerator(java.lang.String id,
                            Event base,
                            EventContext ctx)

Method Detail

getNext

public static EventChoiceGenerator getNext(SystemState ss,
                                           java.lang.String id,
                                           Event base,
                                           EventContext ctx)

convenience method to get successors from current CG chain

getChoice

public Event getChoice(int idx)

Description copied from class: ChoiceGeneratorBase

explicit choice enumeration. Override if supported

Specified by:

getChoice in interface ChoiceGenerator<Event>

Overrides:

getChoice in class ChoiceGeneratorBase<Event>

Returns:

choice value or null if not supported

setContextExpander

public void setContextExpander(EventContext ctx)

containsMatchingChoice

public boolean containsMatchingChoice(Predicate<Event> predicate)

addChoice

public void addChoice(Event newEvent)

getSuccessor

public EventChoiceGenerator getSuccessor(java.lang.String id)

getSuccessor

public EventChoiceGenerator getSuccessor(java.lang.String id,
                                         EventContext ctx)

getNextChoice

public Event getNextChoice()

hasMoreChoices

public boolean hasMoreChoices()

advance

public void advance()

Description copied from interface: ChoiceGenerator

advance to the next choice. This is the only method that really advances our enumeration

reset

public void reset()

Description copied from interface: ChoiceGenerator

this has to reset the CG to its initial state, which includes resetting 'isDone'

getTotalNumberOfChoices

public int getTotalNumberOfChoices()

getProcessedNumberOfChoices

public int getProcessedNumberOfChoices()

toString

public java.lang.String toString()

Overrides:

toString in class ChoiceGeneratorBase<Event>

getChoiceType

public java.lang.Class<Event> getChoiceType()

getFirstNChoices

protected Event[] getFirstNChoices(int n)

getAllChoices

public Event[] getAllChoices()

Specified by:

getAllChoices in interface ChoiceGenerator<Event>

Overrides:

getAllChoices in class ChoiceGeneratorBase<Event>

getProcessedChoices

public Event[] getProcessedChoices()

Specified by:

getProcessedChoices in interface ChoiceGenerator<Event>

Overrides:

getProcessedChoices in class ChoiceGeneratorBase<Event>

getUnprocessedChoices

public Event[] getUnprocessedChoices()

Specified by:

getUnprocessedChoices in interface ChoiceGenerator<Event>

Overrides:

getUnprocessedChoices in class ChoiceGeneratorBase<Event>