readsave.test 19.9 KB
Newer Older
1
#!/bin/sh
2
# -*- coding: utf-8 -*-
3
# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016, 2017 Laboratoire de
4
# Recherche et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
5
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
6
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
12
# et Marie Curie.
#
# 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
13
# the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
14
15
16
17
18
19
20
21
# (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
22
# along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
23

24
25
26
27
28

. ./defs

set -e

29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
cat >input <<\EOF
HOA: v1
States: 3
Start: 0
AP: 3 "a" "b" "F\\G"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {0 1}
[0&!1] 1
State: 1 {0}
[2] 2
State: 2
[t] 0
--END--
45
46
EOF

47
run 0 autfilt --hoa input > stdout
48
diff stdout input
49

50
test `autfilt -c --is-weak input` = 0
51

52
53
54
55
56
57
58
59
autfilt -H1.1 -v --is-weak input | grep properties: | tee props
cat >expected.props <<EOF
properties: trans-labels explicit-labels state-acc !complete
properties: deterministic !weak
EOF
diff expected.props props


60
61
# Transition merging
cat >input <<\EOF
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[0&1] 1 {0}
[!1] 1
[0&!1] 1 {0}
State: 1
[!1] 0
[1&0] 0 {0}
[0&!1] 0 {0}
--END--
79
80
81
EOF

cat >expected <<\EOF
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!1] 1
[0] 1 {0}
State: 1
[!1] 0
[0] 0 {0}
--END--
97
98
EOF

99
run 0 autfilt --merge-transitions --hoa input > stdout
100
cat stdout
101
run 0 autfilt -F stdout --isomorph expected
102
103

# Likewise, with a randomly generated TGBA.
104
run 0 randaut -Q 20 a b -e 0.2 -a 0.2 -A 2 --hoa | tee input
105

106
# the first read-write can renumber the states
107
run 0 autfilt --hoa --merge-transitions input > stdout
108
run 0 autfilt -F input --isomorph stdout
109

110
# But this second output should be the same as the first
111
run 0 autfilt --hoa stdout > stdout2
112
diff stdout stdout2
113
114

# Find formula that can be translated into a 3-state automaton, and
115
116
117
# exercise both %M and %m.  The nonexistant file should never be
# open, because the input stream is infinite and autfilt should
# stop after 10 automata.
118
119
randltl -n -1 a b | ltl2tgba |
    autfilt -F - -F nonexistant --states=3 --edges=..10 --acc-sets=1.. \
120
	     --name='%M, %S states' --stats='<%m>, %e, %a' -n 10 > output
121
cat >expected <<EOF
122
123
<F(b | Ga), 3 states>, 5, 1
<F(!b & G(!b | G!a)), 3 states>, 5, 1
124
<XF!b, 3 states>, 4, 1
125
<G!b | Gb, 3 states>, 4, 1
126
127
128
129
130
131
<XFb, 3 states>, 4, 1
<F(b W a), 3 states>, 6, 1
<(a & !b & (b | (!b M F!a))) | (!a & (b | (!b & (b W Ga)))), 3 states>, 5, 1
<(a & (a U !b)) | (!a & (!a R b)), 3 states>, 5, 1
<a | G((a & GFa) | (!a & FG!a)), 3 states>, 4, 1
<XXG(!a & (Fa W Gb)), 3 states>, 3, 1
132
133
EOF
diff output expected
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


