rwth.i2.ltlrv.afastate.base
Class BinaryAFAState

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.afastate.base.AbstractAFAState
          rwth.i2.ltlrv.afastate.base.BinaryAFAState

All Implemented Interfaces:

IAFAState, IBinaryAFAState, IBinaryTerm, IFormula

Direct Known Subclasses:

CommutativeBinaryAFAState, Release, Until

public abstract class BinaryAFAState
extends AbstractAFAState
implements IBinaryAFAState

BinaryAFAState - Abstract superclass of all binary formulae.

Author:

Eric Bodden

Nested Class Summary

Nested classes/interfaces inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState

IAFAState.ValidationException, IAFAState.VariableKind

Field Summary

protected IFormula	subformula1 the subformulae
protected IFormula	subformula2 the subformulae
protected IAFAState	substate1
protected IAFAState	substate2

Fields inherited from class rwth.i2.ltlrv.formula.base.AbstractFormula

factory

Constructor Summary

BinaryAFAState(IFormula subformula1, IFormula subformula2)

Method Summary

boolean	equals(Object oth)
IFormula	getSubformula1()
IFormula	getSubformula2()
int	hashCode()
IAFAState	negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
void	requires(Set<String> result) This returns the set of required variables.
IAFAState	specializeBindings(WeakValuesMap<String,Object> bindings) Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument.
String	toString()
void	unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result) Default implementation.
void	validate(Set<String> context) To be implemented by actual formulae as described in IAFAState.validate().

Methods inherited from class rwth.i2.ltlrv.afastate.base.AbstractAFAState

doTransition, provides, transition, updateContext, validate

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface rwth.i2.ltlrv.afastate.interfaze.IBinaryAFAState

reconstruct

Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula

symbol

Methods inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState

isFinalStateInAFA, provides, providesNeg, providesPos, transition, validate

Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula

symbol

Field Detail

subformula1

protected IFormula subformula1

the subformulae

subformula2

protected IFormula subformula2

the subformulae

substate1

protected IAFAState substate1

substate2

protected IAFAState substate2

Constructor Detail

BinaryAFAState

public BinaryAFAState(IFormula subformula1,
                      IFormula subformula2)

Parameters:

subformula1 - left subformula

subformula2 - right subformula

Method Detail

getSubformula1

public IFormula getSubformula1()

Specified by:

getSubformula1 in interface IBinaryTerm

Returns:

the left subformula or proposition

getSubformula2

public IFormula getSubformula2()

Specified by:

getSubformula2 in interface IBinaryTerm

Returns:

the right subformula or proposition

equals

public boolean equals(Object oth)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object

unboundVariablesAtCurrentJoinpoint

public void unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind,
                                               Set<String> result)

Default implementation.

Specified by:

unboundVariablesAtCurrentJoinpoint in interface IAFAState

Parameters:

variableKind - TODO

See Also:

IAFAState.unboundVariablesAtCurrentJoinpoint(VariableKind, Set)

requires

public void requires(Set<String> result)

This returns the set of required variables. This is the set of all variables which are free in propositions, meaning they occur in an if-pointcut but are not provided by the same pointcut at the same time.

Specified by:

requires in interface IAFAState

Parameters:

result - The result will be placed here.

validate

public void validate(Set<String> context)
              throws IAFAState.ValidationException

To be implemented by actual formulae as described in IAFAState.validate().

Specified by:

validate in class AbstractAFAState

Parameters:

context - Here the context is passed in from the outer (earlier) temporal layers.

Throws:

IAFAState.ValidationException

negationNormalForm

public IAFAState negationNormalForm()

Produces a formula in negation normal form, where negations occur only in front of propositions. This form also holds only IUntil, IRelease, IAnd, IOr, INot, IProposition subformulae. This must return a copy of the original formula. The major work is done in Not.negationNormalForm().

Specified by:

negationNormalForm in interface IFormula

Returns:

the formula in negation normal form

See Also:

IUntil, IRelease, IAnd, IOr, IProposition

specializeBindings

public IAFAState specializeBindings(WeakValuesMap<String,Object> bindings)

Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument.

Specified by:

specializeBindings in interface IAFAState

Parameters:

bindings - Set of propositions holding actual bindings.

Returns:

subformula with free bindings replaced by the bindings passed in