remfin.test 4.74 KB
Newer Older
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
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 3 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program.  If not, see <http://www.gnu.org/licenses/>.


. ./defs

set -e

autfilt=../../bin/autfilt

cat >test1 <<EOF
/*
** This was a TGBA for GFa & GFb, but
** the acceptance has been changed to Fin(0)|Fin(1)
** so this is now the complement automaton.
33
*/
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Fin(0)|Fin(1)
--BODY--
State: 0
[0&1] 0 {0 1}
[!0&!1] 0
[!0&1] 0 {1}
[0&!1] 0 {0}
--END--
/*
** This one has a mix of Inf and Fin acceptance, but no interference
** between the Fin sets
49
*/
50
51
52
53
54
55
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 5 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(4)
--BODY--
56
State: 0 {3 4}
57
58
59
[t] 0
[0] 1 {1}
[!0] 2 {0}
60
State: 1 {3}
61
62
63
64
65
66
67
68
69
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2}
State: 2
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0}
--END--
/*
70
71
72
** This one is similar, but Inf(0) is used in two terms, so
** we need to introduce extra sets in the output.
*/
73
74
75
76
77
78
79
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(0)
--BODY--
80
State: 0 {3}
81
82
83
[t] 0
[0] 1 {1}
[!0] 2 {0}
84
State: 1 {3}
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
[1] 0
[0&1] 1 {0}
[!0&1] 2 {2}
State: 2
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0}
--END--
/*
** The t and f acceptance.
*/
HOA: v1
States: 1
Start: 0
Acceptance: 0 f
--BODY--
State: 0
--END--
HOA: v1
States: 1
Start: 0
Acceptance: 0 t
--BODY--
State: 0
[t] 0
--END--
/* An example from ltl2dstar.
** No new state should be added.
*/
HOA: v1
States: 2
acc-name: Rabin 1
Acceptance: 2 (Fin(0)&Inf(1))
Start: 0
AP: 1 "p0"
--BODY--
State: 0 {}
0
1
State: 1 {1}
1
1
--END--
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
HOA: v1
States: 8
Start: 2
AP: 1 "p1"
Acceptance: 4 (Fin(3) & Inf(0)) | (Fin(1) & Fin(3)) |
              (Fin(1) & Inf(2)) | (Inf(0)&Inf(2))
properties: trans-labels explicit-labels state-acc complete deterministic
--BODY--
State: 0
[!0] 6
[0] 0
State: 1 {2}
[!0] 3
[0] 3
State: 2 {2}
[!0] 5
[0] 1
State: 3 {2}
[!0] 6
[0] 0
State: 4 {2}
[!0] 6
[0] 4
State: 5 {2}
[!0] 7
[0] 3
State: 6 {1 2}
[!0] 6
[0] 0
State: 7 {3}
[!0] 6
[0] 4
--END--
161
162
163
164
165
166
167
EOF

cat >expected <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
168
169
acc-name: Buchi
Acceptance: 1 Inf(0)
170
171
172
173
174
175
176
177
178
179
180
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[0&1] 0
[!0&!1] 0
[!0&1] 0
[0&!1] 0
[!0&!1] 1
[!0&1] 1
[!0&!1] 2
[0&!1] 2
181
State: 1 {0}
182
183
[!0&!1] 1
[!0&1] 1
184
State: 2 {0}
185
186
187
188
189
190
191
[!0&!1] 2
[0&!1] 2
--END--
HOA: v1
States: 6
Start: 0
AP: 2 "a" "b"
192
Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2))
193
194
195
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
196
197
198
[t] 0 {2 3}
[0] 1 {2 3}
[!0] 2 {2 3}
199
State: 1
200
201
202
[1] 0 {2}
[0&1] 1 {2}
[!0&1] 2 {1 2}
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
State: 2
[!1] 0
[0&!1] 1
[!0&!1] 2
[!1] 3
[0&!1] 4
[!0&!1] 5
State: 3
State: 4
State: 5
[!1] 3
[0&!1] 4 {0}
[!0&!1] 5 {0}
--END--
HOA: v1
States: 6
Start: 0
AP: 2 "a" "b"
221
Acceptance: 5 (Inf(0)&Inf(1)&Inf(4)) | Inf(0) | (Inf(2)&Inf(3))
222
223
224
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
225
226
227
[t] 0 {3}
[0] 1 {3}
[!0] 2 {0 3}
228
State: 1
229
230
231
[1] 0 {3}
[0&1] 1 {0 3}
[!0&1] 2 {2 3}
232
State: 2
233
234
235
236
237
238
[!1] 0
[0&!1] 1 {0}
[!0&!1] 2 {0}
[!1] 3
[0&!1] 4 {0}
[!0&!1] 5 {0}
239
240
241
State: 3
State: 4
State: 5
242
243
244
[!1] 3 {1 4}
[0&!1] 4 {0 1 4}
[!0&!1] 5 {0 1 4}
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
--END--
HOA: v1
States: 1
Start: 0
AP: 0
Acceptance: 0 f
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
--END--
HOA: v1
States: 1
Start: 0
AP: 0
acc-name: all
Acceptance: 0 t
261
262
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
263
264
265
266
267
268
269
270
--BODY--
State: 0
[t] 0
--END--
HOA: v1
States: 2
Start: 0
AP: 1 "p0"
271
272
acc-name: Buchi
Acceptance: 1 Inf(0)
273
274
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
275
276
277
278
--BODY--
State: 0
[!0] 0
[0] 1
279
State: 1 {0}
280
281
282
[!0] 1
[0] 1
--END--
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
HOA: v1
States: 12
Start: 2
AP: 1 "p1"
Acceptance: 2 Inf(1) | Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[!0] 6
[0] 0
[0] 9
[0] 11
State: 1 {0 1}
[!0] 3
[0] 3
State: 2 {0 1}
[!0] 5
[0] 1
State: 3 {0 1}
[!0] 6
[0] 0
State: 4 {0 1}
[!0] 6
[0] 4
State: 5 {0 1}
[!0] 7
[0] 3
State: 6
[!0] 6
[0] 0
State: 7 {1}
[!0] 6
[0] 4
State: 8
State: 9
[!0] 8
[0] 9
State: 10
State: 11 {1}
[!0] 10
[0] 11
--END--
325
326
327
328
329
EOF

run 0 $autfilt -H --remove-fin test1 > output
cat output
diff -u output expected