4176N/A{- |

0N/AModule : $Id$

0N/ADescription : Abstract syntax of CSP-CASL processes

0N/ACopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004

0N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

0N/A

0N/AMaintainer : a.m.gimblett@swan.ac.uk

0N/AStability : provisional

0N/APortability : portable

0N/A

0N/AAbstract syntax of CSP-CASL processes.

0N/A

0N/A-}

0N/A

0N/Amodule CspCASL.AS_CspCASL_Process (

0N/A CHANNEL_NAME,

0N/A CommAlpha,

2362N/A CommType(..),

2362N/A COMM_TYPE,

2362N/A EVENT(..),

0N/A EVENT_SET(..),

4176N/A FQProcVarList,

0N/A PROCESS(..),

0N/A PROCESS_NAME,

1178N/A RENAMING (..),

0N/A TypedChanName(..)

0N/A) where

0N/A

1178N/Aimport CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR)

0N/Aimport Common.Id

0N/Aimport qualified Data.Set as Set

0N/A

4176N/A-- DrIFT command

0N/A{-! global: GetRange !-}

0N/A

0N/Adata EVENT

0N/A -- | @t -> p@ - Term prefix

0N/A = TermEvent (TERM ()) Range

0N/A -- | @[] var :: s -> p@ - External nondeterministic prefix choice

0N/A | ExternalPrefixChoice VAR SORT Range

0N/A -- | @|~| var :: s -> p@ - Internal nondeterministic prefix choice

0N/A | InternalPrefixChoice VAR SORT Range

0N/A -- | @c ! t -> p@ - Channel send

0N/A | ChanSend CHANNEL_NAME (TERM ()) Range

0N/A -- | @c ! var :: s -> p@ - Channel nondeterministic send

0N/A | ChanNonDetSend CHANNEL_NAME VAR SORT Range

0N/A -- | @c ? var :: s -> p@ - Channel recieve

0N/A | ChanRecv CHANNEL_NAME VAR SORT Range

0N/A -- | A fully qualified event contains the (non-fully qualified)

0N/A -- event being qualified. There other parameters depend on the

0N/A -- underlying type of the event.

0N/A --

0N/A -- For TermEvent, the fully qualified channel should be nothing

0N/A -- and the fully qualified term should be the fully qualified

0N/A -- CASL term version of the term being communicated in the inner

0N/A -- process.

0N/A --

0N/A -- For ExternalPrefixChoice and InternalPrefixChoice, the fully

0N/A -- qualified channel should be nothing and the fully qualified

0N/A -- term should be the fully qualified CASL variable version (a

0N/A -- term) of the inner process's variable.

0N/A --

0N/A -- For ChanSend, the fully qualified channel should be the fully

0N/A -- qualified channel of the underlying event and the fully

0N/A -- qualified term should be the fully qualified CASL term

0N/A -- version of the term being communicated in the inner process.

0N/A --

0N/A -- For ChanNonDetSend and ChanRecv, the fully qualified channel

0N/A -- should be the fully qualified channel of the underlying event

0N/A -- and the fully qualified CASL variable version (a term) of the

0N/A -- inner process's variable

0N/A | FQEvent EVENT (Maybe (CHANNEL_NAME, SORT)) (TERM ()) Range

0N/A deriving (Show,Ord, Eq)

0N/A

0N/A-- | Event sets are sets of communication types.

0N/Adata EVENT_SET = EventSet [COMM_TYPE] Range

0N/A -- | FQEvent set distinguishes between channel names and Sorts

0N/A | FQEventSet [CommType] Range

0N/A deriving (Show,Ord, Eq)

0N/A

0N/A-- | CSP renamings are predicate names or op names.

0N/Adata RENAMING = Renaming [Id]

0N/A | FQRenaming [TERM ()]

0N/A deriving (Show,Ord, Eq)

0N/A

0N/Atype CHANNEL_NAME = SIMPLE_ID

0N/A

0N/Atype PROCESS_NAME = SIMPLE_ID

0N/A

0N/Atype COMM_TYPE = SIMPLE_ID

0N/A

0N/A-- | A process communication alphabet consists of a set of sort names

0N/A-- and typed channel names.

0N/Adata TypedChanName = TypedChanName CHANNEL_NAME SORT

0N/A deriving (Eq, Ord, Show)

0N/A

0N/Adata CommType = CommTypeSort SORT

0N/A | CommTypeChan TypedChanName

0N/A deriving (Eq, Ord)

0N/A

0N/Ainstance Show CommType where

0N/A show (CommTypeSort s) = show s

0N/A show (CommTypeChan (TypedChanName c s)) = show (c, s)

0N/A

0N/Atype CommAlpha = Set.Set CommType

0N/A

0N/A-- | FQProcVarList should only contain fully qualified CASL variables

0N/A-- which are TERMs

0N/Atype FQProcVarList = [TERM ()]

0N/A

0N/A-- | CSP-CASL process expressions.

0N/Adata PROCESS

0N/A -- | @Skip@ - Terminate immediately

0N/A = Skip Range

0N/A -- | @Stop@ - Do nothing

0N/A | Stop Range

0N/A -- | @div@ - Divergence

0N/A | Div Range

0N/A -- | @Run es@ - Accept any event in es, forever

0N/A | Run EVENT_SET Range

0N/A -- | @Chaos es@ - Accept\/refuse any event in es, forever

0N/A | Chaos EVENT_SET Range

4176N/A -- | @event -> p@ - Prefix process

0N/A | PrefixProcess EVENT PROCESS Range

0N/A -- | @p ; q@ - Sequential process

0N/A | Sequential PROCESS PROCESS Range

4176N/A -- | @p [] q@ - External choice

0N/A | ExternalChoice PROCESS PROCESS Range

0N/A -- | @p |~| q@ - Internal choice

0N/A | InternalChoice PROCESS PROCESS Range

0N/A -- | @p ||| q@ - Interleaving

0N/A | Interleaving PROCESS PROCESS Range

0N/A -- | @p || q @ - Synchronous parallel

0N/A | SynchronousParallel PROCESS PROCESS Range

0N/A -- | @p [| a |] q@ - Generalised parallel

0N/A | GeneralisedParallel PROCESS EVENT_SET PROCESS Range

0N/A -- | @p [ a || b ] q@ - Alphabetised parallel

0N/A | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range

0N/A -- | @p \\ es@ - Hiding

0N/A | Hiding PROCESS EVENT_SET Range

0N/A -- | @p [[r]]@ - Renaming

0N/A | RenamingProcess PROCESS RENAMING Range

0N/A -- | @if f then p else q@ - Conditional

0N/A | ConditionalProcess (FORMULA ()) PROCESS PROCESS Range

0N/A -- | Named process

0N/A | NamedProcess PROCESS_NAME FQProcVarList Range

0N/A -- | Fully qualified process. The range here shall be the same as

0N/A -- | in the process.

0N/A | FQProcess PROCESS CommAlpha Range

0N/A deriving (Eq, Ord, Show)

0N/A