gov.nasa.jpf.util.script

Class EventGeneratorFactory

java.lang.Object

gov.nasa.jpf.ListenerAdapter

gov.nasa.jpf.util.script.EventGeneratorFactory

All Implemented Interfaces:

JPFListener, PublisherExtension, SearchListener, ElementProcessor, VMListener, java.lang.Iterable<EventGenerator>

public abstract class EventGeneratorFactory
extends ListenerAdapter
implements ElementProcessor, java.lang.Iterable<EventGenerator>

abstract root for backtrackable event generator factories <2do> - we don't support backtracking for sections yet! needs to be implemented for state charts

Field Summary

Fields

Modifier and Type	Field and Description
protected Config	conf
protected int	cur the last returned position in the generator stream
protected java.util.ArrayList<EventGenerator>	queue
protected Script	script
protected java.lang.String	scriptFileName
protected java.util.LinkedHashMap<java.lang.String,java.util.ArrayList<EventGenerator>>	sections

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	EventGeneratorFactory()
protected	EventGeneratorFactory(EventFactory efact)

Method Summary

Modifier and Type	Method and Description
protected void	addLoop(int startPos)
java.util.ArrayList<EventGenerator>	getDefaultSection()
abstract java.lang.Class<?>	getEventType()
protected EventGenerator	getNextEventGenerator()
protected EventGenerator	getQueueItem(int i)
Script	getScript()
java.lang.String	getScriptFileName()
java.util.ArrayList<EventGenerator>	getSection(java.lang.String id)
int	getTotalNumberOfEvents()
boolean	hasSection(java.lang.String id)
protected void	init(java.lang.String fname)
java.util.Iterator<EventGenerator>	iterator()
void	printOn(java.io.PrintWriter pw)
void	reset() reset the enumeration state of this factory
void	searchStarted(Search search) SearchListener interface
protected void	setQueue(java.util.ArrayList<EventGenerator> q)
void	stateAdvanced(Search search) got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set
void	stateBacktracked(Search search) state was backtracked one step
void	stateRestored(Search search) a previously generated state was restored (can be on a completely different path)

Methods inherited from class gov.nasa.jpf.ListenerAdapter

choiceGeneratorAdvanced, choiceGeneratorProcessed, choiceGeneratorRegistered, choiceGeneratorSet, classLoaded, exceptionBailout, exceptionHandled, exceptionThrown, executeInstruction, gcBegin, gcEnd, instructionExecuted, loadClass, methodEntered, methodExited, objectCreated, objectExposed, objectLocked, objectNotify, objectNotifyAll, objectReleased, objectShared, objectUnlocked, objectWait, propertyViolated, publishConstraintHit, publishFinished, publishProbe, publishPropertyViolation, publishStart, publishTransition, searchConstraintHit, searchFinished, searchProbed, stateProcessed, statePurged, stateStored, threadBlocked, threadInterrupted, threadNotified, threadScheduled, threadStarted, threadTerminated, threadWaiting, vmInitialized

Methods inherited from class java.lang.Object

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

Methods inherited from interface gov.nasa.jpf.util.script.ElementProcessor

process, process, process, process

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Field Detail

cur

protected int cur

the last returned position in the generator stream

scriptFileName

protected java.lang.String scriptFileName

script

protected Script script

conf

protected Config conf

sections

protected java.util.LinkedHashMap<java.lang.String,java.util.ArrayList<EventGenerator>> sections

queue

protected java.util.ArrayList<EventGenerator> queue

Constructor Detail

EventGeneratorFactory

protected EventGeneratorFactory()

EventGeneratorFactory

protected EventGeneratorFactory(EventFactory efact)

Method Detail

init

protected void init(java.lang.String fname)
             throws ESParser.Exception

Throws:

ESParser.Exception

iterator

public java.util.Iterator<EventGenerator> iterator()

Specified by:

iterator in interface java.lang.Iterable<EventGenerator>

addLoop

protected void addLoop(int startPos)

getEventType

public abstract java.lang.Class<?> getEventType()

reset

public void reset()

reset the enumeration state of this factory

getScriptFileName

public java.lang.String getScriptFileName()

getScript

public Script getScript()

hasSection

public boolean hasSection(java.lang.String id)

getSection

public java.util.ArrayList<EventGenerator> getSection(java.lang.String id)

getDefaultSection

public java.util.ArrayList<EventGenerator> getDefaultSection()

setQueue

protected void setQueue(java.util.ArrayList<EventGenerator> q)

getNextEventGenerator

protected EventGenerator getNextEventGenerator()

getQueueItem

protected EventGenerator getQueueItem(int i)

getTotalNumberOfEvents

public int getTotalNumberOfEvents()

printOn

public void printOn(java.io.PrintWriter pw)

searchStarted

public void searchStarted(Search search)

SearchListener interface

Specified by:

searchStarted in interface SearchListener

Overrides:

searchStarted in class ListenerAdapter

stateAdvanced

public void stateAdvanced(Search search)

Description copied from interface: SearchListener

got the next state Note - this will be notified before any potential propertyViolated, in which case the currentError will be already set

Specified by:

stateAdvanced in interface SearchListener

Overrides:

stateAdvanced in class ListenerAdapter

stateBacktracked

public void stateBacktracked(Search search)

Description copied from interface: SearchListener

state was backtracked one step

Specified by:

stateBacktracked in interface SearchListener

Overrides:

stateBacktracked in class ListenerAdapter

stateRestored

public void stateRestored(Search search)

Description copied from interface: SearchListener

a previously generated state was restored (can be on a completely different path)

Specified by:

stateRestored in interface SearchListener

Overrides:

stateRestored in class ListenerAdapter