forked from CAAL/CAAL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhelp.html
207 lines (206 loc) · 12.4 KB
/
help.html
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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
<div class="modal-dialog">
<div class="modal-content">
<div class="modal-header">
<button type="button" class="close" data-dismiss="modal"><span aria-hidden="true">×</span><span class="sr-only">Close</span></button>
<h4 class="modal-title"><span class="small-caps">Caal</span> Specification Language</h4>
</div>
<div class="modal-body ace-crisp">
<p>We refer to our <a href="docs/tutorial.pdf" target="_blank">tutorial</a> for an informal introduction to <span class="small-caps">Caal</span>.</p>
<p>Process constants start with capital letters, channel names with small letters and dual channels begin with an apostrophe (e.g. 'out). The silent action is denoted as tau.</p>
<table class="table">
<thead>
<tr>
<th>CCS Expression</th>
<th>Syntax</th>
</tr>
</thead>
<tbody>
<tr>
<td>Nil process</td>
<td class="monospace">0</td>
</tr>
<tr>
<td>Process definition</td>
<td class="monospace">
<span class="ace_constant">A</span>
<span class="ace_keyword ace_operator">=</span>
a<span class="ace_keyword ace_operator">.</span>tau<span class="ace_keyword ace_operator">.</span><span class="ace_constant">P</span>;
</td>
</tr>
<tr>
<td>Action prefixing - input</td>
<td class="monospace">
a<span class="ace_keyword ace_operator">.</span>tau<span class="ace_keyword ace_operator">.</span><span class="ace_constant">P</span>
</td>
</tr>
<tr>
<td>Action prefixing - output</td>
<td class="monospace">
<span class="ace_variable ace_overline">'a</span><span class="ace_keyword ace_operator">.</span>tau<span class="ace_keyword ace_operator">.</span><span class="ace_constant">P</span>
</td>
</tr>
<tr>
<td>Choice operator</td>
<td class="monospace">
<span class="ace_constant">P</span>
<span class="ace_keyword ace_operator">+</span>
<span class="ace_constant">Q</span>
</td>
</tr>
<tr>
<td>Parallel composition</td>
<td class="monospace">
<span class="ace_constant">P</span>
<span class="ace_keyword ace_operator">|</span>
<span class="ace_constant">Q</span>
</td>
</tr>
<tr>
<td>Restriction</td>
<td class="monospace">
<span class="ace_constant">P</span>
<span class="ace_keyword ace_operator">\</span> {a,b}
</td>
</tr>
<tr>
<td>Renaming of channels</td>
<td class="monospace">
<span class="ace_constant">P</span>[b/a, d/c]
</td>
</tr>
<tr>
<td>Set definition</td>
<td class="monospace">
set <span class="ace_constant">L</span>
<span class="ace_keyword ace_operator">=</span> {a,b,c}
</td>
</tr>
<tr>
<td>Comment</td>
<td class="monospace"><span class="ace_comment">* This is a comment</span></td>
</tr>
</tbody>
</table>
<table class="table">
<thead>
<tr>
<th>TCCS Expression</th>
<th>Syntax</th>
</tr>
</thead>
<tfoot>
<tr>
<td>Delay prefixing</td>
<td class="monospace"><span class="ace_delay">3</span><span class="ace_keyword ace_operator">.</span>tau<span class="ace_keyword ace_operator">.</span><span class="ace_constant">P</span></td>
</tr>
</tfoot>
</table>
<p>The property language supports multiple recursively defined HML formulae that are however not mutually recursive.</p>
<table class="table">
<thead>
<tr>
<th>HML Formula</th>
<th>Syntax</th>
</tr>
</thead>
<tbody>
<tr>
<td>True</td>
<td class="monospace"><span class="ace_constant">tt</span> or <span class="ace_constant">T</span></td>
</tr>
<tr>
<td>False</td>
<td class="monospace"><span class="ace_constant">ff</span> or <span class="ace_constant">F</span></td>
</tr>
<tr>
<td>Conjunction</td>
<td class="monospace"><span class="ace_constant">H</span> <span class="ace_keyword ace_operator">and</span> <span class="ace_constant">G</span></td>
</tr>
<tr>
<td>Disjunction</td>
<td class="monospace"><span class="ace_constant">H</span> <span class="ace_keyword ace_operator">or</span> <span class="ace_constant">G</span></td>
</tr>
<tr>
<td>Strong existential modality</td>
<td class="monospace"><span class="ace_keyword ace_operator"><</span>a,b<span class="ace_keyword ace_operator">></span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Weak existential modality</td>
<td class="monospace"><span class="ace_keyword ace_operator"><<</span>a,b<span class="ace_keyword ace_operator">>></span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Strong universal modality</td>
<td class="monospace"><span class="ace_keyword ace_operator">[</span>a,b<span class="ace_keyword ace_operator">]</span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Weak universal modality</td>
<td class="monospace"><span class="ace_keyword ace_operator">[[</span>a,b<span class="ace_keyword ace_operator">]]</span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Wildcard character for all actions</td>
<td class="monospace">-, e.g. <span class="ace_keyword ace_operator"><</span>-<span class="ace_keyword ace_operator">></span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Minimum fixed-point definition</td>
<td class="monospace">
<span class="ace_constant">X</span>
<span class="ace_keyword ace_operator">min= <</span>a<span class="ace_keyword ace_operator">></span><span class="ace_constant">tt</span>
<span class="ace_keyword ace_operator">or <</span>-<span class="ace_keyword ace_operator">></span><span class="ace_constant">X</span>;
</td>
</tr>
<tr>
<td>Maximum fixed-point definition</td>
<td class="monospace">
<span class="ace_constant">X</span>
<span class="ace_keyword ace_operator">max= <</span>a<span class="ace_keyword ace_operator">></span><span class="ace_constant">tt</span>
<span class="ace_keyword ace_operator">and [-]</span><span class="ace_constant">X</span>;
</td>
</tr>
<tr>
<td>Several recursively defined variables</td>
<td class="monospace">
<span class="ace_constant">X</span>
<span class="ace_keyword ace_operator">max= <</span>a<span class="ace_keyword ace_operator">></span><span class="ace_constant">tt</span>
<span class="ace_keyword ace_operator">and</span>
<span class="ace_constant">Y</span>
<span class="ace_keyword ace_operator">and [</span>-<span class="ace_keyword ace_operator">]</span><span class="ace_constant">X</span>;
<br/>
<span class="ace_constant">Y</span>
<span class="ace_keyword ace_operator">min= <</span>b<span class="ace_keyword ace_operator">></span><span class="ace_constant">tt</span>
<span class="ace_keyword ace_operator">or <-></span><span class="ace_constant">Y</span>;
</td>
</tr>
</tbody>
</table>
<table class="table">
<thead>
<tr>
<th>THML Formula</th>
<th>Syntax</th>
</tr>
</thead>
<tbody>
<tr>
<td>Strong existential timed modality</td>
<td class="monospace"><span class="ace_keyword ace_operator"><</span><span class="ace_delay">4</span><span class="ace_keyword ace_operator">></span><span class="ace_constant">H</span> or <span class="ace_keyword ace_operator"><</span><span class="ace_delay">2</span>,<span class="ace_delay">5</span><span class="ace_keyword ace_operator">></span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Weak existential timed modality</td>
<td class="monospace"><span class="ace_keyword ace_operator"><<</span><span class="ace_delay">4</span><span class="ace_keyword ace_operator">>></span><span class="ace_constant">H</span> or <span class="ace_keyword ace_operator"><<</span><span class="ace_delay">2</span>,<span class="ace_delay">5</span><span class="ace_keyword ace_operator">>></span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Strong universal timed modality</td>
<td class="monospace"><span class="ace_keyword ace_operator">[</span><span class="ace_delay">4</span><span class="ace_keyword ace_operator">]</span><span class="ace_constant">H</span> or <span class="ace_keyword ace_operator">[</span><span class="ace_delay">2</span>,<span class="ace_delay">5</span><span class="ace_keyword ace_operator">]</span><span class="ace_constant">H</span></td>
</tr>
<tr>
<td>Weak universal timed modality</td>
<td class="monospace"><span class="ace_keyword ace_operator">[[</span><span class="ace_delay">4</span><span class="ace_keyword ace_operator">]]</span><span class="ace_constant">H</span> or <span class="ace_keyword ace_operator">[[</span><span class="ace_delay">2</span>,<span class="ace_delay">5</span><span class="ace_keyword ace_operator">]]</span><span class="ace_constant">H</span></td>
</tr>
</tbody>
</table>
</div>
<div class="modal-footer">
<button type="button" class="btn btn-primary" data-dismiss="modal">Close</button>
</div>
</div>
</div>