Package net.sourceforge.czt.circus.ast

Interfaces of the AST for Circus.

See: Description

Interface Summary

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 Summary

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.

Package net.sourceforge.czt.circus.ast Description

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.