rwth.i2.ltlrv.afastate.base
Class UnaryAFAState

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

All Implemented Interfaces:

IAFAState, IUnaryAFAState, IFormula, IUnaryTerm

Direct Known Subclasses:

Next, Not

public abstract class UnaryAFAState
extends AbstractAFAState
implements IUnaryAFAState

UnaryAFAState - Abstract superclass of all unary 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

subformula the subformula

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

factory

Constructor Summary

UnaryAFAState(IFormula subformula)

Method Summary

boolean	equals(Object oth)
IFormula	getSubformula()
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.IUnaryAFAState

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

subformula

protected IFormula subformula

the subformula

Constructor Detail

UnaryAFAState

public UnaryAFAState(IFormula subformula)

Parameters:

subformula - the subformula

Method Detail

getSubformula

public IFormula getSubformula()

Specified by:

getSubformula in interface IUnaryTerm

Returns:

the subformula or proposition

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

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)

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