rwth.i2.ltlrv.management
Class FormulaFactory

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

All Implemented Interfaces:

IFormulaFactory

public class FormulaFactory
extends Object
implements IFormulaFactory

FormulaFactory - Default implemetation of IFormulaFactory. Returns instances from the default implementing classes.

Author:

Eric Bodden

Field Summary

private static IFF	ff The unique instance of IFF
private static ITT	tt The unique instance of ITT

Constructor Summary

FormulaFactory()

Method Summary

IAnd	And(IFormula formula1, IFormula formula2) Generates an conjunct.
IEquivalent	Eq(IFormula formula1, IFormula formula2) Generates an equivalence relation.
IFinally	F(IFormula formula) Generates a Finally formula.
IFF	FF() Returns the negative positive sink state.
IGlobally	G(IFormula formula) Generates a Globally formula.
IImplies	Impl(IFormula formula1, IFormula formula2) Generates an implication.
INot	Not(IFormula formula) Generates a negation.
IOr	Or(IFormula formula1, IFormula formula2) Generates an disjunct.
IProposition	Proposition(String label, String... formals) Returns a proposition with the given parameters.
IProposition	Proposition(String label, String[] formals, IIfClosure[] ifClosures) Returns a proposition with the given parameters.
IProposition	Proposition(String label, WeakValuesMap<String,Object> bindings) Deprecated.
IRelease	Release(IFormula formula1, IFormula formula2) Generates a Release formula.
ITT	TT() Returns the unique positive sink state.
IUntil	Until(IFormula formula1, IFormula formula2) Generates an Until formula.
INext	X(IFormula formula) Generates a Next formula.

Methods inherited from class java.lang.Object

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

Field Detail

tt

private static final ITT tt

The unique instance of ITT

ff

private static final IFF ff

The unique instance of IFF

Constructor Detail

FormulaFactory

public FormulaFactory()

Method Detail

And

public IAnd And(IFormula formula1,
                IFormula formula2)

Generates an conjunct.

Specified by:

And in interface IFormulaFactory

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 /\ formula2

Eq

public IEquivalent Eq(IFormula formula1,
                      IFormula formula2)

Generates an equivalence relation.

Specified by:

Eq in interface IFormulaFactory

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 <-> formula2

F

public IFinally F(IFormula formula)

Generates a Finally formula.

Specified by:

F in interface IFormulaFactory

Parameters:

formula - the subformula

Returns:

F subformula

G

public IGlobally G(IFormula formula)

Generates a Globally formula.

Specified by:

G in interface IFormulaFactory

Parameters:

formula - the subformula

Returns:

G subformula

Impl

public IImplies Impl(IFormula formula1,
                     IFormula formula2)

Generates an implication.

Specified by:

Impl in interface IFormulaFactory

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 -> formula2

X

public INext X(IFormula formula)

Generates a Next formula.

Specified by:

X in interface IFormulaFactory

Parameters:

formula - the subformula

Returns:

X subformula

Not

public INot Not(IFormula formula)

Generates a negation.

Specified by:

Not in interface IFormulaFactory

Parameters:

formula - the subformula

Returns:

! subformula

Or

public IOr Or(IFormula formula1,
              IFormula formula2)

Generates an disjunct.

Specified by:

Or in interface IFormulaFactory

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 \/ formula2

Proposition

public IProposition Proposition(String label,
                                String[] formals,
                                IIfClosure[] ifClosures)

Returns a proposition with the given parameters.

Specified by:

Proposition in interface IFormulaFactory

Parameters:

label - a label; this should be distinct for semantically distinct propositions

formals - the formals which will be bound by this pointcut at runtime

ifClosures - the if-closures which this pointcut has to satisfy (@see IIfClosure)

Returns:

an appropriate proposition with boundFormals initialized to IProposition.UNBOUND

Proposition

public IProposition Proposition(String label,
                                String... formals)

Returns a proposition with the given parameters.

Specified by:

Proposition in interface IFormulaFactory

Parameters:

label - a label; this should be distinct for semantically distinct propositions

formals - the formals which will be bound by this pointcut at runtime

Returns:

an appropriate proposition with boundFormals initialized to IProposition.UNBOUND

Proposition

@Deprecated
public IProposition Proposition(String label,
                                           WeakValuesMap<String,Object> bindings)

Deprecated.

This is only to be used by the test harness!

Specified by:

Proposition in interface IFormulaFactory

Parameters:

label - a label; this should be distinct for semantically distinct propositions

bindings - a map of current bindings

Returns:

an appropriate proposition with the given bindings

Release

public IRelease Release(IFormula formula1,
                        IFormula formula2)

Generates a Release formula.

Specified by:

Release in interface IFormulaFactory

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 R formula2

Until

public IUntil Until(IFormula formula1,
                    IFormula formula2)

Generates an Until formula.

Specified by:

Until in interface IFormulaFactory

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 U formula2

TT

public ITT TT()

Returns the unique positive sink state.

Specified by:

TT in interface IFormulaFactory

Returns:

TT

FF

public IFF FF()

Returns the negative positive sink state.

Specified by:

FF in interface IFormulaFactory

Returns:

TT