Hets - the Heterogeneous Tool Set

Copyright(c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
LicenseGPLv2 or higher, see LICENSE.txt
Maintainera.m.gimblett@swan.ac.uk
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred

CspCASL.AS_CspCASL_Process

Description

Abstract syntax of CSP-CASL processes.

Synopsis

Documentation

type CommAlpha = Set CommType

Type of communication alphabet

data CommType

Instances

Eq CommType 
Data CommType 
Ord CommType 
Show CommType

Type of communication types, either a sort communication or a typed channel communications.

ShATermConvertible CommType 
GetRange CommType 
Pretty CommType 
Typeable * CommType 

data EVENT

Constructors

TermEvent (TERM ()) Range

t -> p - Term prefix

ExternalPrefixChoice VAR SORT Range

[] var :: s -> p - External nondeterministic prefix choice

InternalPrefixChoice VAR SORT Range

|~| var :: s -> p - Internal nondeterministic prefix choice

ChanSend CHANNEL_NAME (TERM ()) Range

c ! t -> p - Channel send

ChanNonDetSend CHANNEL_NAME VAR SORT Range

c ! var :: s -> p - Channel nondeterministic send

ChanRecv CHANNEL_NAME VAR SORT Range

c ? var :: s -> p - Channel recieve

FQTermEvent (TERM ()) Range

t -> p - Fully Qualified Term prefix

FQExternalPrefixChoice (TERM ()) Range

[] var :: s -> p - Fully Qualified External nondeterministic prefix choice. The term here holds the fully qualified variable (name and sort).

FQInternalPrefixChoice (TERM ()) Range

|~| var :: s -> p - Fully Qualified Internal nondeterministic prefix choice. The term here holds the fully qualified variable (name and sort).

FQChanSend (CHANNEL_NAME, SORT) (TERM ()) Range

c ! t -> p - Fully Qualified Channel send. The term holds the fully term to send.

FQChanNonDetSend (CHANNEL_NAME, SORT) (TERM ()) Range

c ! var :: s -> p - Fully Qualified Channel nondeterministic send. The term here holds the fully qualified variable (name and sort).

FQChanRecv (CHANNEL_NAME, SORT) (TERM ()) Range

c ? var :: s -> p - Fully Qualified Channel recieve. The term here holds the fully qualified variable (name and sort).

data FQ_PROCESS_NAME

A process name is either a fully qualified process name or a plain process name.

Constructors

PROCESS_NAME PROCESS_NAME

A non-fully qualified process name

FQ_PROCESS_NAME PROCESS_NAME ProcProfile

A name with parameter sorts and communication ids from the parser. This is where the user has tried to specify a fully qualified process name

data PROCESS

CSP-CASL process expressions.

Constructors

Skip Range

Skip - Terminate immediately

Stop Range

Stop - Do nothing

Div Range

div - Divergence

Run EVENT_SET Range

Run es - Accept any event in es, forever

Chaos EVENT_SET Range

Chaos es - Accept/refuse any event in es, forever

PrefixProcess EVENT PROCESS Range

event -> p - Prefix process

Sequential PROCESS PROCESS Range

p ; q - Sequential process

ExternalChoice PROCESS PROCESS Range

p [] q - External choice

InternalChoice PROCESS PROCESS Range

p |~| q - Internal choice

Interleaving PROCESS PROCESS Range

p ||| q - Interleaving

SynchronousParallel PROCESS PROCESS Range

p || q - Synchronous parallel

GeneralisedParallel PROCESS EVENT_SET PROCESS Range

p [| a |] q - Generalised parallel

AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range

p [ a || b ] q - Alphabetised parallel

Hiding PROCESS EVENT_SET Range

p \ es - Hiding

RenamingProcess PROCESS RENAMING Range

p [[r]] - Renaming

ConditionalProcess (FORMULA ()) PROCESS PROCESS Range

if f then p else q - Conditional

NamedProcess FQ_PROCESS_NAME [TERM ()] Range

Named process

FQProcess PROCESS CommAlpha Range

Fully qualified process. The range here shall be the same as in the process.

type PROC_ARGS = [SORT]

data ProcProfile

Fully qualified process names have parameter sorts, and a communication alphabet (a Set of sorts). The CommAlpha here should always contain the minimal super sorts only. The communication over subsorts is implied

data RENAMING

CSP renamings are predicate names or op names.

Constructors

Renaming [Rename] 

data TypedChanName

A process communication alphabet consists of a set of sort names and typed channel names.