-
Notifications
You must be signed in to change notification settings - Fork 1
/
help.jade
238 lines (238 loc) · 8.5 KB
/
help.jade
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
doctype html
html
head
block head
meta(charset='utf-8')
title WKTool Help
link(rel='stylesheet', href='http://fonts.googleapis.com/css?family=Open+Sans')
for source in style
link(rel='stylesheet', href="#{source}")
for source in scripts
script(src="#{source}")
body
div.container-fluid
button.close-button.btn.pull-right
i.icon-remove
| Close
h3 WKTool Help
div#help-contents.navbar.navbar-static
div.navbar-inner
ul.nav
li
a(href="#wccs-help") WCCS
li
a(href="#wctl-help") WCTL
li
a(href="#about-help") About
div.row-fluid
p.
WKTool is a verification tool for weighted Kripke structures.
p.
Models are defined using WCCS syntax or WKS/DOT syntax in the upper input area.
Properties are entered as WCTL expressions and can be edited and verified in the lower
section of the interface.
// WCCS syntax
a#wccs-help
h4 WCCS Syntax Reference
p.
The table listed below contains the available WCCS expressions along with their syntax.
table.table.table-bordered
colgroup
col(width='30%')
col(width='70%')
thead
tr
th Expression
th Syntax
tobody
tr
td Comment
td
code(data-highlight='WCTL', data-code='# This is a comment')
tr
td Process Definition
td
code(data-highlight='WCCS', data-code='M := P;')
tr
td Channel Prefix
td
code(data-highlight='WCCS', data-code='<c,8>.P')
| or
code(data-highlight='WCCS', data-code='<c!,8>.P')
| or
code(data-highlight='WCCS', data-code='<c>.P')
tr
td Atomic Label
td
code(data-highlight='WCCS', data-code='a:P')
tr
td Parallel Composition
td
code(data-highlight='WCCS', data-code='P | Q')
tr
td Choice
td
code(data-highlight='WCCS', data-code='P + Q')
tr
td Restriction
td
code(data-highlight='WCCS', data-code='P \ {c}')
| or
code(data-highlight='WCCS', data-code='P \ {c1, c2, c3}')
tr
td Renaming
td
code(data-highlight='WCCS', data-code='P [a1 => a2, a3 => a4]')
| or
code(data-highlight='WCCS', data-code='P [c1 -> c2, c3 -> c4]')
tr
td Empty Process
td
code(data-highlight='WCCS', data-code='0')
// WCTL syntax
a#wctl-help
h4 WCTL Syntax Reference
p.
The following table lists the available WCTL expressions and their syntax.
p.alert.alert-info
| Note for direct and symbolic encodings:
| There is no support for lower-bounds (i.e. >, >=) on temporal formulas
| and negation is only permitted for atomic propositions.
p
| Atoms are denoted by
code(data-highlight='WCTL', data-code='a')
| , boolean expressions by
code(data-highlight='WCTL', data-code='expr')
|, positive integers by
code(data-highlight='WCTL', data-code='k')
| and arithmetic expressions by
code(data-highlight='WCTL', data-code='o')
|.
table.table.table-bordered
colgroup
col(width='30%')
col(width='70%')
thead
tr
th Expression
th Syntax
tobody
tr
td Comment
td
code(data-highlight='WCTL', data-code='# This is a comment')
tr
td Boolean
td
code(data-highlight='WCTL', data-code='true')
|,
code(data-highlight='WCTL', data-code='false')
tr
td Atomic Proposition
td
code(data-highlight='WCTL', data-code='a')
tr
td Negation
td
code(data-highlight='WCTL', data-code='!expr')
tr
td Conjunction
td
code(data-highlight='WCTL', data-code='expr1 && expr2')
tr
td Disjunction
td
code(data-highlight='WCTL', data-code='expr1 || expr2')
tr
td Universal Until
td
code(data-highlight='WCTL', data-code='A expr1 U[<=8] expr2')
| or
code(data-highlight='WCTL', data-code='A expr1 W[>=8] expr2')
| or
code(data-highlight='WCTL', data-code='A expr1 U expr2')
tr
td Existential Until
td
code(data-highlight='WCTL', data-code=' E expr1 U[<=8] expr2')
| or
code(data-highlight='WCTL', data-code=' E expr1 W[>=8] expr2')
| or
code(data-highlight='WCTL', data-code='E expr1 U expr2')
tr
td Universal Finally
td
code(data-highlight='WCTL', data-code='AF[<=8] expr')
| or
code(data-highlight='WCTL', data-code='AF expr')
tr
td Existential Finally
td
code(data-highlight='WCTL', data-code='EF[<=8] expr')
| or
code(data-highlight='WCTL', data-code='EF expr')
tr
td Universal Globally
td
code(data-highlight='WCTL', data-code='AG[<=8] expr')
| or
code(data-highlight='WCTL', data-code='AG expr')
tr
td Existential Globally
td
code(data-highlight='WCTL', data-code='EG[<=8] expr')
| or
code(data-highlight='WCTL', data-code='EG expr')
tr
td Universal Next
td
code(data-highlight='WCTL', data-code='AX[<=8] expr')
| or
code(data-highlight='WCTL', data-code='AX[>=8] expr')
| or
code(data-highlight='WCTL', data-code='AX expr')
tr
td Existential Next
td
code(data-highlight='WCTL', data-code='EX[<=8] expr')
| or
code(data-highlight='WCTL', data-code='EX[>=8] expr')
| or
code(data-highlight='WCTL', data-code='EX expr')
tr
td Comparison
td
code(data-highlight='WCTL', data-code='x < y')
|,
code(data-highlight='WCTL', data-code='x <= y')
|,
code(data-highlight='WCTL', data-code='x == y')
|,
code(data-highlight='WCTL', data-code='x != y')
|,
code(data-highlight='WCTL', data-code='x >= y')
|,
code(data-highlight='WCTL', data-code='x > y')
|, where 'x' and 'y' are arithmetic expressions.
tr
td Arithmetic expression
td
code(data-highlight='WCTL', data-code='o1 * o2')
|,
code(data-highlight='WCTL', data-code='o1 + o2')
|,
code(data-highlight='WCTL', data-code='o1 - o2')
|,
code(data-highlight='WCTL', data-code='o1 / o2')
|,
code(data-highlight='WCTL', data-code='o1 ^ o2')
|,
code(data-highlight='WCTL', data-code='-o')
|, where operands are atomic propositions, integers or arithmetic expressions.
a#about-help
h4 About
p This tool has been developed as part of a project at Aalborg University.
h5 Source Code
p The source code is hosted on
a(href='https://github.com/jonasfj/WKTool') GitHub
| .