rwth.i2.ltlrv.management
Class VerificationRuntime

java.lang.Object
  rwth.i2.ltlrv.management.VerificationRuntime

public class VerificationRuntime
extends Object

VerificationRuntime - Runtime manager holding formula configurations and notifying listeners about the ongoing evaluations.

Author:

Eric Bodden

Nested Class Summary

static interface

VerificationRuntime.Listener Listener - Interface for listers that wish to be notified about evaluation progress.

Field Summary

private Map<String,Configuration>	configurationForFormulaId Mapping from formula ID to the configuration fot this formula.
private static VerificationRuntime.Listener[]	DEFAULT_LISTENERS The default listeners for the case that the environment variable is not set.
private IFormulaFactory	FORMULA_FACTORY
private List<VerificationRuntime.Listener>	listeners All currently registered listeners.
private static String	LTL_RV_LISTENERS Environment variable pointing to listener classes (semicolon separated): LTLRV_LISTENERS=package1.Listener1;package1.Listener2
private Map<String,Configuration>	originalConfigurationForFormulaId Similar to configurationForFormulaId but keeps copies of the initial configurations
private static boolean	REMATCHING If rematching is on, falsified/satisfied formulae are not removed but rather reinstantiated.
private static VerificationRuntime	singletonInstance Singleton instance of this class.

Constructor Summary

private

VerificationRuntime() Default constructor.

Method Summary

IFormulaFactory	getFactory() Returns the term factory.
static VerificationRuntime	getInstance() Returns the singleton instance.
private void	initializeListeners() Installs listeners from the environment variable or installs the default listeners if the variable is not set.
private void	notifyListeners(boolean update, String formulaId, Thread associatedThread, Configuration newConfig) Notifies all listeners about a formula being updated/registered.
protected void	notifyOnUserCausedException(String formulaId, Thread thread, String ifExpression, Throwable exception, Configuration config) Notifies all listeners about a user-caused exception that happened during the evaluation of an if-pointcut.
void	registerFormula(String formulaId, IFormula formula) Registers a new formula.
void	tearDown() Notifies that the system shuts down.
void	updateFormula(String formulaId, PropositionSet currentPropositions) Requests that the formula with the given ID shall be updated.

Methods inherited from class java.lang.Object

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

Field Detail

LTL_RV_LISTENERS

private static final String LTL_RV_LISTENERS

Environment variable pointing to listener classes (semicolon separated): LTLRV_LISTENERS=package1.Listener1;package1.Listener2

See Also:

Constant Field Values

DEFAULT_LISTENERS

private static final VerificationRuntime.Listener[] DEFAULT_LISTENERS

The default listeners for the case that the environment variable is not set.

singletonInstance

private static VerificationRuntime singletonInstance

Singleton instance of this class.

configurationForFormulaId

private Map<String,Configuration> configurationForFormulaId

Mapping from formula ID to the configuration fot this formula.

originalConfigurationForFormulaId

private Map<String,Configuration> originalConfigurationForFormulaId

Similar to configurationForFormulaId but keeps copies of the initial configurations

listeners

private List<VerificationRuntime.Listener> listeners

All currently registered listeners.

REMATCHING

private static final boolean REMATCHING

If rematching is on, falsified/satisfied formulae are not removed but rather reinstantiated.

FORMULA_FACTORY

private final IFormulaFactory FORMULA_FACTORY

Constructor Detail

VerificationRuntime

private VerificationRuntime()

Default constructor. Called by getInstance() only.

See Also:

getInstance()

Method Detail

initializeListeners

private void initializeListeners()

Installs listeners from the environment variable or installs the default listeners if the variable is not set.

registerFormula

public void registerFormula(String formulaId,
                            IFormula formula)

Registers a new formula.

Parameters:

formulaId - Unique ID for this formula.

formula - The new formula to install.

updateFormula

public void updateFormula(String formulaId,
                          PropositionSet currentPropositions)

Requests that the formula with the given ID shall be updated.

Parameters:

formulaId - Unique ID for the formula to be updated.

currentPropositions - the set of propositions under which the transition shall be taken.

tearDown

public void tearDown()

Notifies that the system shuts down.

notifyOnUserCausedException

protected void notifyOnUserCausedException(String formulaId,
                                           Thread thread,
                                           String ifExpression,
                                           Throwable exception,
                                           Configuration config)

Notifies all listeners about a user-caused exception that happened during the evaluation of an if-pointcut.

Parameters:

formulaId - id of the formula which caused this exception

thread - Thread that triggered the evaluation

ifExpression - expression that caused the exception

exception - exception that occured

config - last configuration before this exception occured

notifyListeners

private void notifyListeners(boolean update,
                             String formulaId,
                             Thread associatedThread,
                             Configuration newConfig)

Notifies all listeners about a formula being updated/registered.

Parameters:

update - if true, this calls notifyUpdate, else notifyRegistered

formulaId - Unique ID for the formula to be notified about.

associatedThread - Thread who updated/installed the formula.

newConfig - The new/initial configuration.

See Also:

VerificationRuntime.Listener.notifyUpdate(String, Thread, Configuration), VerificationRuntime.Listener.notifyRegistered(String, Thread, Configuration)

getInstance

public static VerificationRuntime getInstance()

Returns the singleton instance.

Returns:

the singleton instance

getFactory

public IFormulaFactory getFactory()

Returns the term factory.

Returns:

The term factory.