hets/CspCASL/AS_CspCASL_Process.der.hs

	AS_CspCASL_Process.der.hs revision 293d1430cbd764408a2565ce95380ee9aedd26c4


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
{- |
Module      :  $Id$
Description :  Abstract syntax of CSP-CASL processes
Copyright   :  (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer  :  a.m.gimblett@swan.ac.uk
Stability   :  provisional
Portability :  portable

Abstract syntax of CSP-CASL processes.

-}

module CspCASL.AS_CspCASL_Process (
    CHANNEL_NAME,
    COMM_TYPE,
    EVENT(..),
    EVENT_SET(..),
    PROCESS(..),
    PROCESS_NAME,
    RENAMING (..),
    CommAlpha,
    CommType(..),
    TypedChanName(..)
) where

import CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR)
import Common.Id
import qualified Data.Set as Set

-- DrIFT command
{-! global: GetRange !-}

data EVENT
    -- | @t -> p@ - Term prefix
    = TermEvent (TERM ()) Range
    -- | @[] var :: s -> p@ - External nondeterministic prefix choice
    | ExternalPrefixChoice VAR SORT Range
    -- | @|~| var :: s -> p@ - Internal nondeterministic prefix choice
    | InternalPrefixChoice VAR SORT Range
    -- | @c ! t -> p@ - Channel send
    | ChanSend CHANNEL_NAME (TERM ()) Range
    -- | @c ! var :: s -> p@ - Channel nondeterministic send
    | ChanNonDetSend CHANNEL_NAME VAR SORT Range
    -- | @c ? var :: s -> p@ - Channel recieve
    | ChanRecv CHANNEL_NAME VAR SORT Range
    -- | A fully qualified event contains the (non-fully qualified)
    --   event being qualified. There other parameters depend on the
    --   underlying type of the event.
    --
    --   For TermEvent, the fully qualified channel should be nothing
    --   and the fully qualified term should be the fully qualified
    --   CASL term version of the term being communicated in the inner
    --   process.
    --
    --   For ExternalPrefixChoice and InternalPrefixChoice, the fully
    --   qualified channel should be nothing and the fully qualified
    --   term should be the fully qualified CASL variable version (a
    --   term) of the inner process's variable.
    --
    --   For ChanSend, the fully qualified channel should be the fully
    --   qualified channel of the underlying event and the fully
    --   qualified term should be the fully qualified CASL term
    --   version of the term being communicated in the inner process.
    --
    --  For ChanNonDetSend and ChanRecv, the fully qualified channel
    --   should be the fully qualified channel of the underlying event
    --   and the fully qualified CASL variable version (a term) of the
    --   inner process's variable
    | FQEvent EVENT (Maybe (CHANNEL_NAME, SORT)) (TERM ()) Range
    deriving (Show,Ord, Eq)

-- | Event sets are sets of communication types.
data EVENT_SET = EventSet [COMM_TYPE] Range
               -- | FQEvent set distinguishes between channel names and Sorts
               | FQEventSet [CommType] Range
                 deriving (Show,Ord, Eq)

-- | CSP renamings are predicate names or op names.
data RENAMING = Renaming [Id]
              | FQRenaming [TERM ()]
                deriving (Show,Ord, Eq)

type CHANNEL_NAME = SIMPLE_ID

type PROCESS_NAME = SIMPLE_ID

type COMM_TYPE = SIMPLE_ID

-- | A process communication alphabet consists of a set of sort names
-- and typed channel names.
data TypedChanName = TypedChanName CHANNEL_NAME SORT
                     deriving (Eq, Ord, Show)

data CommType = CommTypeSort SORT
              | CommTypeChan TypedChanName
                deriving (Eq, Ord)

instance Show CommType where
    show (CommTypeSort s) = show s
    show (CommTypeChan (TypedChanName c s)) = show (c, s)

type CommAlpha = Set.Set CommType

-- | CSP-CASL process expressions.
data PROCESS
    -- | @Skip@ - Terminate immediately
    = Skip Range
    -- | @Stop@ - Do nothing
    | Stop Range
    -- | @div@ - Divergence
    | Div Range
    -- | @Run es@ - Accept any event in es, forever
    | Run EVENT_SET Range
    -- | @Chaos es@ - Accept\/refuse any event in es, forever
    | Chaos EVENT_SET Range
    -- | @event -> p@ - Prefix process
    | PrefixProcess EVENT PROCESS Range
    -- | @p ; q@ - Sequential process
    | Sequential PROCESS PROCESS Range
    -- | @p [] q@ - External choice
    | ExternalChoice PROCESS PROCESS Range
    -- | @p |~| q@ - Internal choice
    | InternalChoice PROCESS PROCESS Range
    -- | @p ||| q@ - Interleaving
    | Interleaving PROCESS PROCESS Range
    -- | @p || q @ - Synchronous parallel
    | SynchronousParallel PROCESS PROCESS Range
    -- | @p [| a |] q@ - Generalised parallel
    | GeneralisedParallel PROCESS EVENT_SET PROCESS Range
    -- | @p [ a || b ] q@ - Alphabetised parallel
    | AlphabetisedParallel PROCESS EVENT_SET EVENT_SET PROCESS Range
    -- | @p \\ es@ - Hiding
    | Hiding PROCESS EVENT_SET Range
    -- | @p [[r]]@ - Renaming
    | RenamingProcess PROCESS RENAMING Range
    -- | @if f then p else q@ - Conditional
    | ConditionalProcess (FORMULA ()) PROCESS PROCESS Range
    -- | Named process
    | NamedProcess PROCESS_NAME [TERM ()] Range
    -- | Fully qualified process. The range here shall be the same as
    -- | in the process.
    | FQProcess PROCESS CommAlpha Range
    deriving (Eq, Ord, Show)