rwth.i2.ltlrv.afastate.impl
Class Proposition

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.afastate.base.AbstractAFAState
          rwth.i2.ltlrv.afastate.base.NullaryAFAState
              rwth.i2.ltlrv.afastate.impl.Proposition

All Implemented Interfaces:

IAFAState, INullaryAFAState, IProposition, IFormula

public class Proposition
extends NullaryAFAState
implements IProposition

Proposition - Implements a proposition. A proposition may hold a list of bindings, which map formal parameters represented by Strings to actual objects. Two propositions are equal if their label is equal and their bindings are equal as well. This means, that each formal must be bound to the same object, not just to equal objects. References to objects have to be provided by maps emplyoing weak references.

Author:

Eric Bodden

See Also:

WeakReference

Nested Class Summary

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

IAFAState.ValidationException, IAFAState.VariableKind

Field Summary

protected WeakValuesMap<String,Object>	bindings Bindings of formal parameters for this proposition.
protected int	bindingsSize Copy of size of the bindings map.
protected Collection<IIfClosure>	ifClosures List of if-closures that have to be satisfied in order to match.
protected String	label An appropriate label for this proposition.
protected String[]	provides List of provided variables.
protected Set<String>	varsInIfClosure

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

factory

Fields inherited from interface rwth.i2.ltlrv.afastate.interfaze.IProposition

UNBOUND

Constructor Summary

	Proposition(String label, String[] formals, IIfClosure[] ifClosures) Constructs a new proposition with the given label and free bindings for the given formals.
	Proposition(String label, WeakValuesMap<String,Object> bindings) Deprecated.
private	Proposition(String label, WeakValuesMap<String,Object> bindings, String[] provides, Collection<IIfClosure> ifClosures) Constructs a new proposition with the given label and bindings of formals to actual objects.

Method Summary

private boolean	allIfClosuresSatisfied() Returns true if all if closures are currently satisfied.
void	doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
boolean	equals(Object oth) Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
private boolean	fullyBound() Returns true if this proposition is fully bound.
WeakValuesMap<String,Object>	getBindings() Returns a copy of all bindings in this proposition.
int	hashCode()
boolean	isFinalStateInAFA() Returns true if this formula represents a final state in the AFA.
boolean	matches(IProposition specializedProposition) Returns true if this proposition matches the given specializedProposition.
void	providesNeg(Set<String> result) This returns the set of negatively provided variables at the current temporal levels.
void	providesPos(Set<String> result) This returns the set of positively provided variables at the current temporal levels.
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.
IProposition	specializeBindings(WeakValuesMap<String,Object> specializedBindings) Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument.
String	symbol() Returns the symbol for this term constructor.
String	toString()
void	unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result)
void	validate(Set<String> context) To be implemented by actual formulae as described in IAFAState.validate().
private Set<String>	variableNamesInIfClosures() Returns the set of variables that are contained in if-closures (including those that are bound by this pointcut).
private boolean	wasGarbageCollected()

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

getInstance, negationNormalForm

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

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.INullaryAFAState

getInstance

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

provides, transition, validate

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

negationNormalForm

Field Detail

label

protected final String label

An appropriate label for this proposition. This must be different for propositions with different semantics.

bindings

protected WeakValuesMap<String,Object> bindings

Bindings of formal parameters for this proposition. Must provide support for weak keys.

bindingsSize

protected final int bindingsSize

Copy of size of the bindings map. The size of the map can implicitly change when objects are garbage collected. This copy is used in order to detect such a change.

ifClosures

protected final Collection<IIfClosure> ifClosures

List of if-closures that have to be satisfied in order to match.

See Also:

IIfClosure

varsInIfClosure

protected final Set<String> varsInIfClosure

provides

protected final String[] provides

List of provided variables. This has to be stored at creation time, since bindings change over time.

Constructor Detail

Proposition

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

Constructs a new proposition with the given label and free bindings for the given formals.

Parameters:

label - an appropriate label for this proposition

formals - list of formals that may be bound during evaluation

ifClosures - if-closures which are to be evaluated at runtime

See Also:

IIfClosure

Proposition

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

Deprecated.

Constructs a new proposition with the given label and bindings of formals to actual objects.
This is deprecated. Use Proposition(String, String[], IIfClosure[]) in combination with specializeBindings(WeakValuesMap) instead.

Parameters:

label - an appropriate label for this proposition

bindings - a map mapping from formals represented as String to actual objects

Proposition

private Proposition(String label,
                    WeakValuesMap<String,Object> bindings,
                    String[] provides,
                    Collection<IIfClosure> ifClosures)

Constructs a new proposition with the given label and bindings of formals to actual objects. This is used by specializeBindings(WeakValuesMap)

Parameters:

label - an appropriate label for this proposition

bindings - a map mapping from formals represented as String to actual

provides - old provides set. This is needed, cause bindings may have changed.

ifClosures - if-closures which are to be evaluated at runtime

Method Detail

toString

public String toString()

Overrides:

toString in class NullaryAFAState

isFinalStateInAFA

public boolean isFinalStateInAFA()

Returns true if this formula represents a final state in the AFA. This is the case if the formula is either a Release subformula, TT, or a boolean combination of subformulae evaluating to true.