cat >input <<EOF
HOA: v1
States: 10
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {0}
[!0] 1 {0}
[!0] 2 {0}
[0] 3 {0}
[0] 3 {0 2}
[!0] 2 {0 2}
[!0] 4 {1}
[!0] 5 {1}
[!0] 6 {1}
[!0] 6 {1 2}
[!0] 7 {1}
[!0] 8 {1}
[!0] 9 {1}
[!0] 9 {1 2}
[!0] 4 {0 1}
[!0] 5 {0 1}
[!0] 6 {0 1}
[!0] 6 {0 1 2}
[!0] 7 {0 1}
[!0] 8 {0 1}
[!0] 9 {0 1}
[!0] 9 {0 1 2}
State: 1
[0] 3 {0 2}
State: 2
[!0] 2 {0 2}
[!0] 6 {1 2}
[!0] 9 {1 2}
[!0] 6 {0 1 2}
[!0] 9 {0 1 2}
State: 3
[!0] 1 {0 2}
[!0] 2 {0}
[0] 3 {0 2}
[!0] 2 {0 2}
[!0] 5 {1 2}
[!0] 6 {1}
[!0] 6 {1 2}
[!0] 8 {1 2}
[!0] 9 {1}
[!0] 9 {1 2}
[!0] 5 {0 1 2}
[!0] 6 {0 1}
[!0] 6 {0 1 2}
[!0] 8 {0 1 2}
[!0] 9 {0 1}
[!0] 9 {0 1 2}
State: 4
[!0] 4 {1}
[!0] 5 {1}
[!0] 6 {1}
[!0] 6 {1 2}
[!0] 7
[!0] 8
[!0] 9
[!0] 9 {2}
[!0] 7 {1}
[!0] 8 {1}
[!0] 9 {1}
[!0] 9 {1 2}
State: 5
State: 6
[!0] 6 {1 2}
[!0] 9 {2}
[!0] 9 {1 2}
State: 7
[0] 0 {0}
[0] 3 {0}
[0] 3 {0 2}
State: 8
[0] 3 {0 2}
State: 9
--END--
EOF

cat >expected <<EOF
HOA: v1
name: "63->32 edges, 64->33 transitions"
States: 10
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
properties: trans-labels explicit-labels
--BODY--
State: 0
[t] 0 {0}
[!0] 1 {0}
[!0] 2 {0 2}
[0] 3 {0 2}
[!0] 4 {0 1}
[!0] 5 {0 1}
[!0] 6 {0 1 2}
[!0] 7 {0 1}
[!0] 8 {0 1}
[!0] 9 {0 1 2}
State: 1 {0 2}
[0] 3
State: 2
[!0] 2 {0 2}
[!0] 6 {0 1 2}
[!0] 9 {0 1 2}
State: 3
[!0] 1 {0 2}
[!0] 2 {0 2}
[0] 3 {0 2}
[!0] 5 {0 1 2}
[!0] 6 {0 1 2}
[!0] 8 {0 1 2}
[!0] 9 {0 1 2}
State: 4
[!0] 4 {1}
[!0] 5 {1}
[!0] 6 {1 2}
[!0] 7 {1}
[!0] 8 {1}
[!0] 9 {1 2}
State: 5
State: 6 {1 2}
[!0] 6
[!0] 9
State: 7
[0] 0 {0}
[0] 3 {0 2}
State: 8 {0 2}
[0] 3
State: 9
--END--
EOF

276
autfilt --merge -Hm input --name="%E->%e edges, %T->%t transitions" > output
277
diff output expected
278
279


280
ltl2tgba -x degen-lskip=1 --ba > tmp.hoa <<EOF
281
282
283
284
a U b
false
!b && Xb && GFa
EOF
285
autfilt <tmp.hoa --stats='"%M","%w"' > output
286
287
288
289
290
291
cat >expected <<EOF
"a U b","cycle{b}"
"0",""
"!b & X(b & GFa)","!b; cycle{a & b}"
EOF
diff output expected
292
293


294
cat >input <<EOF
295
296
297
298
299
300
301
302
303
HOA: v1
States: 4
Start: 2
Start: 3
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
304
State: 0 "s0" {0}
305
[1] 0
306
State: 1 "s1" {0}
307
[0] 1
308
State: 2 "s2"
309
[1] 0
310
State: 3 "s3"
311
312
313
[0] 1
--END--
EOF
314

315
autfilt -H input |
316
    SPOT_DEFAULT_FORMAT=dot \
317
    SPOT_DOTDEFAULT=vcsnaA \
318
319
    SPOT_DOTEXTRA='/* hello world */' \
    autfilt >output
320
321
322
323

