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
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
|
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0//EN">
<HTML><HEAD>
<TITLE>The property automaton translator interface</TITLE>
<LINK REV=MADE HREF="mailto:msmakela@tcs.hut.fi">
</HEAD>
<BODY>
<H1>The property automaton translator interface</H1>
<P>Maria relies on external programs translating LTL formulae into
generalised Bchi automata or finite-word automata. It communicates
with these programs by writing a formula to the standard input of the
translator and by reading the translated automaton from the standard
output of the translator. Each formula is translated in a separate
run of the external program. The program is invoked without
arguments.</P>
<H1>Grammar Definitions</H1>
<P>The grammars are presented in Backus-Naur Form, one grammar rule
per line. Comments delimited by the symbols <EM>/*</EM> and
<EM>*/</EM> are not part of the formal grammar. Non-terminal symbols
are enclosed within single quotes or presented as <A
HREF="http://www.gnu.org/software/flex/flex.html">Flex</A>-style
regular-expressions.</P>
<H2>Output format for LTL formulae</H2>
<P>Currently, Maria does not make use of the implication, equivalence
or exclusive disjunction operators, but they might be generated in the
future.</P>
<H3>Propositional operators</H3>
<TABLE>
<TR>
<TD><A NAME="f"><f></A> ::=</TD>
<TD><CODE>'t'</CODE></TD>
<TD><EM>/* true */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'f'</CODE></TD>
<TD><EM>/* false */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'p'[0-9]+</CODE></TD>
<TD><EM>/* proposition */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'!'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* negation */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'|'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* disjunction */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'&'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* conjunction */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'i'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* implication:
<CODE>"i <f1> <f2>"</CODE> is short-hand for
<CODE>"| ! <f1> <f2>"</CODE> */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'e'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* equivalence */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'^'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* exclusive disjunction (xor) */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>[ \t\n\r\v\f]</CODE> <<A HREF="#f">f</A>></TD>
<TD><EM>/* white space is ignored */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><<A HREF="#f">f</A>> <CODE>[ \t\n\r\v\f]</CODE></TD>
<TD><EM>/* white space is ignored */</EM></TD>
</TR>
</TABLE>
<H3>Temporal operators</H3>
<TABLE>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'X'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* next */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'F'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* finally, eventually */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'G'</CODE>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* globally, henceforth */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'U'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* until */</EM></TD>
</TR>
<TR>
<TD><f> ::=</TD>
<TD><CODE>'V'</CODE>
<<A HREF="#f">f</A>>
<<A HREF="#f">f</A>></TD>
<TD><EM>/* release */</EM></TD>
</TR>
</TABLE>
<H2>Input format for automata</H2>
<P>The same grammar is used for both finite automata (safety
properties) and for generalised Bchi automata (liveness properties).
A finite automaton has zero acceptance sets and exactly one final
state that does not have any successor states. A generalised Bchi
automaton has no final state. If the number of acceptance sets of a
generalised Bchi automaton is zero, this means that the automaton has
one acceptance set to which all states belong.</P>
<TABLE>
<TR>
<TD><A NAME="automaton"><automaton></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<CODE>[0-9]+</CODE>
<<A HREF="#states">states</A>>
</TD>
<TD><EM>/* first the number of states, then the number of acceptance sets
(if the latter is 0, it is a generalised Bchi automaton whose all states
accept, or a finite automaton) */</EM></TD>
</TR>
<TR>
<TD><A NAME="space"><space></A> ::=</TD>
<TD><CODE>[ \n]+</CODE></TD>
</TR>
<TR>
<TD><A NAME="states"><states></A> ::=</TD>
<TD><EM>/* empty */</EM></TD>
</TR>
<TR>
<TD><states> ::=</TD>
<TD><<A HREF="#states">states</A>> <<A HREF="#space">space</A>>
<<A HREF="#state">state</A>></TD>
</TR>
<TR>
<TD><A NAME="state"><state></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<<A HREF="#finitial">finitial?</A>> <<A HREF="#space">space</A>>
<<A HREF="#acceptance sets">acceptance sets</A>> '-1'
<<A HREF="#transitions">transitions</A>> '-1'</TD>
<TD><EM>/* state identifiers can be arbitrary unsigned integers */</EM></TD>
</TR>
<TR>
<TD><A NAME="finitial"><finitial?></A> ::=</TD>
<TD><CODE>'0'</CODE></TD>
<TD><EM>/* not an initial or a final state */</EM></TD>
</TR>
<TR>
<TD><finitial?> ::=</TD>
<TD><CODE>'1'</CODE></TD>
<TD><EM>/* initial state (exactly one state must be initial) */</EM></TD>
</TR>
<TR>
<TD><finitial?> ::=</TD>
<TD><CODE>'2'</CODE></TD>
<TD><EM>/* final state (exactly one state must be final for finite automata) */</EM></TD>
</TR>
<TR>
<TD><A NAME="acceptance sets"><acceptance sets></A> ::=</TD>
<TD><EM>/* empty */</EM></TD>
</TR>
<TR>
<TD><acceptance sets> ::=</TD>
<TD><<A HREF="#acceptance sets">acceptance sets</A>>
<CODE>[0-9]+</CODE> <<A HREF="#space">space</A>></TD>
<TD><EM>/* acceptance set identifiers can be arbitrary unsigned integers */</EM></TD>
</TR>
<TR>
<TD><A NAME="transitions"><transitions></A> ::=</TD>
<TD><EM>/* empty */</EM></TD>
</TR>
<TR>
<TD><transitions> ::=</TD>
<TD><<A HREF="#transitions">transitions</A>>
<<A HREF="#space">space</A>>
<<A HREF="#transition">transition</A>></TD>
</TR>
<TR>
<TD><A NAME="transition"><transition></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<CODE>'t'</CODE></TD>
<TD><EM>/* constantly enabled transition to
a <A HREF="#state">state</A> */</EM></TD>
</TR>
<TR>
<TD><A NAME="transition"><transition></A> ::=</TD>
<TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* conditionally enabled transition to
a <A HREF="#state">state</A> */</EM></TD>
</TR>
<TR>
<TD><A NAME="gate"><gate></A> ::=</TD>
<TD><CODE>'p'[0-9]+</CODE></TD>
<TD><EM>/* proposition */</EM></TD>
</TR>
<TR>
<TD><gate> ::=</TD>
<TD><CODE>'!'</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* negation */</EM></TD>
</TR>
<TR>
<TD><gate> ::=</TD>
<TD><CODE>'|'</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* disjunction */</EM></TD>
</TR>
<TR>
<TD><gate> ::=</TD>
<TD><CODE>'&'</CODE> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>> <<A HREF="#space">space</A>>
<<A HREF="#gate">gate</A>></TD>
<TD><EM>/* conjunction */</EM></TD>
</TR>
</TABLE>
<H1>Hints for Debugging</H1>
<P>Maria maps the state numbers in the property automata to a
contiguous sequence. If you want to see the automata after this
mapping, define the preprocessor symbol <CODE>DEBUG_AUTOMATON</CODE>
when compiling the file <CODE>Property.C</CODE>. In that way, Maria
will dump the mapped automaton to the standard output. The automaton
can be visualised with the <CODE>lbt2dot</CODE> tool of <A
HREF="http://www.tcs.hut.fi/Software/maria/tools/lbt/">LBT</A>.</P>
<P>To grab the formula sent by Maria to the external translator, write
a wrapper shell script for the translator that does something like
<CODE>tee formula.txt | exec the-real-translator</CODE>.</P>
</BODY></HTML>
|
