ConForM.CoopnTools.CoKer.CoopnSem
Class CoopnSem

java.lang.Object
  |
  +--ConForM.CoopnTools.CoKer.CoopnSem.CoopnSem

public class CoopnSem
extends java.lang.Object

Coopn semantics evaluator. This class essentially defines the various requests dealing with the semantics of CO-OPN. Objects of this class are able to handle one request at a time and deliver their set of results as an Iterator on individual results. Accordingly, Each method call, each new request (eval methods, next methods, formal or short form methods) invalidates all previous returned iterators.


Field Summary
static int DEFAULTBOUND
          Default Evaluation bound.
static int SLDMODE
          SLD Evaluation mode.
static java.lang.String VERSION
          Coopn semantics version.
 
Constructor Summary
CoopnSem(CoopnWorkspace spec, CoopnEnv env)
          Constructor for a semantics of a workspace (therefore for a specification).
 
Method Summary
 void dispose()
          Leave a coopn semantics; dispose all its resources.
 CoopnSubstitutionIterator eval(CoopnAdtFormulaSymbol formula, AnonymousNameBridge bridge)
          Evaluation of an ADT formula.
 CoopnSubstitutionIterator eval(CoopnAdtFormulaSymbol formula, CoopnSubstitution init, AnonymousNameBridge bridge)
          Evaluation of an ADT formula.
 java.lang.String[] getEvaluationModes()
          Get the various evaluation mode.
 StateIterator initial(State state, AnonymousNameBridge bridge)
          Evaluation of the initial state of a specification.
 StateIterator initial(State state, CoopnSubstitution init, AnonymousNameBridge bridge)
          Evaluation of the initial state of a specification.
 void interrupt()
          Iterator interruption.
 void setEvaluationBound(int bound)
          Set the evaluation bound.
 void setEvaluationMode(int mode)
          Set the evaluation mode.
 void setNormalForm()
          Set normal form mode.
 void setShortForm()
          Set short form mode.
 CoopnWorkspace spec()
          Return the associated specification.
 StepIterator step(Transition transition, AnonymousNameBridge bridge)
          Evaluates the next step in the semantics of a specification.
 StepIterator step(Transition transition, CoopnSubstitution init, AnonymousNameBridge bridge)
          Evaluates the next step in the semantics of a specification.
 void use()
          Uses an aspect manager.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

VERSION

public static final java.lang.String VERSION
Coopn semantics version.

SLDMODE

public static int SLDMODE
SLD Evaluation mode.

DEFAULTBOUND

public static int DEFAULTBOUND
Default Evaluation bound.
Constructor Detail

CoopnSem

public CoopnSem(CoopnWorkspace spec,
                CoopnEnv env)
Constructor for a semantics of a workspace (therefore for a specification).
Parameters:
spec - the workspace
Throws:
java.lang.IllegalArgumentException - the semnatics cannot be created, because of erroneous arguments or because the underlying logic engine cannot be created.
Method Detail

use

public void use()
Uses an aspect manager.

dispose

public void dispose()
Leave a coopn semantics; dispose all its resources.

spec

public CoopnWorkspace spec()
Return the associated specification.

setNormalForm

public void setNormalForm()
Set normal form mode.

setShortForm

public void setShortForm()
Set short form mode.

setEvaluationMode

public void setEvaluationMode(int mode)
Set the evaluation mode.

setEvaluationBound

public void setEvaluationBound(int bound)
Set the evaluation bound.

getEvaluationModes

public java.lang.String[] getEvaluationModes()
Get the various evaluation mode. Return an array of strings, the index of which represent the mode as an integer, the String representing a presentation name.

interrupt

public void interrupt()
Iterator interruption. Interrupt - if possible - an evaluation in execution. A pending iteration will return (more or less quickly) with a negative result.

eval

public CoopnSubstitutionIterator eval(CoopnAdtFormulaSymbol formula,
                                      CoopnSubstitution init,
                                      AnonymousNameBridge bridge)
Evaluation of an ADT formula. Get the substitution such that the formula holds. A call to this method invalidates all the iterators returned previously by this object.
Parameters:
formula - the formula to evaluate
init - the initial substitution, or null
bridge - an anonymous name bridge, or null
Returns:
an iterator on substitutions

eval

public CoopnSubstitutionIterator eval(CoopnAdtFormulaSymbol formula,
                                      AnonymousNameBridge bridge)
Evaluation of an ADT formula. Get the substitution such that the formula holds. A call to this method invalidates all the iterators returned previously by this object.
Parameters:
formula - the formula to evaluate
bridge - an anonymous name bridge, or null
Returns:
an iterator on substitutions

initial

public StateIterator initial(State state,
                             CoopnSubstitution init,
                             AnonymousNameBridge bridge)
Evaluation of the initial state of a specification. A call to this method invalidates all the iterators returned previously by this object.
Parameters:
state - the initial to evaluate, cannot be null
init - the initial substitution, or null
bridge - an anonymous name bridge, or null
Returns:
an iterator on states

initial

public StateIterator initial(State state,
                             AnonymousNameBridge bridge)
Evaluation of the initial state of a specification. A call to this method invalidates all the iterators returned previously by this object.
Parameters:
state - the initial to evaluate, cannot be null
bridge - an anonymous name bridge, or null
Returns:
an iterator on states

step

public StepIterator step(Transition transition,
                         CoopnSubstitution init,
                         AnonymousNameBridge bridge)
Evaluates the next step in the semantics of a specification. Get the steps such accoring to the semantics of the specification. A call to this method invalidates all the iterators returned previously by this object.
Parameters:
transition - the transition to evaluate, cannot be null
init - the initial substitution, or null
bridge - an anonymous name bridge, or null
Returns:
an iterator on steps

step

public StepIterator step(Transition transition,
                         AnonymousNameBridge bridge)
Evaluates the next step in the semantics of a specification. Get the steps such accoring to the semantics of the specification. A call to this method invalidates all the iterators returned previously by this object.
Parameters:
transition - the transition to evaluate, cannot be null
bridge - an anonymous name bridge, or null
Returns:
an iterator on steps