gov.nasa.jpf.util.script

Class ScriptEnvironment<CG extends ChoiceGenerator<?>>

java.lang.Object

gov.nasa.jpf.util.script.ScriptEnvironment<CG>

All Implemented Interfaces:

StateExtensionClient<gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot>

public abstract class ScriptEnvironment<CG extends ChoiceGenerator<?>>
extends Object
implements StateExtensionClient<gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot>

class representing a statemachine environment that produces SCEventGenerators from scripts

Constructor Summary

Constructors

Constructor and Description
ScriptEnvironment(String fname)
ScriptEnvironment(String name, Reader r)

Method Summary

Methods

Modifier and Type	Method and Description
protected abstract CG	createCGFromEvents(String id, List<Event> events)
CG	getNext(String id)
CG	getNext(String id, String[] activeStates)
CG	getNext(String id, String[] activeStates, BitSet isReEntered)
gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot	getStateExtension()
void	parseScript()
void	registerListener(JPF jpf)
void	restore(gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot stateExtension)

Methods inherited from class java.lang.Object

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

Constructor Detail

ScriptEnvironment

public ScriptEnvironment(String fname)
                  throws FileNotFoundException

Throws:

FileNotFoundException

ScriptEnvironment

public ScriptEnvironment(String name,
                 Reader r)

Method Detail

parseScript

public void parseScript()
                 throws ESParser.Exception

Throws:

ESParser.Exception

getNext

public CG getNext(String id)

getNext

public CG getNext(String id,
         String[] activeStates)

getNext

public CG getNext(String id,
         String[] activeStates,
         BitSet isReEntered)

createCGFromEvents

protected abstract CG createCGFromEvents(String id,
                    List<Event> events)

getStateExtension

public gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot getStateExtension()

Specified by:

getStateExtension in interface StateExtensionClient<gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot>

restore

public void restore(gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot stateExtension)

Specified by:

restore in interface StateExtensionClient<gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot>

registerListener

public void registerListener(JPF jpf)

Specified by:

registerListener in interface StateExtensionClient<gov.nasa.jpf.util.script.ScriptEnvironment.ActiveSnapshot>