gov.nasa.jpf.vm.choice

Class InvocationCG

java.lang.Object

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

gov.nasa.jpf.vm.choice.InvocationCG

All Implemented Interfaces:

ChoiceGenerator<Invocation>, java.lang.Cloneable

public class InvocationCG
extends ChoiceGeneratorBase<Invocation>

ChoiceGenerator that represents method calls

Field Summary

Fields

Modifier and Type	Field and Description
protected Invocation	cur
protected java.util.List<Invocation>	invokes
protected java.util.ListIterator<Invocation>	it

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
InvocationCG(java.lang.String id, java.util.List<Invocation> invokes)

Method Summary

Modifier and Type	Method and Description
void	advance() advance to the next choice.
Invocation	getChoice(int idx) explicit choice enumeration.
java.lang.Class<Invocation>	getChoiceType()
Invocation	getNextChoice()
int	getProcessedNumberOfChoices()
int	getTotalNumberOfChoices()
boolean	hasMoreChoices()
void	printOn(java.io.PrintWriter pw)
ChoiceGenerator<Invocation>	randomize() turn the order of choices random (if it isn't already).
void	reset() this has to reset the CG to its initial state, which includes resetting 'isDone'
java.lang.String	toString()

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

addAttr, advance, attrIterator, attrIterator, clone, deepClone, getAll, getAllChoices, getAllOfType, getAttr, getAttr, getCascade, getCascadedParent, getId, getIdRef, getInsn, getNextAttr, getNumberOfParents, getPreviousChoiceGenerator, getPreviousChoiceGeneratorOfType, getProcessedChoices, getSourceLocation, getStateId, getThreadInfo, getUnprocessedChoices, hasAttr, hasAttr, hasAttrValue, init, isCascaded, isDone, isProcessed, isSchedulingPoint, 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

invokes

protected java.util.List<Invocation> invokes

cur

protected Invocation cur

it

protected java.util.ListIterator<Invocation> it

Constructor Detail

InvocationCG

public InvocationCG(java.lang.String id,
                    java.util.List<Invocation> invokes)

Method Detail

getChoice

public Invocation getChoice(int idx)

Description copied from class: ChoiceGeneratorBase

explicit choice enumeration. Override if supported

Specified by:

getChoice in interface ChoiceGenerator<Invocation>

Overrides:

getChoice in class ChoiceGeneratorBase<Invocation>

Returns:

choice value or null if not supported

advance

public void advance()

Description copied from interface: ChoiceGenerator

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

getChoiceType

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

getNextChoice

public Invocation getNextChoice()

getProcessedNumberOfChoices

public int getProcessedNumberOfChoices()

getTotalNumberOfChoices

public int getTotalNumberOfChoices()

hasMoreChoices

public boolean hasMoreChoices()

randomize

public ChoiceGenerator<Invocation> randomize()

Description copied from interface: ChoiceGenerator

turn the order of choices random (if it isn't already). Only drawback of this generic method (which might be a decorator factory) is that our type layer (e.g. IntChoiceGenerator) has to guarantee type safety. But hey - this is the first case where we can use covariant return types! NOTES: - this method may alter this ChoiceGenerator and return that or return a new "decorated" version. - random data can be read from the "Random random" field in this class.

Specified by:

randomize in interface ChoiceGenerator<Invocation>

Overrides:

randomize in class ChoiceGeneratorBase<Invocation>

toString

public java.lang.String toString()

Overrides:

toString in class ChoiceGeneratorBase<Invocation>

printOn

public void printOn(java.io.PrintWriter pw)

reset

public void reset()

Description copied from interface: ChoiceGenerator

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