| Interface | Description |
|---|---|
| Action1 |
An abstract unary Circus action definition.
|
| Action2 |
An abstract binary Circus action definition.
|
| ActionD |
An abstract unary Circus action with Z declarations.
|
| ActionIte |
An abstract iterated unary Circus action definition.
|
| ActionList |
An abstract Action list.
|
| ActionPara |
A action paragraph that declares a name for an action definition.
|
| ActionSignature |
An action signature consists of the action name, formal parameters,
the channels used, the communications, channel sets and name sets used.
|
| ActionSignatureAnn |
An action signature wrapped within an annotation, where generic type are resolved.
|
| ActionSignatureList |
An signature list with action signatures.
|
| ActionTransformerPred |
An action transformer predicate is a predicate that relates two actions
by one of the available transformation relations in one of the available
models.
|
| ActionType |
An action type contains the action signature.
|
| AlphabetisedParallelAction |
Alphabetised Parallel composition between two actions;
it includes the channel set expression for both alphabets as synchronisation sets.
|
| AlphabetisedParallelActionIte |
Circus action for alphabetised iterated parallel composition.
|
| AlphabetisedParallelProcess |
Circus alphabetised parallel process; it includes the two alphabets as channel sets.
|
| AlphabetisedParallelProcessIdx |
Circus process for alphabetised indexed and iterated parallel composition.
|
| AlphabetisedParallelProcessIte |
Circus process for alphabetised iterated parallel composition.
|
| AssignmentCommand |
Circus command declaring (possibly) multiple assignment.
|
| AssignmentPairs |
Encapsulates two lists used for assignments.
|
| BasicAction |
An abstract class for basic Circus action.
|
| BasicChannelSetExpr |
A channel set expression containing a set of references to previously declared channel names (i.e.
|
| BasicProcess |
A process definition for an explicit process declaration.
|
| CallAction |
Circus action reference call.
|
| CallProcess |
Circus process reference call.
|
| ChannelDecl |
A channel declaration is a Z declaration that accepts generic types.
|
| ChannelPara |
A channel paragraph that declares channel names with corresponding types, possibly generic.
|
| ChannelSet |
Abstract base classe for Circus channel set expressions.
|
| ChannelSetList |
An abstract name set list.
|
| ChannelSetPara |
A channel set paragraph that declares a name for a channel set.
|
| ChannelSetType |
A channel set type contains the signature of the set of names it represents, where synchronisation channels have null type.
|
| ChannelType |
A channel type is like a generic type, where the type can be
null for synchronisation channels. |
| ChaosAction |
Chaotic Circus action as defined by the UTP (see also Hoare's CSP CHAOS process,
as well as Roscoe's CSP div process).
|
| CircusAction |
An abstract Circus action definition.
|
| CircusActionList |
A list with (concrete) Circus actions.
|
| CircusAnn |
Abstract annotation type for all term annotations used within Circus.
|
| CircusChannelSet |
An channel set expression is a special kind of expression used in Circus that is
not within the Z expressions subtree.
|
| CircusChannelSetList |
A list with (concrete) Circus name sets An alternative implementation
would be a list with name set jokers.
|
| CircusCommand |
An abstract command action definition.
|
| CircusCommunicationList |
A list with (concrete) Circus communications.
|
| CircusConjPara |
A (generic) Circus conjecture paragraph.
|
| CircusFactory |
The object factory for the AST.
|
| CircusFieldList |
A communication fields list.
|
| CircusGuardedCommand |
Abstract base class for IfGuardedCommand and DoGuardedCommand
|
| CircusNameSet |
A name set expression is a special kind of expression used in Circus that is
not within the Z expressions subtree.
|
| CircusNameSetList |
A list with (concrete) Circus name sets An alternative implementation
would be a list with name set jokers.
|
| CircusProcess |
An abstract Circus process definition.
|
| CircusSignature |
Abstract Circus signature: it contains a name.
|
| CircusSigType |
An abstract Circus type that contains a signature.
|
| CircusStateAnn |
Defines if a given paragraph is the process state.
|
| CircusType |
An abstract Circus type.
|
| Communication |
A CSP communication that is part of a prefixing process or action.
|
| CommunicationList |
An abstract communication list.
|
| CommunicationType |
In a declaration like "channel [X] c: X \cross X", the type will be ChannelType(GenericType(List(X), ProdType(List(X, X)))).
|
| DoGuardedCommand |
Command declaring a do (while) statement containing guarded actions in Dijkstra's style.
|
| DotField |
A field that is part of a communication and contains an expression.
|
| ExtChoiceAction |
External choice between two actions.
|
| ExtChoiceActionIte |
Circus action for iterated external choice.
|
| ExtChoiceProcess |
Circus process for external choice.
|
| ExtChoiceProcessIdx |
Circus process for indexed and iterated external choice.
|
| ExtChoiceProcessIte |
Circus process for iterated external choice.
|
| Field |
An abstract field is part of a communication.
|
| FieldList |
An abstract communication fields list.
|
| GuardedAction |
The Circus guarded action defines an action guarded by a Z predicate.
|
| HideAction |
The Circus hide operator defines events concealment within an action definition.
|
| HideProcess |
Circus process with event concealment through hiding.
|
| IfGuardedCommand |
Command declaring a if statement containing guarded actions in Dijkstra's style.
|
| ImplicitChannelAnn |
Annotation used for implicitly declared channnels via indexed processes.
|
| IndexedProcess |
An indexed process definition.
|
| InputField |
An input field that is part of a communication.
|
| IntChoiceAction |
Internal choice between two actions.
|
| IntChoiceActionIte |
Circus action for iterated internal choice.
|
| IntChoiceProcess |
Circus process for internal choice.
|
| IntChoiceProcessIdx |
Circus process for indexed and iterated internal choice.
|
| IntChoiceProcessIte |
Circus process for iterated internal choice.
|
| InterleaveAction |
Interleaving between two actions.
|
| InterleaveActionIte |
Circus action for iterated interleaving.
|
| InterleaveProcess |
Circus process for interleaving.
|
| InterleaveProcessIdx |
Circus process for indexed and iterated interleaving.
|
| InterleaveProcessIte |
Circus process for iterated interleaving.
|
| InterruptAction |
Interruption between two actions.
|
| LetAction |
Abstract local environment.
|
| LetMuAction |
Local environment for mu actions.
|
| LetVarAction |
Local environment for prefixing actions involving input fields, parameterised actions, and variable commands.
|
| MuAction |
The mu operator defines a recursive action.
|
| NameSet |
Abstract base classe for Circus name set expressions.
|
| NameSetList |
An abstract name set list.
|
| NameSetPara |
A name set paragraph that introduces a name for a name set.
|
| NameSetType |
A name set type contains the signature of the set of names it represents.
|
| OnTheFlyDefAnn |
Defines an on-the-fly definition annotation used for both Process and Action terms.
|
| OutputFieldAnn |
Marks a dot field as an output field.
|
| ParAction |
An abstract parallel action definition;
it includes the name set partitions of the state.
|
| ParActionIte |
An abstract parallel iterated action definition.
|
| ParallelAction |
Parallel composition between two actions;
it includes the channel set expression for the synchronisation set.
|
| ParallelActionIte |
Circus action for iterated parallel composition.
|
| ParallelProcess |
Circus process for parallel composition;
it includes the synchronisation set.
|
| ParallelProcessIdx |
Circus process for indexed and iterated parallel composition.
|
| ParallelProcessIte |
Circus process for iterated parallel composition.
|
| ParamAction |
A parameterised action definition.
|
| ParamProcess |
A parameterised process definition.
|
| ParProcess |
Abstract circus process for parallel operators.
|
| ParProcessIdx |
Abstract circus indexed iterated parallel process.
|
| ParProcessIte |
Abstract circus iterated parallel process.
|
| PrefixingAction |
The Circus operator for actions prefixed with a communication.
|
| Process1 |
An abstract unary Circus process.
|
| Process2 |
An abstract binary Circus process.
|
| ProcessD |
An abstract unary Circus process with Z declarations.
|
| ProcessIdx |
An abstract indexed and iterated Circus process with Z declarations.
|
| ProcessIte |
An abstract iterated Circus process with Z declarations.
|
| ProcessPara |
A process paragraph that introduces a name for a process definition.
|
| ProcessSignature |
A process signature consists of the process name, possibly empty generic formal parameters,
possibly empty formal parameters or indexes, and the channels usage.
|
| ProcessSignatureAnn |
A process signature wrapped within an annotation, where generic type are resolved.
|
| ProcessSignatureList |
An signature list with process signatures.
|
| ProcessTransformerPred |
A process transformer predicate is a predicate that relates two process
by one of the available transformation relations in one of the available
models.
|
| ProcessType |
A process type contains its signature.
|
| ProofObligationAnn |
Annotation used for attaching proof obligations to terms.
|
| QualifiedDecl |
This is like
VarDecl, but it includes qualifier attributes for each Name. |
| RenameAction |
Circus action with channel renaming.
|
| RenameProcess |
Circus process with channel renaming.
|
| SchExprAction |
An action given as a schema expression.
|
| SeqAction |
Sequential composition between two actions.
|
| SeqActionIte |
Circus action for iterated sequential composition.
|
| SeqProcess |
Circus process for sequential composition.
|
| SeqProcessIdx |
Circus process for indexed and iterated sequential composition.
|
| SeqProcessIte |
Circus process for iterated sequential composition.
|
| SigmaExpr |
Expression for channel selections, such as c.x or c.true for channel c.
|
| SignatureList |
An abstract signature list.
|
| SkipAction |
Circus action that represents successful silent termination.
|
| SpecStmtCommand |
Circus command declaring a specification statement in Carroll Morgan's style.
|
| StateUpdate |
Process state update is a list of assignment pairs representing
how state updates took place sequentially.
|
| StateUpdateAnn |
Annotation for StateUpdate instances outside ProcessSignature
|
| StopAction |
Circus action that represents deadlock.
|
| SubstitutionAction |
Circus action variable substitution.
|
| TransformerPara |
A circus conjecture between two circus transformer predicates.
|
| TransformerPred |
A quantified refinement predicate, where the quantifier is
universal on the alphabet of the Circus preocess or action.
|
| VarDeclCommand |
Command declaring (possibly multiple) variables local to an action definition.
|
| ZSignatureList |
An signature list with Z signatures.
|
| Enum | Description |
|---|---|
| CallUsage |
A(n) CallUsage enumeration.
|
| CommPattern |
A(n) CommPattern enumeration.
|
| CommUsage |
A(n) CommUsage enumeration.
|
| Model |
A(n) Model enumeration.
|
| ParamQualifier |
A(n) ParamQualifier enumeration.
|
| Transformation |
A(n) Transformation enumeration.
|
Interfaces of the AST for Circus.
See net.sourceforge.czt.base.ast for an overview over the AST for Z.
These interfaces represent the AST for Circus.
Copyright © 2003–2016 Community Z Tools Project. All rights reserved.