cat >expected <<EOF
digraph G {
  node [shape="circle"]
324
  /* hello world */
325
326
327
  I [label="", style=invis, height=0]
  I -> 3
  subgraph cluster_0 {
328
  color=green
329
  1 [label="s1", peripheries=2]
330
331
  }
  subgraph cluster_1 {
332
  color=green
333
  0 [label="s0", peripheries=2]
334
335
  }
  subgraph cluster_2 {
336
  color=black
337
  3 [label="s3"]
338
  }
339
340
  0 -> 0 [label="b"]
  1 -> 1 [label="a"]
341
  2 [label="s2"]
342
  2 -> 0 [label="b"]
343
344
  3 -> 1 [label="a"]
  3 -> 0 [label="b"]
345
346
347
348
}
EOF

diff output expected
349

350
test 1 = `autfilt -H input --complete | autfilt --is-complete --count`
351
352


353
# The SPOT_DEFAULT_FORMAT envvar should be ignored if --dot is given.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
354
355
# --dot=k should be ignored when not applicable.
SPOT_DEFAULT_FORMAT=hoa ltl2tgba --dot=ak 'GFa & GFb' >output
356
357
358
359
cat output
cat >expected <<EOF
digraph G {
  rankdir=LR
360
  label="Inf(0)&Inf(1)\n[gen. Büchi 2]"
361
  labelloc="t"
362
  node [shape="circle"]
363
364
365
366
367
368
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label="!a & !b"]
  0 -> 0 [label="!a & b\n{1}"]
  0 -> 0 [label="a & !b\n{0}"]
369
  0 -> 0 [label="a & b\n{0,1}"]
370
371
372
373
}
EOF
diff output expected

374
ltl2tgba -dban 'GFa & GFb' >output
375
376
377
378
cat output
cat >expected <<EOF
digraph G {
  rankdir=LR
379
  label="G(Fa & Fb)\nInf(⓿)&Inf(❶)\n[gen. Büchi 2]"
380
  labelloc="t"
381
  node [shape="circle"]
382
383
384
385
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
  0 -> 0 [label="!a & !b"]
386
387
  0 -> 0 [label="!a & b\n❶"]
  0 -> 0 [label="a & !b\n⓿"]
388
  0 -> 0 [label="a & b\n⓿❶"]
389
390
391
392
393
}
EOF
diff output expected


394
SPOT_DOTDEFAULT=bra ltl2tgba --dot='e.f(Lato)' 'GFa & GFb' >output
395
396
cat output

397
398
zero='<font color="#1F78B4">⓿</font>'
one='<font color="#FF4DA0">❶</font>'
399
400
401
cat >expected <<EOF
digraph G {
  rankdir=LR
402
  label=<Inf($zero)&amp;Inf($one)<br/>[gen. Büchi 2]>
403
404
405
406
407
408
  labelloc="t"
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  I [label="", style=invis, width=0]
  I -> 0
409
  0 [label=<0>]
410
411
412
  0 -> 0 [label=<!a &amp; !b>]
  0 -> 0 [label=<!a &amp; b<br/>$one>]
  0 -> 0 [label=<a &amp; !b<br/>$zero>]
413
  0 -> 0 [label=<a &amp; b<br/>$zero$one>]
414
415
416
}
EOF
diff output expected
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472


cat >in <<EOF
HOA: v1
States: 10
Start: 0
AP: 2 "a" "b"
Acceptance: 4 Fin(0) | (Fin(1) & Inf(2)) | Fin(3)
--BODY--
State: 0
[!0&!1] 1
[0&!1] 2
[!0&1] 3
[0&1] 4
State: 1 "test me" {0 3}
[!0&!1] 1
[0&!1] 2
[!0&1] 6
[0&1] 7
State: 2 {0 2 3}
[!0&!1] 1
[0&!1] 2
[!0&1] 6
[0&1] 7
State: 3 {3}
[t] 5
State: 4 "hihi" {2 3}
[t] 5
State: 5 {1 3}
[t] 5
State: 6 {0}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
State: 7 {0 2}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
State: 8 {0 3}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
State: 9 {0 2 3}
[!0&!1] 8
[!0&1] 6
[0&!1] 9
[0&1] 7
--END--
EOF

cat >expected <<EOF
digraph G {
  rankdir=LR
473
  label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))\n[gen. Rabin 3]"
