Attachment 24525 Details for Bug 103304 – the test case

the test case

testcase.java (text/plain), 7.88 KB, created by Eric Bodden

on 2005-07-11 07:24:20 EDT

(hide)

Description:

Filename:

MIME Type:

Creator: Eric Bodden

Created: 2005-07-11 07:24:20 EDT

Size: 7.88 KB

patch

obsolete

>package rwth.i2.ltlrv.afastate.interfaze;
>
>import java.util.Set;
>
>import rwth.i2.ltlrv.data.PropositionSet;
>import rwth.i2.ltlrv.data.WeakValuesMap;
>import rwth.i2.ltlrv.formula.interfaze.IFormula;
>
>/**
> * 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 {@link rwth.i2.ltlrv.formula.interfaze.IFormula#negationNormalForm()}. 
> * Attention: A lot of algorithms here assume that the whole term structure remains in negation normal form.
> * So be careful when generating {@link rwth.i2.ltlrv.afastate.interfaze.INot} terms somewhere: Always invoke
> * {@link rwth.i2.ltlrv.formula.interfaze.IFormula#negationNormalForm()} on the newly created term!
> * (@see rwth.i2.ltlrv.formula.impl.Implies#negationNormalForm())
> *
> * @author Eric Bodden
> * @see IUntil
> * @see IRelease
> * @see IAnd
> * @see IOr
> * @see INext
> * @see ITT
> * @see IFF
> * @see IProposition
> */
>public interface IAFAState extends IFormula {
>
> /**
> * ValidationException - Exception that is thrown on validation of a formula.
> * 
> * @author Eric Bodden
> */
> @SuppressWarnings("serial")
> public class ValidationException extends Exception {
>
> 
> /**
> * @param variableName name of potentially unbound variable
> * @param subformula subformulae in where <code>variableName</code>
> * is potentially unbound
> */
> public ValidationException(String variableName, IAFAState subformula) {
> super("Variable '"+variableName+"' may be unbound in '"+subformula+"'");
> }
> 
> }
>
>	/**
> * Returns <code>true</code> 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 <code>true</code>.
> * @return <code>true</code> if this formula represents a final
> * state in the AFA
> * @see IRelease
> * @see ITT
> */
> public boolean isFinalStateInAFA();
>
> /**
> * Returns a fresh copy of this subformula with bindings in propositions specialized
> * by the bindings of propositions, which are passed in as argument. 
> * @param bindings Set of propositions holding actual bindings.
> * @return subformula with free bindings replaced by the bindings passed in
> */
> public IAFAState specializeBindings(WeakValuesMap<String, Object> bindings);
> 
> /**
> * Specializes the bindings of all items in <code>clauseSet</code> except the ones that are
> * equal to <code>this</code> term. 
> * @param bindings set of propositions holding actual bindings
> * @param clauseSet the set of clauses containing terms whose bindings shall be specialized;
> * the operation performs a destructive update, so the result will be passed here as well
> * @see #specializeBindings(WeakValuesMap)
> */
> public void specializeBindings(WeakValuesMap<String, Object> bindings, Set<Set<IAFAState>> clauseSet);
> 
>	/**
> * Performs a transition on this term under the given propositions and bindings.
> * The result is returned in the <code>result</code> 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 subset reduction (@see rwth.i2.ltlrv.management.Configuration#subSetReduction(Set)).
> * A typicall initial call would be: 
> * <code><pre>
> Set<Set<IAFAState>> result = new HashSet<Set<IAFAState>>();
> transition(new HastSet<String>(), props, binding, result);
> </pre></code>
>	 * @param 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
> * {@link #provides(Set)} returns. It is only used by the {@link INext} operator
> * (@see Next#doTransition(Set, PropositionSet, WeakValuesMap, Set)). 
>	 * @param currentProps The set of propositions that are currently active.
> * Those must hold all bindings they provide.
>	 * @param currentBinding The current binding to evaluate under. (@see PropositionSet#validCombinationsOfBindings())
>	 * @param result The result will be placed here.
>	 */
>	public void transition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String, Object> currentBinding, Set<Set<IAFAState>> result);
> 
> //TODO STILL USED?
> public enum VariableKind { ALL, IF_CLOSURES_ONLY };
> //TODO STILL USED?
> public void unboundVariablesAtCurrentJoinpoint(VariableKind variableKind, Set<String> result);
> 
> /**
> * This returns the set of provided variables at the current temporal levels.
> * At each state s it holds, that provides(s) = providesPos(s) join providesNeg(s).
> * @param result The result will be placed here.
> * @see #providesPos(Set)
> * @see #providesNeg(Set)
> */
> public void provides(Set<String> result);
>
> /**
> * This returns the set of positively provided variables at the current temporal levels.
> * This function is defined as:
> <pre>
> 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
> </pre>
> * @param result The result will be placed here.
> */
> public void providesPos(Set<String> result);
> 
> /**
> * This returns the set of negatively provided variables at the current temporal levels.
> * This function is defined as:
> <pre>
> 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
> </pre>
> * @param result The result will be placed here.
> */
> public void providesNeg(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.
> * @param result The result will be placed here.
> */
> public void requires(Set<String> result); 
> //TODO refactor: visitors
>
> /**
> * Validates a formula for consistent bindings. Bindings are consistent, when at each point in time,
> * the set of povided variables can be guaranteed to be a superset of the set of required variables.
> * @throws ValidationException Thrown if a variable is unbound. 
> * @see #provides(Set)
> * @see #requires(Set)
> * @see ValidationException#IAFAState.ValidationException(String, IAFAState)
> */
> public void validate() throws ValidationException;
> 
>}

Actions: View

Attachments on bug 103304: 24525