gov.nasa.jpf.vm.choice

Class BreakGenerator

java.lang.Object

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

gov.nasa.jpf.vm.choice.BreakGenerator

All Implemented Interfaces:

ChoiceGenerator<ThreadInfo>, ThreadChoiceGenerator, Cloneable

public class BreakGenerator
extends ChoiceGeneratorBase<ThreadInfo>
implements ThreadChoiceGenerator

a pseudo CG that is used to break transitions. It can be used to break and just reschedule the current thread, or to indicate an end state (e.g. for System.exit())

Field Summary

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

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

Constructor Summary

Constructors

Constructor and Description
BreakGenerator(String id, ThreadInfo ti, boolean isTerminator)

Method Summary

Methods

Modifier and Type	Method and Description
void	advance() advance to the next choice.
boolean	contains(ThreadInfo ti)
Class<ThreadInfo>	getChoiceType()
ThreadInfo	getNextChoice()
int	getProcessedNumberOfChoices()
int	getTotalNumberOfChoices()
boolean	hasMoreChoices()
boolean	isSchedulingPoint()
void	printOn(PrintWriter pw)
ChoiceGenerator<ThreadInfo>	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'

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, getPreviousChoiceGenerator, getPreviousChoiceGeneratorOfType, getSourceLocation, getThreadInfo, hasAttr, hasAttr, hasAttrValue, init, isCascaded, isDone, isProcessed, removeAttr, reorder, replaceAttr, select, setAttr, setCascaded, setContext, setDone, setId, setIdRef, setInsn, setPreviousChoiceGenerator, setThreadInfo, supportsReordering, 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, getAllOfType, getAttr, getAttr, getCascade, getCascadedParent, getId, getIdRef, getInsn, getNextAttr, getPreviousChoiceGenerator, getPreviousChoiceGeneratorOfType, getSourceLocation, getThreadInfo, hasAttr, hasAttr, isCascaded, isDone, isProcessed, removeAttr, reorder, replaceAttr, select, setAttr, setCascaded, setContext, setDone, setId, setIdRef, setInsn, setPreviousChoiceGenerator, setThreadInfo, supportsReordering

Constructor Detail

BreakGenerator

public BreakGenerator(String id,
              ThreadInfo ti,
              boolean isTerminator)

Method Detail

getNextChoice

public ThreadInfo getNextChoice()

Specified by:

getNextChoice in interface ChoiceGenerator<ThreadInfo>

printOn

public void printOn(PrintWriter pw)

Specified by:

printOn in interface ThreadChoiceGenerator

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

getProcessedNumberOfChoices

public int getProcessedNumberOfChoices()

Specified by:

getProcessedNumberOfChoices in interface ChoiceGenerator<ThreadInfo>

getTotalNumberOfChoices

public int getTotalNumberOfChoices()

Specified by:

getTotalNumberOfChoices in interface ChoiceGenerator<ThreadInfo>

hasMoreChoices

public boolean hasMoreChoices()

Specified by:

hasMoreChoices in interface ChoiceGenerator<ThreadInfo>

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>

contains

public boolean contains(ThreadInfo ti)

Specified by:

contains in interface ThreadChoiceGenerator

getChoiceType

public Class<ThreadInfo> getChoiceType()

Specified by:

getChoiceType in interface ChoiceGenerator<ThreadInfo>

randomize

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

isSchedulingPoint

public boolean isSchedulingPoint()

Specified by:

isSchedulingPoint in interface ChoiceGenerator<ThreadInfo>

Overrides:

isSchedulingPoint in class ChoiceGeneratorBase<ThreadInfo>