rwth.i2.ltlrv.management
Class VerificationRuntime

java.lang.Object
  extended by 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.