Specified by:

isFinalStateInAFA in interface IAFAState

Returns:

true if this formula represents a final state in the AFA

See Also:

IRelease, ITT

variableNamesInIfClosures

private Set<String> variableNamesInIfClosures()

Returns the set of variables that are contained in if-closures (including those that are bound by this pointcut).

Returns:

the set of variables that are contained in if-closures

matches

public 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.

Specified by:

matches in interface IProposition

Parameters:

specializedProposition - a specialized proposition

Returns:

true if this proposition matches the given specializedProposition

equals

public boolean equals(Object oth)

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

Specified by:

equals in interface IProposition

Overrides:

equals in class Object

See Also:

Object.equals(java.lang.Object)

hashCode

public int hashCode()

Specified by:

hashCode in interface IProposition

Overrides:

hashCode in class NullaryAFAState

See Also:

Object.hashCode()

getBindings

public 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.

Specified by:

getBindings in interface IProposition

Returns:

a copy of all bindings in this proposition

doTransition

public void doTransition(Set<String> context,
                         PropositionSet currentProps,
                         WeakValuesMap<String,Object> currentBinding,
                         Set<Set<IAFAState>> result)

Performs the actual transition based on the current context.

Specified by:

doTransition in class AbstractAFAState

Parameters:

context - @see #transition(Set, PropositionSet, WeakValuesMap, Set)

currentProps - @see #transition(Set, PropositionSet, WeakValuesMap, Set)

currentBinding - @see #transition(Set, PropositionSet, WeakValuesMap, Set)

result - @see #transition(Set, PropositionSet, WeakValuesMap, Set)

See Also:

IAFAState.transition(Set, PropositionSet, WeakValuesMap, Set), AbstractAFAState.transition(Set, PropositionSet, WeakValuesMap, Set), AbstractAFAState.updateContext(Set)

wasGarbageCollected

private boolean wasGarbageCollected()

Returns:

true if a binding was garbage collected

allIfClosuresSatisfied

private boolean allIfClosuresSatisfied()

Returns true if all if closures are currently satisfied. This implies that the proposition is fully bound.

Returns:

true if all if closures are currently satisfied

fullyBound

private boolean fullyBound()

Returns true if this proposition is fully bound.

Returns:

true if for all b in bindings, b!=IProposition.UNBOUND

unboundVariablesAtCurrentJoinpoint

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

Specified by:

unboundVariablesAtCurrentJoinpoint in interface IAFAState

Overrides:

unboundVariablesAtCurrentJoinpoint in class NullaryAFAState

specializeBindings

public IProposition specializeBindings(WeakValuesMap<String,Object> specializedBindings)

Description copied from class: NullaryAFAState

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

Specified by:

specializeBindings in interface IProposition

Overrides:

specializeBindings in class NullaryAFAState

Parameters:

specializedBindings - Set of propositions holding actual bindings.

Returns:

subformula with free bindings replaced by the bindings passed in

See Also:

IAFAState.specializeBindings(WeakValuesMap)

providesPos

public void providesPos(Set<String> result)

Description copied from class: NullaryAFAState

This returns the set of positively provided variables at the current temporal levels. This function is defined as:

        providesPos( phi /\ psi ) = providesPos( phi ) join providesPos( psi )

        providesPos( phi \/ psi ) = providesPos( phi ) intersect providesPos( psi )

        providesPos( phi R psi ) =  providesPos( (psi /\ phi) \/ (psi /\ X(phi R psi)) )
                                 =  providesPos( psi )

        providesPos( phi U psi ) = providesPos( psi \/ (phi /\ X(phi U psi) )
                                 = providesPos( psi ) intersect providesPos( phi ) 

        providesPos( X phi )     = emptyset

        providesPos( !prop )     = emptyset

        providesPos( prop )      = provided variables of prop
     

Specified by:

providesPos in interface IAFAState

Overrides:

providesPos in class NullaryAFAState

Parameters:

result - The result will be placed here.

providesNeg

public void providesNeg(Set<String> result)

Description copied from class: NullaryAFAState

This returns the set of negatively provided variables at the current temporal levels. This function is defined as:

        providesNeg( phi /\ psi ) = providesNeg( phi ) intersect providesNeg( psi )

        providesNeg( phi \/ psi ) = providesNeg( phi ) join providesNeg( psi )

        providesNeg( phi R psi ) =  providesNeg( psi ) intersect providesNeg( phi )

        providesNeg( phi U psi ) =  providesNeg( psi )

        providesNeg( X phi )     = emptyset

        providesNeg( !prop )     = provided variables of prop

        providesNeg( prop )      = emptyset
     

Specified by:

providesNeg in interface IAFAState

Overrides:

providesNeg in class NullaryAFAState

Parameters:

result - The result will be placed here.

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

Overrides:

requires in class NullaryAFAState

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().

Overrides:

validate in class NullaryAFAState

Parameters:

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

Throws:

IAFAState.ValidationException

symbol

public String symbol()

Returns the symbol for this term constructor. Propositions should return their label. All symbols, including those for nullary term constructors should be distinct.

Specified by:

symbol in interface IFormula

Returns:

The symbol for this term constructor.