AS_CspCASL_Process.der.hs revision 9582375827616730f146b77f9d5a4fd0cc78bc47
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
{- |
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(..),
CSP_FORMULA(..),
PROCESS(..),
PROCESS_NAME,
RENAMING,
) where
import CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR)
import Common.Id
-- DrIFT command
{-! global: UpPos !-}
data EVENT
= TermEvent (TERM ()) Range
| ChanSend CHANNEL_NAME (TERM ()) Range
| ChanNonDetSend CHANNEL_NAME VAR SORT Range
| ChanRecv CHANNEL_NAME VAR SORT Range
deriving (Show,Eq)
-- |Event sets are sets of communication types.
data EVENT_SET = EventSet [COMM_TYPE] Range
deriving (Show,Eq)
-- |Formulas. These are basically just CASL formulas.
data CSP_FORMULA
= Formula (FORMULA ()) Range
deriving (Show,Eq)
-- |CSP renamings are predicate names or op names.
type RENAMING = [Id]
type CHANNEL_NAME = SIMPLE_ID
type PROCESS_NAME = SIMPLE_ID
type COMM_TYPE = SIMPLE_ID
-- |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
-- | @es -> p@ - Prefix process
| PrefixProcess EVENT PROCESS Range
-- | @[] var : es -> p@ - External nondeterministic prefix choice
| ExternalPrefixProcess VAR SORT PROCESS Range
-- | @|~| var : es -> p@ - Internal nondeterministic prefix choice
| InternalPrefixProcess VAR SORT 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
| RelationalRenaming PROCESS RENAMING Range
-- | @if f then p else q@ - Conditional
| ConditionalProcess CSP_FORMULA PROCESS PROCESS Range
-- | Named process
| NamedProcess PROCESS_NAME [EVENT] Range
deriving (Eq, Show)