|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectrwth.i2.ltlrv.formula.base.AbstractFormula
rwth.i2.ltlrv.afastate.base.AbstractAFAState
rwth.i2.ltlrv.afastate.base.NullaryAFAState
rwth.i2.ltlrv.afastate.impl.Proposition
public class Proposition
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.
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 |
---|
protected final String label
protected WeakValuesMap<String,Object> bindings
protected final int bindingsSize
protected final Collection<IIfClosure> ifClosures
IIfClosure
protected final Set<String> varsInIfClosure
protected final String[] provides
Constructor Detail |
---|
public Proposition(String label, String[] formals, IIfClosure[] ifClosures)
label
- an appropriate label for this propositionformals
- list of formals that may be bound during evaluationifClosures
- if-closures which are to be evaluated at runtimeIIfClosure
@Deprecated public Proposition(String label, WeakValuesMap<String,Object> bindings)
Proposition(String, String[], IIfClosure[])
in combination
with specializeBindings(WeakValuesMap)
instead.
label
- an appropriate label for this propositionbindings
- a map mapping from formals represented as String to actual
objectsprivate Proposition(String label, WeakValuesMap<String,Object> bindings, String[] provides, Collection<IIfClosure> ifClosures)
specializeBindings(WeakValuesMap)
label
- an appropriate label for this propositionbindings
- a map mapping from formals represented as String to actualprovides
- old provides set. This is needed, cause bindings may have changed.ifClosures
- if-closures which are to be evaluated at runtimeMethod Detail |
---|
public String toString()
toString
in class NullaryAFAState
public boolean isFinalStateInAFA()
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
.
isFinalStateInAFA
in interface IAFAState
true
if this formula represents a final
state in the AFAIRelease
,
ITT
private Set<String> variableNamesInIfClosures()
public boolean matches(IProposition specializedProposition)
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.
matches
in interface IProposition
specializedProposition
- a specialized proposition
true
if this proposition matches the
given specializedPropositionpublic boolean equals(Object oth)
equals
in interface IProposition
equals
in class Object
Object.equals(java.lang.Object)
public int hashCode()
hashCode
in interface IProposition
hashCode
in class NullaryAFAState
Object.hashCode()
public WeakValuesMap<String,Object> getBindings()
getBindings
in interface IProposition
public void doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result)
doTransition
in class AbstractAFAState
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)IAFAState.transition(Set, PropositionSet, WeakValuesMap, Set)
,
AbstractAFAState.transition(Set, PropositionSet, WeakValuesMap, Set)
,
AbstractAFAState.updateContext(Set)
private boolean wasGarbageCollected()
private boolean allIfClosuresSatisfied()
true
if all if closures are currently satisfied.
This implies that the proposition is fully bound.
true
if all if closures are currently satisfiedprivate boolean fullyBound()
true
if this proposition is fully bound.
true
if for all b in bindings
,
b!=IProposition.UNBOUND
public void unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result)
unboundVariablesAtCurrentJoinpoint
in interface IAFAState
unboundVariablesAtCurrentJoinpoint
in class NullaryAFAState
public IProposition specializeBindings(WeakValuesMap<String,Object> specializedBindings)
NullaryAFAState
specializeBindings
in interface IAFAState
specializeBindings
in interface IProposition
specializeBindings
in class NullaryAFAState
specializedBindings
- Set of propositions holding actual bindings.
IAFAState.specializeBindings(WeakValuesMap)
public void providesPos(Set<String> result)
NullaryAFAState
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
providesPos
in interface IAFAState
providesPos
in class NullaryAFAState
result
- The result will be placed here.public void providesNeg(Set<String> result)
NullaryAFAState
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
providesNeg
in interface IAFAState
providesNeg
in class NullaryAFAState
result
- The result will be placed here.public void requires(Set<String> result)
requires
in interface IAFAState
requires
in class NullaryAFAState
result
- The result will be placed here.public void validate(Set<String> context) throws IAFAState.ValidationException
IAFAState.validate()
.
validate
in class NullaryAFAState
context
- Here the context is passed in from the outer (earlier) temporal layers.
IAFAState.ValidationException
public String symbol()
symbol
in interface IFormula
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |