gov.nasa.jpf.vm.choice

Class ThreadChoiceFromSet

java.lang.Object

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

gov.nasa.jpf.vm.choice.ThreadChoiceFromSet

All Implemented Interfaces:

ChoiceGenerator<ThreadInfo>, ThreadChoiceGenerator, java.lang.Cloneable

Direct Known Subclasses:

ExceptionThreadChoiceFromSet, ExposureCG

public class ThreadChoiceFromSet
extends ChoiceGeneratorBase<ThreadInfo>
implements ThreadChoiceGenerator

Field Summary

Fields

Modifier and Type	Field and Description
protected int	count
protected boolean	isSchedulingPoint
protected ThreadInfo[]	values

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

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

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	ThreadChoiceFromSet(java.lang.String id)
	ThreadChoiceFromSet(java.lang.String id, ThreadInfo[] set, boolean isSchedulingPoint)

Method Summary

Modifier and Type	Method and Description
void	advance() this has to handle timeouts, which we do with temporary thread status changes (i.e.
boolean	contains(ThreadInfo ti)
ThreadInfo[]	getAllThreadChoices()
ThreadInfo	getChoice(int idx) explicit choice enumeration.
ThreadInfo[]	getChoices()
java.lang.Class<ThreadInfo>	getChoiceType()
ThreadInfo	getNextChoice()
java.lang.Object	getNextChoiceObject()
int	getProcessedNumberOfChoices()
int	getTotalNumberOfChoices()
boolean	hasMoreChoices()
boolean	isSchedulingPoint()
void	printOn(java.io.PrintWriter pw)
ThreadChoiceFromSet	randomize() turn the order of choices random (if it isn't already).
ThreadChoiceGenerator	reorder(java.util.Comparator<ThreadInfo> comparator) reorder according to a user provided comparator
void	reset() this has to reset the CG to its initial state, which includes resetting 'isDone'
boolean	supportsReordering()

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

Field Detail

isSchedulingPoint

protected boolean isSchedulingPoint

values

protected ThreadInfo[] values

count

protected int count

Constructor Detail

ThreadChoiceFromSet

protected ThreadChoiceFromSet(java.lang.String id)

ThreadChoiceFromSet

public ThreadChoiceFromSet(java.lang.String id,
                           ThreadInfo[] set,
                           boolean isSchedulingPoint)

Method Detail

getChoice

public ThreadInfo getChoice(int idx)

Description copied from class: ChoiceGeneratorBase

explicit choice enumeration. Override if supported

Specified by:

getChoice in interface ChoiceGenerator<ThreadInfo>

Overrides:

getChoice in class ChoiceGeneratorBase<ThreadInfo>

Returns:

choice value or null if not supported

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<ThreadInfo>

getNextChoice

public ThreadInfo getNextChoice()

Specified by:

getNextChoice in interface ChoiceGenerator<ThreadInfo>

hasMoreChoices

public boolean hasMoreChoices()

Specified by:

hasMoreChoices in interface ChoiceGenerator<ThreadInfo>

advance

public void advance()

this has to handle timeouts, which we do with temporary thread status changes (i.e. the TIMEOUT_WAITING threads are in our list of choices, but only change their status to TIMEDOUT when they are picked as the next choice) <2do> this should be in SystemState.nextSuccessor - there might be other ThreadChoiceGenerators, and we should handle this consistently

Specified by:

advance in interface ChoiceGenerator<ThreadInfo>

getTotalNumberOfChoices

public int getTotalNumberOfChoices()

Specified by:

getTotalNumberOfChoices in interface ChoiceGenerator<ThreadInfo>

getProcessedNumberOfChoices

public int getProcessedNumberOfChoices()

Specified by:

getProcessedNumberOfChoices in interface ChoiceGenerator<ThreadInfo>

getNextChoiceObject

public java.lang.Object getNextChoiceObject()

getChoices

public ThreadInfo[] getChoices()

supportsReordering

public boolean supportsReordering()

Specified by:

supportsReordering in interface ChoiceGenerator<ThreadInfo>

Overrides:

supportsReordering in class ChoiceGeneratorBase<ThreadInfo>

reorder

public ThreadChoiceGenerator reorder(java.util.Comparator<ThreadInfo> comparator)

Description copied from class: ChoiceGeneratorBase

reorder according to a user provided comparator

Specified by:

reorder in interface ChoiceGenerator<ThreadInfo>

Overrides:

reorder in class ChoiceGeneratorBase<ThreadInfo>

printOn

public void printOn(java.io.PrintWriter pw)

Specified by:

printOn in interface ThreadChoiceGenerator

randomize

public ThreadChoiceFromSet 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<ThreadInfo>

Overrides:

randomize in class ChoiceGeneratorBase<ThreadInfo>

getAllThreadChoices

public ThreadInfo[] getAllThreadChoices()

contains

public boolean contains(ThreadInfo ti)

Specified by:

contains in interface ThreadChoiceGenerator

getChoiceType

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

Specified by:

getChoiceType in interface ChoiceGenerator<ThreadInfo>

isSchedulingPoint

public boolean isSchedulingPoint()

Specified by:

isSchedulingPoint in interface ChoiceGenerator<ThreadInfo>

Overrides:

isSchedulingPoint in class ChoiceGeneratorBase<ThreadInfo>