474
475
476
477
  labelloc="t"
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0"]
478
479
480
481
  0 -> 1 [label="!a & !b", taillabel="0"]
  0 -> 2 [label="a & !b", taillabel="1"]
  0 -> 3 [label="!a & b", taillabel="2"]
  0 -> 4 [label="a & b", taillabel="3"]
482
  1 [label="test me\n⓿❸"]
483
484
485
486
  1 -> 1 [label="!a & !b", taillabel="0"]
  1 -> 2 [label="a & !b", taillabel="1"]
  1 -> 6 [label="!a & b", taillabel="2"]
  1 -> 7 [label="a & b", taillabel="3"]
487
  2 [label="2\n⓿❷❸"]
488
489
490
491
  2 -> 1 [label="!a & !b", taillabel="0"]
  2 -> 2 [label="a & !b", taillabel="1"]
  2 -> 6 [label="!a & b", taillabel="2"]
  2 -> 7 [label="a & b", taillabel="3"]
492
  3 [label="3\n❸"]
493
  3 -> 5 [label="1", taillabel="0"]
494
  4 [label="hihi\n❷❸"]
495
  4 -> 5 [label="1", taillabel="0"]
496
  5 [label="5\n❶❸"]
497
  5 -> 5 [label="1", taillabel="0"]
498
  6 [label="6\n⓿"]
499
500
501
502
  6 -> 8 [label="!a & !b", taillabel="0"]
  6 -> 6 [label="!a & b", taillabel="1"]
  6 -> 9 [label="a & !b", taillabel="2"]
  6 -> 7 [label="a & b", taillabel="3"]
503
  7 [label="7\n⓿❷"]
504
505
506
507
  7 -> 8 [label="!a & !b", taillabel="0"]
  7 -> 6 [label="!a & b", taillabel="1"]
  7 -> 9 [label="a & !b", taillabel="2"]
  7 -> 7 [label="a & b", taillabel="3"]
508
  8 [label="8\n⓿❸"]
509
510
511
512
  8 -> 8 [label="!a & !b", taillabel="0"]
  8 -> 6 [label="!a & b", taillabel="1"]
  8 -> 9 [label="a & !b", taillabel="2"]
  8 -> 7 [label="a & b", taillabel="3"]
513
  9 [label="9\n⓿❷❸"]
514
515
516
517
  9 -> 8 [label="!a & !b", taillabel="0"]
  9 -> 6 [label="!a & b", taillabel="1"]
  9 -> 9 [label="a & !b", taillabel="2"]
  9 -> 7 [label="a & b", taillabel="3"]
518
519
520
}
EOF

521
autfilt --dot=bao in >out
522
diff out expected
523

524
525
526
cat >expected2 <<EOF
digraph G {
  rankdir=LR
527
  label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))\n[gen. Rabin 3]"
528
  labelloc="t"
529
  node [shape="circle"]
530
531
532
533
534
535
536
537
538
539
540
541
542
543
  I [label="", style=invis, width=0]
  0 [label="0"]
  1 [label="1\n⓿❸"]
  2 [label="2\n⓿❷❸"]
  3 [label="3\n❸"]
  4 [label="4\n❷❸"]
  5 [label="5\n❶❸"]
  6 [label="6\n⓿"]
  7 [label="7\n⓿❷"]
  8 [label="8\n⓿❸"]
  9 [label="9\n⓿❷❸"]
}
EOF

544
545
# This should remove the state names, and automatically use circled
# states.
546
autfilt --dot=bao1 in | grep -v '>' >out
547
diff out expected2
548

549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
cat >expected3 <<EOF
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  0 [label="6", peripheries=2]
  u0 [label="...", shape=none, width=0, height=0]
  1 [label="0", peripheries=2]
  2 [label="1", peripheries=2]
  3 [label="2", peripheries=2]
  4 [label="3", peripheries=2]
}
EOF

# States should be circled even if <5 causes all states to be named,
# because the names are smaller then 2 characters anyway.
ltl2tgba --det 'Ga | Gb | Gc' -d'<5' | grep -v '>' >out
diff out expected3

568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
# Let's pretend that this is some used supplied input, as discussed in
# the comments of https://github.com/adl/hoaf/issues/39

