gov.nasa.jpf.vm.choice

Class IntIntervalGenerator

java.lang.Object

gov.nasa.jpf.vm.ChoiceGeneratorBase<java.lang.Integer>

gov.nasa.jpf.vm.choice.IntIntervalGenerator

All Implemented Interfaces:

ChoiceGenerator<java.lang.Integer>, IntChoiceGenerator, java.lang.Cloneable

public class IntIntervalGenerator
extends ChoiceGeneratorBase<java.lang.Integer>
implements IntChoiceGenerator

Choice Generator that enumerates an interval of int values. Pretty simplistic implementation for now, but at least it can count up and down randomizing is handled through RandomOrderIntCG

Field Summary

Fields

Modifier and Type	Field and Description
protected int	delta
protected int	max
protected int	min
protected int	next

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
IntIntervalGenerator(Config conf, java.lang.String id)
IntIntervalGenerator(int min, int max) Deprecated.
IntIntervalGenerator(int min, int max, int delta) Deprecated.
IntIntervalGenerator(java.lang.String id, int min, int max)
IntIntervalGenerator(java.lang.String id, int min, int max, int delta)

Method Summary

Modifier and Type	Method and Description
void	advance() advance to the next choice.
java.lang.Integer	getChoice(int idx) explicit choice enumeration.
java.lang.Integer[]	getChoices()
java.lang.Class<java.lang.Integer>	getChoiceType()
java.lang.Integer	getNextChoice()
int	getProcessedNumberOfChoices()
int	getTotalNumberOfChoices()
boolean	hasMoreChoices()
boolean	isAscending()
ChoiceGenerator<java.lang.Integer>	randomize() turn the order of choices random (if it isn't already).
ChoiceGenerator<java.lang.Integer>	reorder(java.util.Comparator<java.lang.Integer> comparator) reorder according to a user provided comparator
void	reset() this has to reset the CG to its initial state, which includes resetting 'isDone'
void	reverse() note this should only be called before the CG is advanced since it resets the enumeration state
boolean	supportsReordering()
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, replaceAttr, select, setAttr, setCascaded, setContext, setCurrent, setDone, setId, setIdRef, setInsn, setPreviousChoiceGenerator, setStateId, setThreadInfo, useRandomization

Methods inherited from class java.lang.Object

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

Methods inherited from interface gov.nasa.jpf.vm.ChoiceGenerator

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, isCascaded, isDone, isProcessed, isSchedulingPoint, removeAttr, replaceAttr, select, setAttr, setCascaded, setContext, setCurrent, setDone, setId, setIdRef, setInsn, setPreviousChoiceGenerator, setStateId, setThreadInfo

Field Detail

min

protected int min

max

protected int max

next

protected int next

delta

protected int delta

Constructor Detail

IntIntervalGenerator

@Deprecated
public IntIntervalGenerator(int min,
                                        int max)

Deprecated.

don't use this since it is not safe for cascaded ChoiceGenerators (we need the 'id' to be as context specific as possible)

IntIntervalGenerator

@Deprecated
public IntIntervalGenerator(int min,
                                        int max,
                                        int delta)

Deprecated.

IntIntervalGenerator

public IntIntervalGenerator(java.lang.String id,
                            int min,
                            int max,
                            int delta)

IntIntervalGenerator

public IntIntervalGenerator(java.lang.String id,
                            int min,
                            int max)

IntIntervalGenerator

public IntIntervalGenerator(Config conf,
                            java.lang.String id)

Method Detail

reset

public void reset()

Description copied from interface: ChoiceGenerator

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

Specified by:

reset in interface ChoiceGenerator<java.lang.Integer>

getChoice

public java.lang.Integer getChoice(int idx)

Description copied from class: ChoiceGeneratorBase

explicit choice enumeration. Override if supported

Specified by:

getChoice in interface ChoiceGenerator<java.lang.Integer>

Overrides:

getChoice in class ChoiceGeneratorBase<java.lang.Integer>

Returns:

choice value or null if not supported

getNextChoice

public java.lang.Integer getNextChoice()

Specified by:

getNextChoice in interface ChoiceGenerator<java.lang.Integer>

hasMoreChoices

public boolean hasMoreChoices()

Specified by:

hasMoreChoices in interface ChoiceGenerator<java.lang.Integer>

advance

public void advance()

Description copied from interface: ChoiceGenerator

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

Specified by:

advance in interface ChoiceGenerator<java.lang.Integer>

getTotalNumberOfChoices

public int getTotalNumberOfChoices()

Specified by:

getTotalNumberOfChoices in interface ChoiceGenerator<java.lang.Integer>

getProcessedNumberOfChoices

public int getProcessedNumberOfChoices()

Specified by:

getProcessedNumberOfChoices in interface ChoiceGenerator<java.lang.Integer>

isAscending

public boolean isAscending()

reverse

public void reverse()

note this should only be called before the CG is advanced since it resets the enumeration state

getChoices

public java.lang.Integer[] getChoices()

supportsReordering

public boolean supportsReordering()

Specified by:

supportsReordering in interface ChoiceGenerator<java.lang.Integer>

Overrides:

supportsReordering in class ChoiceGeneratorBase<java.lang.Integer>

reorder

public ChoiceGenerator<java.lang.Integer> reorder(java.util.Comparator<java.lang.Integer> comparator)

Description copied from class: ChoiceGeneratorBase

reorder according to a user provided comparator

Specified by:

reorder in interface ChoiceGenerator<java.lang.Integer>

Overrides:

reorder in class ChoiceGeneratorBase<java.lang.Integer>

toString

public java.lang.String toString()

Overrides:

toString in class ChoiceGeneratorBase<java.lang.Integer>

getChoiceType

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

Specified by:

getChoiceType in interface ChoiceGenerator<java.lang.Integer>

randomize

public ChoiceGenerator<java.lang.Integer> 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<java.lang.Integer>

Overrides:

randomize in class ChoiceGeneratorBase<java.lang.Integer>