---

Engine Class Reference

List of all members.

Static Public Methods
void	init (String[] args)
void	start ()
void	stop ()
void	threads ()
JPF	getJPF ()
void	init (String[] args)
iSearch	newSearchAlgorithm ()
void	run (iVirtualMachine vm)
Static Public Attributes
iStore	store
rStatus	status
iVirtualMachine	vm
iSearch	search
JPFOptions	options
String	className
Statistics	statistics
boolean	finished = false
boolean	cleanup = false
String[]	arguments
Static Private Methods
void	printStatistics ()
void	printVersion ()
void	setJPF (JPF jpf)
Static Private Attributes
String	VERSION = "JPF 0.1 beta 12 - (C) 2000 RIACS/NASA Ames Research Center"
String[]	classes
JPF	xjpf

---

Detailed Description

Main engine of the model checker.

Author:

Flavio Lerda , Willem Visser

Version:

1.0

Since:

1.0

Definition at line 20 of file lib/jpf/gov/nasa/arc/ase/jpf/Engine.java.

---

Member Function Documentation

JPF Engine::getJPF (    )  [inline, static]

Accesses the thread local copy of a JPF object. Returns: the local JPF object Definition at line 310 of file src/gov/nasa/arc/ase/jpf/Engine.java.

void Engine::init (  String   args[] )  [inline, static]

Initialize the model checker. Prints the version information. Parses the program arguments in the options field. Check for correctness of the arguments. Handles the -help and -version switches. Prints the current options if necessary. Parameters: args   arguments the program has been called with Definition at line 337 of file src/gov/nasa/arc/ase/jpf/Engine.java.

iSearch Engine::newSearchAlgorithm (    )  [inline, static]

Creates a new iSearch object based on the current options Returns: an iSearch that is going to be used to do the search Definition at line 357 of file src/gov/nasa/arc/ase/jpf/Engine.java. Referenced by run().

void Engine::printStatistics (    )  [inline, static, private]

Prints the statistics accumulated during model checking. Definition at line 381 of file src/gov/nasa/arc/ase/jpf/Engine.java. Referenced by run().

void Engine::printVersion (    )  [inline, static, private]

Prints the version information about the model checker. Definition at line 447 of file src/gov/nasa/arc/ase/jpf/Engine.java. Referenced by init().

void Engine::run (  iVirtualMachine   vm )  [inline, static]

Runs the model checking. First initializes the virtual machine with the arguments received from the command line, initializes the internal structures and then starts the search algorithm. Parameters: vm   a iVirtualMachine implementation Definition at line 464 of file src/gov/nasa/arc/ase/jpf/Engine.java.

void Engine::setJPF (  JPF   jpf )  [inline, static, private]

Sets the local JPF object into the thread local object. Parameters: jpf   a JPF object Definition at line 496 of file src/gov/nasa/arc/ase/jpf/Engine.java. Referenced by run().

---

Member Data Documentation

String Engine::VERSION = "JPF 0.1 beta 12 - (C) 2000 RIACS/NASA Ames Research Center" [static, private]

A String containing the version of the model checker engine. This field is used to output the version information. See also: start() Definition at line 42 of file src/gov/nasa/arc/ase/jpf/Engine.java.

String [] Engine::arguments [static]

Arguments given to the model checker. Definition at line 52 of file src/gov/nasa/arc/ase/jpf/Engine.java.

JPFOptions Engine::options [static]

Parsed program arguments. Definition at line 47 of file src/gov/nasa/arc/ase/jpf/Engine.java.

Statistics Engine::statistics [static]

Facility used to maintain statistics about the verification. Definition at line 57 of file src/gov/nasa/arc/ase/jpf/Engine.java.

JPF Engine::xjpf [static, private]

Local object which contains all the thread specific information. Used by the parallel version in order to have this information accessible without passing a reference thorught each method call, and avoiding to have to share it between the threads. Definition at line 66 of file src/gov/nasa/arc/ase/jpf/Engine.java.

---

The documentation for this class was generated from the following files:

• lib/jpf/gov/nasa/arc/ase/jpf/Engine.java
• src/gov/nasa/arc/ase/jpf/Engine.java

---