cat >input <<EOF
HOA: v1
States: 7
Start: 1
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc
--BODY--
State: 1
[!0&1] 0
[!0&!1] 4
State: 3
[!0&!1] 2
State: 4
[0&1] 6
[0&1] 5
[0&1] 2
[!0&1] 3
State: 6
[!0&!1] 1
[!0&!1] 3
[0&1] 7
--END--
EOF

# autfilt should complain about the input (we only check the exit
# status here, because the actual error messages are tested in
599
# parseaut.test) and produce a valid output with the number of states
600
# fixed, and the missing state definitions.
601
autfilt -H input >output1 && exit 1
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634

cat >expect1 <<EOF
HOA: v1
States: 8
Start: 1
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
State: 1
[!0&1] 0
[!0&!1] 4
State: 2
State: 3
[!0&!1] 2
State: 4
[0&1] 6
[0&1] 5
[0&1] 2
[!0&1] 3
State: 5
State: 6
[!0&!1] 1
[!0&!1] 3
[0&1] 7
State: 7
--END--
EOF

diff output1 expect1
# Make sure the output is valid.
635
autfilt -H output1 > output1b
636
637
638
639
640
diff output1 output1b

# Here is the scenario where the undefined states are actually states
# we wanted to remove.  So we tell autfilt to fix the automaton using
# --remove-dead-states
641
SPOT_DEFAULT_FORMAT=hoa autfilt --remove-dead input >output2 && exit 1
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662

cat >expect2 <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0&!1] 1
State: 1
[0&1] 2
State: 2
[!0&!1] 0
--END--
EOF

diff output2 expect2

663
SPOT_DEFAULT_FORMAT=hoa=k autfilt expect2 >output2b
664

665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
cat >expect2b <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
properties: state-labels explicit-labels state-acc deterministic
--BODY--
State: [!0&!1] 0
1
State: [0&1] 1
2
State: [!0&!1] 2
0
--END--
EOF

diff output2b expect2b
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708

# Check the difference between --remove-unreach and --remove-dead
cat >input <<EOF
HOA: v1
States: 6
Start: 0
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
--BODY--
State: 0
[!0&!1] 1
State: 1
[0&1] 2
State: 2
[!0&!1] 0
[t] 5
State: 3
[t] 4
State: 4
[t] 3
State: 5
--END--
EOF

709
710
autfilt -H --remove-unreach input >output3
autfilt -H --remove-dead input >>output3
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747

cat >expect3 <<EOF
HOA: v1
States: 4
Start: 0
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[!0&!1] 1
State: 1
[0&1] 2
State: 2
[!0&!1] 0
[t] 3
State: 3
--END--
HOA: v1
States: 3
Start: 0
AP: 2 "p0" "p1"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0&!1] 1
State: 1
[0&1] 2
State: 2
[!0&!1] 0
--END--
EOF

diff output3 expect3
748
749


750
autfilt -Hz input 2>stderr && exit 1
751
grep 'print_hoa.*z' stderr
752
753
754
755
756
757
758
759
760
761
762
763
764
765

cat >input4 <<EOF
HOA: v1
States: 3
Start: 0
AP: 2 "a" "b"
Acceptance: 2 Inf(0) & Inf(1)
--BODY--
State: 0 {0}   [0] 1
State: 1 {1}   [1] 2
State: 2 {0 1} [0] 2
--END--
EOF

766
767
768
test `autfilt --is-weak -c input4` = 1
test `autfilt --is-inherently-weak -c input4` = 1
test `autfilt --is-terminal -c input4` = 0
769

770
771
772
autfilt -H --small --high input4 >output4
autfilt -H --small input4 >output4b
autfilt -H --high input4 >output4c
773
774
775
776
777
778
779
780
781
cat output4

cat >expect4<<EOF
HOA: v1
States: 3
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
782
properties: trans-labels explicit-labels state-acc deterministic weak
783
784
785
786
787
788
789
790
791
792
793
--BODY--
State: 0
[1] 2
State: 1
[0] 0
State: 2 {0}
[0] 2
--END--
EOF

diff output4 expect4
794
795
diff output4b expect4
diff output4c expect4
796

