|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
public interface IAFAState
This interface reflects any subformula which is valid as input
for AFA generation.
Those are IUntil, IRelease, IAnd, IOr, INot, INext, ITT, IFF and IProposition subformulae.
Such formulae can be obtained by invoking IFormula.negationNormalForm()
.
Attention: A lot of algorithms here assume that the whole term structure remains in negation normal form.
So be careful when generating INot
terms somewhere: Always invoke
IFormula.negationNormalForm()
on the newly created term!
(@see rwth.i2.ltlrv.formula.impl.Implies#negationNormalForm())
IUntil
,
IRelease
,
IAnd
,
IOr
,
INext
,
ITT
,
IFF
,
IProposition
Nested Class Summary | |
---|---|
static class |
IAFAState.ValidationException
ValidationException - Exception that is thrown on validation of a formula. |
static class |
IAFAState.VariableKind
|
Method Summary | |
---|---|
boolean |
isFinalStateInAFA()
Returns true if this formula represents a final
state in the AFA. |
void |
provides(Set<String> result)
This returns the set of provided variables at the current temporal levels. |
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. |
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. |
void |
transition(Set<String> context,
PropositionSet currentProps,
WeakValuesMap<String,Object> currentBinding,
Set<Set<IAFAState>> result)
Performs a transition on this term under the given propositions and bindings. |
void |
unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind,
Set<String> result)
|
void |
validate()
Validates a formula for consistent bindings. |
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula |
---|
negationNormalForm, symbol |
Method Detail |
---|
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
.
true
if this formula represents a final
state in the AFAIRelease
,
ITT
IAFAState specializeBindings(WeakValuesMap<String,Object> bindings)
bindings
- Set of propositions holding actual bindings.
void transition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result)
result
variable and is actually a set of clauses
representing a disjunct of a conjunct of states. This may not yet be the minimal model. It can be
reduced by applying subsumption reduction (@see rwth.i2.ltlrv.management.Configuration#subsumptionReduction(Set)).
A typicall initial call would be:
Set<Set<IAFAState>> result = new HashSet<Set<IAFAState>>();
transition(new HastSet<String>(), props, binding, result);
context
- The context holds the set of variables that are provided by the outer (previous) temporal layers.
Initially this is empty. Then it has to be updated on each layer by adding the variables which
provides(Set)
returns. It is only used by the INext
operator
(@see Next#doTransition(Set, PropositionSet, WeakValuesMap, Set)).currentProps
- The set of propositions that are currently active.
Those must hold all bindings they provide.currentBinding
- The current binding to evaluate under. (@see PropositionSet#validCombinationsOfBindings())result
- The result will be placed here.void unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result)
void provides(Set<String> result)
result
- The result will be placed here.providesPos(Set)
,
providesNeg(Set)
void providesPos(Set<String> result)
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
result
- The result will be placed here.void providesNeg(Set<String> result)
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
result
- The result will be placed here.void requires(Set<String> result)
result
- The result will be placed here.void validate() throws IAFAState.ValidationException
IAFAState.ValidationException
- Thrown if a variable is unbound.provides(Set)
,
requires(Set)
,
IAFAState.ValidationException.IAFAState.ValidationException(String, IAFAState)
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |