Uses of Package
net.sourceforge.czt.circus.ast

Packages that use net.sourceforge.czt.circus.ast

Package	Description
net.sourceforge.czt.circus.ast	Interfaces of the AST for Circus.
net.sourceforge.czt.circus.impl	Implementation classes of the AST for Circus.
net.sourceforge.czt.circus.jaxb	Provides classes enabling validation as well as reading and writing XML using Jaxb generated classes.
net.sourceforge.czt.circus.util
net.sourceforge.czt.circus.visitor	Visitors for the AST for Circus.

Classes in net.sourceforge.czt.circus.ast used by net.sourceforge.czt.circus.ast

Class and 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.
CallUsage A(n) CallUsage enumeration.
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.
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.
CommPattern A(n) CommPattern enumeration.
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)))).
CommUsage A(n) CommUsage enumeration.
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.
Model A(n) Model enumeration.
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.
ParamQualifier A(n) ParamQualifier enumeration.
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.
Transformation A(n) Transformation enumeration.
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.

Classes in net.sourceforge.czt.circus.ast used by net.sourceforge.czt.circus.impl

Class and 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.
CallUsage A(n) CallUsage enumeration.
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.
CommPattern A(n) CommPattern enumeration.
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)))).
CommUsage A(n) CommUsage enumeration.
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.
Model A(n) Model enumeration.
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.
ParamQualifier A(n) ParamQualifier enumeration.
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.
Transformation A(n) Transformation enumeration.
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.

Classes in net.sourceforge.czt.circus.ast used by net.sourceforge.czt.circus.jaxb

Class and Description
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.
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.
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).
CircusActionList A list with (concrete) Circus actions.
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.
CircusCommunicationList A list with (concrete) Circus communications.
CircusFactory The object factory for the AST.
CircusFieldList A communication fields list.
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.
CircusStateAnn Defines if a given paragraph is the process state.
Communication A CSP communication that is part of a prefixing process or action.
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.
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.
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.
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.
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.
PrefixingAction The Circus operator for actions prefixed with a communication.
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.
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.
VarDeclCommand Command declaring (possibly multiple) variables local to an action definition.
ZSignatureList An signature list with Z signatures.

Classes in net.sourceforge.czt.circus.ast used by net.sourceforge.czt.circus.util

Class and Description
Action2 An abstract binary 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.
CallUsage A(n) CallUsage enumeration.
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.
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.
CircusCommunicationList A list with (concrete) Circus communications.
CircusFactory The object factory for the AST.
CircusFieldList A communication fields list.
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.
CircusStateAnn Defines if a given paragraph is the process state.
CommPattern A(n) CommPattern enumeration.
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)))).
CommUsage A(n) CommUsage enumeration.
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.
LetMuAction Local environment for mu actions.
LetVarAction Local environment for prefixing actions involving input fields, parameterised actions, and variable commands.
Model A(n) Model enumeration.
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.
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.
ParamQualifier A(n) ParamQualifier enumeration.
PrefixingAction The Circus operator for actions prefixed with a communication.
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.
Transformation A(n) Transformation enumeration.
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.

Classes in net.sourceforge.czt.circus.ast used by net.sourceforge.czt.circus.visitor

Class and 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.
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.