797
798
799
autfilt -Hv --small input4 >output5
test `autfilt --is-weak -c output4` = 1
test `autfilt --is-terminal -c output4` = 0
800
801

sed 's/\[0\]/[t]/g' expect4 > output4d
802
test `autfilt --is-terminal -c output4d` = 1
803

804
805
806
807
808
809
810
811

cat >expect5<<EOF
HOA: v1
States: 3
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
812
813
properties: trans-labels explicit-labels state-acc deterministic
properties: no-univ-branch unambiguous semi-deterministic weak
814
properties: inherently-weak
815
816
817
818
819
820
821
822
823
824
--BODY--
State: 0
[1] 2
State: 1
[0] 0
State: 2 {0}
[0] 2
--END--
EOF
diff output5 expect5
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848

cat >input6 <<EOF
HOA: v1
States: 3
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: no-univ-branch trans-labels explicit-labels state-acc
--BODY--
State: 0
[1] 2
[1] 1
[1] 1
State: 1
[0] 0
[0] 1
State: 2 {0}
[0] 2
[0] 0
[0] 1
--END--
EOF

849
run 0 autfilt -Hk input6 >output6
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
cat >expect6 <<EOF
HOA: v1
States: 3
Start: 1
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: state-labels explicit-labels state-acc
--BODY--
State: [1] 0
2 1 1
State: [0] 1
0 1
State: [0] 2 {0}
2 0 1
--END--
EOF

diff output6 expect6
869

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
run 0 autfilt -dk input6 >output6d
cat >expect6d <<EOF
digraph G {
  rankdir=LR
  I [label="", style=invis, width=0]
  I -> 1
  0 [label="0\nb"]
  0 -> 2 [label=""]
  0 -> 1 [label=""]
  0 -> 1 [label=""]
  1 [label="1\na"]
  1 -> 0 [label=""]
  1 -> 1 [label=""]
  2 [label="2\na", peripheries=2]
  2 -> 2 [label=""]
  2 -> 0 [label=""]
  2 -> 1 [label=""]
}
EOF
diff output6d expect6d

run 0 autfilt -dbark input6 >output6d2
cat >expect6d2 <<EOF
digraph G {
  rankdir=LR
895
  label=<Inf(<font color="#1F78B4"></font>)<br/>[Büchi]>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
896
897
898
899
900
901
902
903
904
905
  labelloc="t"
  I [label="", style=invis, width=0]
  I -> 1
  0 [label=<0<br/>b>]
  0 -> 2 [label=<>]
  0 -> 1 [label=<>]
  0 -> 1 [label=<>]
  1 [label=<1<br/>a>]
  1 -> 0 [label=<>]
  1 -> 1 [label=<>]
906
  2 [label=<2<br/><font color="#1F78B4"></font><br/>a>]
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
907
908
909
910
911
912
  2 -> 2 [label=<>]
  2 -> 0 [label=<>]
  2 -> 1 [label=<>]
}
EOF
diff output6d2 expect6d2
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929

cat >input7 <<EOF
HOA: v1
States: 3
Start: 1
AP: 0
acc-name: Buchi
Acceptance: 2 Inf(0) & Inf(1)
--BODY--
State: 0
[t] 1 {0}
[t] 0 {0 1}
State: 1
[t] 0 {1}
[t] 1 {0 1}
--END--
EOF
930
931
test `autfilt -c --is-inherently-weak input7` = 1
test `autfilt -c --is-weak input7` = 0
932
test `autfilt -c --is-stutter-invariant input7` = 1
933
autfilt --check input7 -H >output7
934
935
936
937
938
939
940
cat >expected7 <<EOF
HOA: v1
States: 3
Start: 1
AP: 0
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
941
942
properties: trans-labels explicit-labels trans-acc stutter-invariant
properties: inherently-weak
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
--BODY--
State: 0
[t] 1 {0}
[t] 0 {0 1}
State: 1
[t] 0 {1}
[t] 1 {0 1}
State: 2
--END--
EOF
diff output7 expected7

