rwth.i2.ltlrv.afastate.interfaze
Interface IProposition

All Superinterfaces:

IAFAState, IFormula, INullaryAFAState

All Known Implementing Classes:

Proposition

public interface IProposition
extends INullaryAFAState

IProposition represents a proposition

Author:

Eric Bodden

Nested Class Summary

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

IAFAState.ValidationException, IAFAState.VariableKind

Field Summary

static Object

UNBOUND Constant meaning "unbound binding".

Method Summary

boolean	equals(Object obj) Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
WeakValuesMap<String,Object>	getBindings() Returns a copy of all bindings in this proposition.
int	hashCode() Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
boolean	matches(IProposition specializedProposition) Returns true if this proposition matches the given specializedProposition.
IProposition	specializeBindings(WeakValuesMap<String,Object> bindings) Specialized return type, for convenience.

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

getInstance

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

isFinalStateInAFA, provides, providesNeg, providesPos, requires, transition, unboundVariablesAtCurrentJoinpoint, validate

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

negationNormalForm, symbol

Field Detail

UNBOUND

static final Object UNBOUND

Constant meaning "unbound binding".

Method Detail

equals

boolean equals(Object obj)

Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.

Overrides:

equals in class Object

See Also:

Object.equals(java.lang.Object)

hashCode

int hashCode()

Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.

Overrides:

hashCode in class Object

See Also:

Object.hashCode()

matches

boolean matches(IProposition specializedProposition)

Returns true if this proposition matches the given specializedProposition. This is the case when the labels are equal and specializedProposition is at least as special as this, meaning it holds the same formals and at least the formals bound in this are bound in specializedProposition.

Parameters:

specializedProposition - a specialized proposition

Returns:

true if this proposition matches the given specializedProposition

getBindings

WeakValuesMap<String,Object> getBindings()

Returns a copy of all bindings in this proposition. This is a weak map: Values which are mapped may be claimed by the garbage collector. In this case, the mapping will disappear.

Returns:

a copy of all bindings in this proposition

specializeBindings

IProposition specializeBindings(WeakValuesMap<String,Object> bindings)

Specialized return type, for convenience.

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

See Also:

IAFAState.specializeBindings(WeakValuesMap)