gov.nasa.jpf

Class JPF

java.lang.Object

gov.nasa.jpf.JPF

All Implemented Interfaces:

java.lang.Runnable

public class JPF
extends java.lang.Object
implements java.lang.Runnable

main class of the JPF verification framework. This reads the configuration, instantiates the Search and VM objects, and kicks off the Search

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	JPF.ExitException private helper class for local termination of JPF (without killing the whole Java process via System.exit).
static class	JPF.Status

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	VERSION

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	JPF()
	JPF(Config conf) create new JPF object.
	JPF(java.lang.String... args) convenience method if caller doesn't care about Config

Method Summary

Modifier and Type	Method and Description
void	addListener(JPFListener l)
protected void	addPendingSearchListener(SearchListener l)
protected void	addPendingVMListener(VMListener l)
void	addPropertyListener(PropertyListenerAdapter pl)
<T extends Publisher> boolean	addPublisherExtension(java.lang.Class<T> pCls, PublisherExtension e)
void	addSearchListener(SearchListener l)
void	addSearchProperty(Property p)
boolean	addUniqueTypeListener(JPFListener l)
void	addVMListener(VMListener l)
protected void	cleanUp()
static Config	createConfig(java.lang.String[] args) return a Config object that holds the JPF options.
static void	exit()
boolean	foundErrors()
Config	getConfig()
Error	getLastError()
<T> T	getListenerOfType(java.lang.Class<T> type)
static JPFLogger	getLogger(java.lang.String name) use this one to get a Logger that is initialized via our Config mechanism.
Reporter	getReporter()
Search	getSearch() return the search object.
java.util.List<Error>	getSearchErrors()
JPF.Status	getStatus()
VM	getVM() return the VM object.
static void	handleException(JPFException e)
boolean	isRunnable()
static void	main(java.lang.String[] args)
static void	printBanner(Config config)
void	removeListener(JPFListener l)
void	run() runs the verification.
<T extends Publisher> void	setPublisherItems(java.lang.Class<T> pCls, int category, java.lang.String[] topics)
static void	start(Config conf, java.lang.String[] args)

Methods inherited from class java.lang.Object

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

Field Detail

VERSION

public static java.lang.String VERSION

Constructor Detail

JPF

protected JPF()

JPF

public JPF(Config conf)

create new JPF object. Note this is always guaranteed to return, but the Search and/or VM object instantiation might have failed (i.e. the JPF object might not be really usable). If you directly use getSearch() / getVM(), check for null

JPF

public JPF(java.lang.String... args)

convenience method if caller doesn't care about Config

Method Detail

getLogger

public static JPFLogger getLogger(java.lang.String name)

use this one to get a Logger that is initialized via our Config mechanism. Note that our own Loggers do NOT pass

main

public static void main(java.lang.String[] args)

start

public static void start(Config conf,
                         java.lang.String[] args)

getStatus

public JPF.Status getStatus()

isRunnable

public boolean isRunnable()

addPropertyListener

public void addPropertyListener(PropertyListenerAdapter pl)

addSearchListener

public void addSearchListener(SearchListener l)

addPendingVMListener

protected void addPendingVMListener(VMListener l)

addPendingSearchListener

protected void addPendingSearchListener(SearchListener l)

addListener

public void addListener(JPFListener l)

getListenerOfType

public <T> T getListenerOfType(java.lang.Class<T> type)

addUniqueTypeListener

public boolean addUniqueTypeListener(JPFListener l)

removeListener

public void removeListener(JPFListener l)

addVMListener

public void addVMListener(VMListener l)

addSearchProperty

public void addSearchProperty(Property p)

getReporter

public Reporter getReporter()

addPublisherExtension

public <T extends Publisher> boolean addPublisherExtension(java.lang.Class<T> pCls,
                                                           PublisherExtension e)

setPublisherItems

public <T extends Publisher> void setPublisherItems(java.lang.Class<T> pCls,
                                                    int category,
                                                    java.lang.String[] topics)

getConfig

public Config getConfig()

getSearch

public Search getSearch()

return the search object. This can be null if the initialization has failed

getVM

public VM getVM()

return the VM object. This can be null if the initialization has failed

exit

public static void exit()

foundErrors

public boolean foundErrors()

printBanner

public static void printBanner(Config config)

createConfig

public static Config createConfig(java.lang.String[] args)

return a Config object that holds the JPF options. This first loads the properties from a (potentially configured) properties file, and then overlays all command line arguments that are key/value pairs

run

public void run()

runs the verification.

Specified by:

run in interface java.lang.Runnable

cleanUp

protected void cleanUp()

getSearchErrors

public java.util.List<Error> getSearchErrors()

getLastError

public Error getLastError()

handleException

public static void handleException(JPFException e)