cat >input8 <<EOF
HOA: v1
States: 3
Start: 1
AP: 0
acc-name: Buchi
Acceptance: 2 Inf(0) & Inf(1)
--BODY--
State: 0
[t] 1 {0}
[t] 0 {0 1}
State: 1
[t] 0 {1}
[t] 1 {0}
--END--
EOF
971
972
test `autfilt -c --is-inherently-weak input8` = 0
test `autfilt -c --is-weak input8` = 0
973

974
975
976
977
978
979
980
981
982
983
984
autfilt input8 -Hl >oneline.hoa
autfilt input8 --stats='%h' >oneline2.hoa
autfilt input8 --stats='%H' >oneline3.hoa
autfilt input8 --randomize --stats='%h' >oneline4.hoa
autfilt input8 --randomize --stats='%H' >oneline5.hoa
diff oneline.hoa oneline2.hoa
diff oneline.hoa oneline3.hoa
diff oneline.hoa oneline4.hoa && exit 1
diff oneline.hoa oneline5.hoa


985
986
987
988
989
990
991
992
993
994
cat >input9 <<EOF
HOA: v1
name: "a U (b U c)"
States: 3
Start: 2
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant terminal
995
spot.highlight.edges: 3 0 1 1 4 3 2 2
996
997
spot.highlight.states: 0 0 2 3
--BODY--
998
999
1000
State: 1  /* Defined before State 0 on purpose */
[2] 0     /* because it affects the edge numbering */
[1&!2] 1  /* used in spot.highlight.edges */
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
State: 0 {0}
[t] 0
State: 2
[2] 0
[!0&1&!2] 1
[0&!2] 2
--END--
EOF
autfilt -d input9 > output9
cat >expected9 <<EOF
digraph G {
  rankdir=LR
  node [shape="circle"]
  I [label="", style=invis, width=0]
  I -> 2
1016
1017
  0 [label="0", peripheries=2, style="bold", color="#1F78B4"]
  0 -> 0 [label="1", style=bold, color="#1F78B4"]
1018
  1 [label="1"]
1019
1020
1021
1022
  1 -> 0 [label="c", style=bold, color="#FF4DA0"]
  1 -> 1 [label="b & !c", style=bold, color="#FF7F00"]
  2 [label="2", style="bold", color="#6A3D9A"]
  2 -> 0 [label="c", style=bold, color="#6A3D9A"]
1023
1024
1025
1026
1027
  2 -> 1 [label="!a & b & !c"]
  2 -> 2 [label="a & !c"]
}
EOF
diff output9 expected9
1028

1029
1030
1031
1032
1033
1034
1035
1036
# spot.hightlight.edges and spot.hightlight.states are not valid HOA
# v1 output, so they should only but output for HOA 1.1
autfilt input9 -H1 | autfilt -H1  | grep highlight && exit 1
autfilt input9 -H1 | autfilt -H1.1 | grep highlight && exit 1
autfilt -H1.1 input9 | autfilt -H1.1 | grep highlight
autfilt -H1.1 input9 | autfilt -d > output9b
diff output9 output9b

1037
test 2 = `ltl2tgba 'GFa' 'a U b' 'a U b U c'| autfilt --ap=2..3 --count`
1038
1039
1040
1041
1042

# reading CSV with embedded automata
test 2 = `genltl --dac=1..3 | ltl2tgba --stats='%e,"%h",%s' |
          dstar2tgba -F-/2 --stats='%<,%>,"%h"' |
          autfilt --states=2..3 -F-/3 --stats='%<,"%h"' | wc -l`
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065

# --dot=d
ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=d | grep ' (' >out
cat >expected <<EOF
  0 [label="0 (0)", peripheries=2]
  1 [label="1 (0)"]
  2 [label="2 (1)"]
  3 [label="3 (2)", peripheries=2]
  4 [label="4 (2)"]
EOF
diff out expected
# --dot=d should also not use circles
ltl2tgba 'a U b' | autfilt --remove-ap=b=0 --dot=d >out
cat >expected <<EOF
digraph G {
  rankdir=LR
  I [label="", style=invis, width=0]
  I -> 0
  0 [label="0 (1)"]
  0 -> 0 [label="a"]
}
EOF
diff out expected