c6110a884c
Report from Tomáš Babiak. * src/hoaparse/hoaparse.yy: Here. * src/tgbatest/hoaparse.test: Add example from a development version of ltl3ba.
1212 lines
24 KiB
Bash
Executable file
1212 lines
24 KiB
Bash
Executable file
#!/bin/sh
|
|
# -*- coding: utf-8 -*-
|
|
# Copyright (C) 2014, 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
|
|
|
|
expecterr()
|
|
{
|
|
cat >$1.exp
|
|
../../bin/autfilt --hoa "$@" 2>$1.err >$1.out && exit 1
|
|
test $? = 2
|
|
cat $1.err
|
|
diff $1.err $1.exp
|
|
}
|
|
|
|
expectok()
|
|
{
|
|
cat >$1.exp
|
|
../../bin/autfilt --hoa "$@" >$1.out
|
|
test $? = 0
|
|
cat $1.out
|
|
diff $1.out $1.exp
|
|
}
|
|
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 1 "a"
|
|
States: 2
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[0] 1
|
|
State: 1 {0}
|
|
[t] 1
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:5.1-9: redefinition of the number of states...
|
|
input:2.1-9: ... previously defined here.
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 1 "a"
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[0] 1
|
|
State: 1 {0}
|
|
[t] 1
|
|
--END--
|
|
2 1t
|
|
2 1
|
|
1 -1 "b"
|
|
0 -1 & "a" ! "b"
|
|
-1
|
|
1 0
|
|
2 0 -1 t
|
|
-1
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:8.5: state number is larger than state count...
|
|
input:2.1-9: ... declared here.
|
|
input:9.8: state number is larger than state count...
|
|
input:2.1-9: ... declared here.
|
|
input:10.5: state number is larger than state count...
|
|
input:2.1-9: ... declared here.
|
|
input:13.1: state number is larger than state count...
|
|
input:12.1: ... declared here.
|
|
input:18.1: state number is larger than state count...
|
|
input:12.1: ... declared here.
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 1 "a"
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[2] 0
|
|
State: 0 {0}
|
|
[t] 0
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:8.2: AP number is larger than the number of APs...
|
|
input:4.1-5: ... declared here
|
|
input:9.1-8: redeclaration of state 0
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 0
|
|
AP: 1 "a" "b"
|
|
Acceptance: 0 t
|
|
--BODY--
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:3.1-13: found 2 atomic propositions instead of the 1 announced
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
AP: 1 "a"
|
|
States: 0
|
|
AP: 2 "a" "b"
|
|
Acceptance: 0 t
|
|
--BODY--
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:4.1-3: ignoring this redeclaration of APs...
|
|
input:2.1-5: ... previously declared here.
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
AP: 1 "a"
|
|
States: 0
|
|
Start: 1
|
|
--BODY--
|
|
State: 0 {0 1}
|
|
[0] 0 {0}
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:4.1-8: initial state number is larger than state count...
|
|
input:3.1-9: ... declared here.
|
|
input:1.1-4.8: missing 'Acceptance:' header
|
|
input:6.8: state number is larger than state count...
|
|
input:3.1-9: ... declared here.
|
|
input:6.10-14: ignoring acceptance sets because of missing acceptance condition
|
|
input:7.5: state number is larger than state count...
|
|
input:3.1-9: ... declared here.
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
AP: 1 "a"
|
|
Start: 1
|
|
States: 1
|
|
--BODY--
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:3.1-8: initial state number is larger than state count...
|
|
input:4.1-9: ... declared here.
|
|
input:1.1-4.9: missing 'Acceptance:' header
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
Acceptance: 1 Inf(0)
|
|
Start: 0
|
|
States: 1
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:5.1-13: ignoring this redefinition of the acceptance condition...
|
|
input:2.1-13: ... previously defined here.
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
Start: 0
|
|
AP: 1 "a"
|
|
States: 2
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[0] 1
|
|
State: 1 {1}
|
|
[t] 1
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:9.11: number is larger than the count of acceptance sets...
|
|
input:5.1-13: ... declared here.
|
|
EOF
|
|
|
|
# Let's have two broken automata in a row...
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
Start: 0
|
|
AP: 1 "a"
|
|
States: 2
|
|
Acceptance: 1 Inf(2)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[0] 1
|
|
State: 1 {0}
|
|
[t] 1
|
|
--END--
|
|
HOA: v2
|
|
--BODY--
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:5.19: number is larger than the count of acceptance sets...
|
|
input:5.1-13: ... declared here.
|
|
input:12.6-7: unsupported version of the HOA format
|
|
input:12.1-7: missing 'Acceptance:' header
|
|
EOF
|
|
|
|
cat >input<<EOF
|
|
HOA: v1
|
|
States: 3
|
|
Start: 0
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
AP: 2 "a" "b"
|
|
--BODY--
|
|
State: 0 "foo" { 0 }
|
|
2 /* !a & !b */
|
|
0 /* a & !b */
|
|
1 /* !a & b */
|
|
1 /* a & b */
|
|
State: 1 { 1 }
|
|
1 1 1 1 /* four transitions on one line */
|
|
State: 2 "sink state" { 0 }
|
|
2 2 2 2
|
|
--END--
|
|
EOF
|
|
|
|
expectok input <<EOF
|
|
HOA: v1
|
|
States: 3
|
|
Start: 0
|
|
AP: 2 "a" "b"
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 Inf(0)&Inf(1)
|
|
properties: trans-labels explicit-labels state-acc complete deterministic
|
|
--BODY--
|
|
State: 0 {0}
|
|
[!0&!1] 2
|
|
[0&!1] 0
|
|
[!0&1] 1
|
|
[0&1] 1
|
|
State: 1 {1}
|
|
[!0&!1] 1
|
|
[0&!1] 1
|
|
[!0&1] 1
|
|
[0&1] 1
|
|
State: 2 {0}
|
|
[!0&!1] 2
|
|
[0&!1] 2
|
|
[!0&1] 2
|
|
[0&1] 2
|
|
--END--
|
|
EOF
|
|
|
|
cat >input<<EOF
|
|
HOA: v1
|
|
States: 3
|
|
Start: 0
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
AP: 2 "a" "b"
|
|
properties: state-labels complete
|
|
--BODY--
|
|
State: 0 "foo" { 0 }
|
|
2 /* !a & !b */
|
|
0 /* a & !b */
|
|
1 /* !a & b */
|
|
/* missing transition */
|
|
State: 1 { 1 }
|
|
1 1 1 1 /* four transitions on one line */
|
|
State: 2 "sink state" { 0 }
|
|
2 2 2 2
|
|
--END--
|
|
HOA: v1
|
|
States: 3
|
|
Start: 0
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
AP: 2 "a" "b"
|
|
properties: implicit-labels complete
|
|
--BODY--
|
|
State: [t] 0 "foo" { 0 }
|
|
2 /* !a & !b */
|
|
0 /* a & !b */
|
|
1 /* !a & b */
|
|
0 /* a & b */
|
|
State: 1 { 1 }
|
|
1 1 1 1 /* four transitions on one line */
|
|
State: 2 "sink state" { 0 }
|
|
2 2 2 2
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:9.5-12.7: not enough transitions for this state
|
|
input:10.7-12.7: these transitions have implicit labels but the automaton is...
|
|
input:7.17-28: ... declared with 'property: state-labels'
|
|
input:9.5-12.7: automaton is not complete...
|
|
input:7.30-37: ... despite 'property: complete'
|
|
input:27.8-10: state label used although the automaton was...
|
|
input:25.13-27: ... declared with 'property: implicit-labels' here
|
|
EOF
|
|
|
|
cat >input<<EOF
|
|
HOA: v1
|
|
tool: "test"
|
|
States: 3
|
|
Start: 0
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
properties: implicit-labels explicit-labels /* ? */ complete
|
|
AP: 2 "a" "b"
|
|
--BODY--
|
|
State: 0 "foo" { 0 }
|
|
2 /* !a & !b */
|
|
0 /* a & !b */
|
|
1 /* !a & b */
|
|
1 /* a & b */
|
|
2 /* extra transition ! */
|
|
State: 1 { 1 }
|
|
1 1 1 1 /* four transitions on one line */
|
|
State: 2 "sink state" { 0 }
|
|
2 2 2 2
|
|
--END--
|
|
HOA: v1
|
|
tool: "test"
|
|
States: 3
|
|
Start: 0
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
properties: implicit-labels state-labels /* ? */
|
|
AP: 2 "a" "b"
|
|
--BODY--
|
|
State: 0 "foo" { 0 }
|
|
2 /* !a & !b */
|
|
0 /* a & !b */
|
|
1 /* !a & b */
|
|
1 /* a & b */
|
|
State: 1 { 1 }
|
|
1 1 1 1 /* four transitions on one line */
|
|
State: 2 "sink state" { 0 }
|
|
2 2 2 2
|
|
--END--
|
|
HOA: v1
|
|
tool: "test"
|
|
States: 3
|
|
Start: 0
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
properties: implicit-labels
|
|
AP: 2 "a" "b"
|
|
--BODY--
|
|
State: 0 "foo" { 0 }
|
|
2 /* !a & !b */
|
|
0 /* a & !b */
|
|
1 /* !a & b */
|
|
1 /* a & b */
|
|
State: 1 { 1 }
|
|
1 1 1 1 /* four transitions on one line */
|
|
State: 2 "sink state" { 0 }
|
|
[t] 2
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:7.17-31: 'property: implicit-labels' is incompatible with...
|
|
input:7.33-47: ... 'property: explicit-labels'.
|
|
input:15.7: too many transition for this state, ignoring this one
|
|
input:27.33-44: 'property: state-labels' is incompatible with...
|
|
input:27.17-31: ... 'property: implicit-labels'.
|
|
input:57.7-9: transition label used although the automaton was...
|
|
input:46.17-31: ... declared with 'property: implicit-labels' here
|
|
EOF
|
|
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
name: "GFa & GF(b & c)"
|
|
States: 1
|
|
Start: 0
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
AP: 3 "a" "b" "c"
|
|
Alias: @a 0
|
|
Alias: @a 1 & 2 /* should be @bc */
|
|
properties: state-labels /* this is bogus */
|
|
--BODY--
|
|
State: 0
|
|
[!@a & !@bc] 0
|
|
[@a & !@bc] 0 {0}
|
|
[!@a & @bc] 0 {1}
|
|
[@a & @bc] 0 {0 1}
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:9.5-19: ignoring redefinition of alias @a
|
|
input:13.13-15: unknown alias @bc
|
|
input:13.5-16: transition label used although the automaton was...
|
|
input:10.17-28: ... declared with 'property: state-labels' here
|
|
input:14.12-14: unknown alias @bc
|
|
input:15.12-14: unknown alias @bc
|
|
input:16.11-13: unknown alias @bc
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
name: "GFa & GF(b & c)"
|
|
States: 1
|
|
Start: 0
|
|
acc-name: who cares
|
|
Acceptance: 2 (Inf(0) & Inf(1))
|
|
AP: 3 "a" "b" "c"
|
|
Alias: @a 0
|
|
Alias: @bc 1 & 2
|
|
--BODY--
|
|
State: 0
|
|
[!@a & !@bc] 0
|
|
[@a & !@bc] 0 {0}
|
|
[!@a & @bc] 0 {1}
|
|
[@a & @bc] 0 {0 1}
|
|
--END--
|
|
/* Some comment */
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
Acceptance: 0 t
|
|
AP: 1 "a"
|
|
--BODY--
|
|
State: [0] 0 1
|
|
State: [0] 1 1
|
|
--END--
|
|
EOF
|
|
|
|
expectok input <<EOF
|
|
HOA: v1
|
|
name: "GFa & GF(b & c)"
|
|
States: 1
|
|
Start: 0
|
|
AP: 3 "a" "b" "c"
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 Inf(0)&Inf(1)
|
|
properties: trans-labels explicit-labels trans-acc complete deterministic
|
|
--BODY--
|
|
State: 0
|
|
[!0&!1 | !0&!2] 0
|
|
[0&!1 | 0&!2] 0 {0}
|
|
[!0&1&2] 0 {1}
|
|
[0&1&2] 0 {0 1}
|
|
--END--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 1 "a"
|
|
acc-name: all
|
|
Acceptance: 0 t
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
--BODY--
|
|
State: 0
|
|
[0] 1
|
|
State: 1
|
|
[0] 1
|
|
--END--
|
|
EOF
|
|
|
|
expectok input --stats='%F:%L' <<EOF
|
|
input:1.5-16.11
|
|
input:18.1-26.7
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
--ABORT--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
Acceptance: 2 (Inf(0) & Inf(!0)) &
|
|
--ABORT----ABORT--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
Acceptance: 2 (Inf(0) & Inf(!0)) & Inf(!1)
|
|
AP: 1 "a"
|
|
--BODY-- State: 0 {0
|
|
}
|
|
[0] 1
|
|
[!0--ABORT--
|
|
HOA: v1
|
|
States: 2
|
|
name: "survivor"
|
|
Start: 0
|
|
Acceptance: 2 (Inf(0) & Inf(!0)) & Inf(!1)
|
|
AP: 1 "a"
|
|
--BODY--
|
|
State: 0 {0}
|
|
[0] 1
|
|
[!0] 0 {1}
|
|
State: 1
|
|
[!0] 1
|
|
[0] 0
|
|
[f] 0
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:1.1-2.9: aborted input automaton
|
|
input:3.1-7.14: aborted input automaton
|
|
input:7.15-23: aborted input automaton
|
|
input:8.1-16.12: aborted input automaton
|
|
EOF
|
|
|
|
# DOS-style new lines should have the same output.
|
|
perl -pi -e 's/$/\r/' input
|
|
../../bin/autfilt --hoa input 2>stderr && exit 1
|
|
cat stderr
|
|
diff stderr input.exp
|
|
|
|
cat >expected <<EOF
|
|
HOA: v1
|
|
name: "survivor"
|
|
States: 2
|
|
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 complete deterministic
|
|
--BODY--
|
|
State: 0
|
|
[0] 1 {0 1}
|
|
[!0] 0 {0}
|
|
State: 1
|
|
[!0] 1 {1 2}
|
|
[0] 0 {1 2}
|
|
--END--
|
|
EOF
|
|
|
|
diff expected input.out
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
Start: 1
|
|
AP: 2 "a" "\"b\""
|
|
Acceptance: 1 Inf(0)
|
|
properties: deterministic
|
|
--BODY--
|
|
State: 0 {0}
|
|
[1] 1
|
|
[!1] 0
|
|
State: 1
|
|
[!0] 1
|
|
[0] 0
|
|
--END--
|
|
HOA: v1
|
|
States: 0
|
|
AP: 0
|
|
Acceptance: 1 Inf(0)
|
|
properties: complete
|
|
--BODY--
|
|
--END--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 2 "a" "\"b\""
|
|
Acceptance: 1 Inf(0)
|
|
properties: deterministic
|
|
--BODY--
|
|
State: 0 {0}
|
|
[1] 1
|
|
[!1] 0
|
|
State: 1
|
|
[!0] 1
|
|
[!0] 0
|
|
--END--
|
|
EOF
|
|
expecterr input <<EOF
|
|
input:7.13-25: deterministic automata should have at most one initial state
|
|
input:20.13-20: complete automata should have at least one initial state
|
|
input:33.1-35.6: automaton is not deterministic...
|
|
input:28.13-25: ... despite 'property: deterministic'
|
|
EOF
|
|
|
|
# Mix HOA with neverclaims and LBTT automata
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
Start: 1
|
|
Start: 0 /* duplicate */
|
|
AP: 2 "a" "\"b\""
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[1] 1
|
|
[!1] 0
|
|
State: 1
|
|
[!0] 1
|
|
[0] 0
|
|
--END--
|
|
|
|
/* some LBTT with mixed state/transition acceptance,
|
|
just because we can */
|
|
4 2ts
|
|
0 1 -1
|
|
1 -1 "c"
|
|
2 -1 & "b" ! "c"
|
|
3 -1 ! "c"
|
|
-1
|
|
1 0 1 -1
|
|
1 0 -1 t
|
|
-1
|
|
2 0 -1
|
|
1 -1 "c"
|
|
2 -1 & "b" ! "c"
|
|
-1
|
|
3 0 -1
|
|
3 0 1 -1 & "a" "b"
|
|
3 1 -1 & "a" ! "b"
|
|
3 0 -1 & ! "a" "b"
|
|
3 -1 & ! "a" ! "b"
|
|
-1
|
|
|
|
|
|
never { /* a U b */
|
|
T0_init:
|
|
if
|
|
:: ((b)) -> goto accept_all
|
|
:: ((a)) -> goto T0_init
|
|
fi;
|
|
accept_all:
|
|
skip
|
|
}
|
|
|
|
|
|
never {
|
|
start: if :: false -> goto T0 fi;
|
|
T0: false
|
|
}
|
|
EOF
|
|
|
|
expectok input <<EOF
|
|
HOA: v1
|
|
States: 3
|
|
Start: 2
|
|
AP: 2 "a" "\"b\""
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels state-acc complete
|
|
--BODY--
|
|
State: 0 {0}
|
|
[1] 1
|
|
[!1] 0
|
|
State: 1
|
|
[!0] 1
|
|
[0] 0
|
|
State: 2
|
|
[1] 1
|
|
[!1] 0
|
|
[!0] 1
|
|
[0] 0
|
|
--END--
|
|
HOA: v1
|
|
States: 4
|
|
Start: 0
|
|
AP: 3 "c" "b" "a"
|
|
acc-name: generalized-Buchi 2
|
|
Acceptance: 2 Inf(0)&Inf(1)
|
|
properties: trans-labels explicit-labels trans-acc
|
|
--BODY--
|
|
State: 0
|
|
[0] 1
|
|
[!0&1] 2
|
|
[!0] 3
|
|
State: 1
|
|
[t] 1 {0 1}
|
|
State: 2
|
|
[0] 1
|
|
[!0&1] 2
|
|
State: 3
|
|
[1&2] 3 {0 1}
|
|
[!1&2] 3 {0}
|
|
[1&!2] 3 {1}
|
|
[!1&!2] 3
|
|
--END--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 2 "b" "a"
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels state-acc
|
|
--BODY--
|
|
State: 0
|
|
[0] 1
|
|
[1] 0
|
|
State: 1 {0}
|
|
[t] 1
|
|
--END--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
--BODY--
|
|
State: 0
|
|
[f] 1
|
|
State: 1
|
|
--END--
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
Start: 0 /* duplicate */
|
|
AP: 2 "a" "b"
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[1] 1
|
|
[!1] 0 /* nested /* comment */ */
|
|
State: 1
|
|
[!0] 1
|
|
[0] 0
|
|
--END--
|
|
EOF
|
|
|
|
expectok input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 2 "a" "b"
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels state-acc complete deterministic
|
|
--BODY--
|
|
State: 0 {0}
|
|
[1] 1
|
|
[!1] 0
|
|
State: 1
|
|
[!0] 1
|
|
[0] 0
|
|
--END--
|
|
EOF
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 3
|
|
Start: 0
|
|
AP: 2 "a" "b"/* multi
|
|
line
|
|
comment */
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: [1] 0 {0}
|
|
[!1] 0
|
|
1
|
|
State: 1
|
|
[!0] 1
|
|
2
|
|
State: 2
|
|
1
|
|
[t] 2
|
|
1 2
|
|
--END--
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 2 "a" "b"
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels /* this is bogus */
|
|
--BODY--
|
|
State: [1] 0 {0} 0
|
|
--END--
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 2 "a" "b"
|
|
Acceptance: 1 Inf(0)
|
|
properties: state-labels trans-labels /* this is bogus */
|
|
--BODY--
|
|
State: [1] 0 {0} 0
|
|
--END--
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 2 "a" "b"
|
|
Acceptance: 1 Inf(0)
|
|
properties: state-labels /* OK */
|
|
--BODY--
|
|
State: [1] 0 {0} 0
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:10.1-4: cannot label this edge because...
|
|
input:9.8-10: ... the state is already labeled.
|
|
input:14.6: missing label for this edge (previous edge is labeled)
|
|
input:17.1-3: ignoring this label, because previous edge has no label
|
|
input:27.8-10: state label used although the automaton was...
|
|
input:25.13-24: ... declared with 'property: trans-labels' here
|
|
input:34.26-37: 'property: trans-labels' is incompatible with...
|
|
input:34.13-24: ... 'property: state-labels'.
|
|
EOF
|
|
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: /* multi-line
|
|
comment
|
|
*/2
|
|
Start: 0
|
|
Important: 4 very important "with multi-line
|
|
string!"
|
|
AP: 0
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0} 1
|
|
State: 1 0
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:6.1-7.8: ignoring unsupported header "Important:"
|
|
(but the capital indicates information that should not be ignored)
|
|
EOF
|
|
|
|
cat >expected <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels state-acc complete deterministic
|
|
--BODY--
|
|
State: 0 {0}
|
|
[t] 1
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
EOF
|
|
|
|
diff expected input.out
|
|
|
|
# DOS-style new lines should have the same output.
|
|
perl -pe -e 's/$/\r/' input
|
|
../../bin/autfilt --hoa input 2>stderr && exit 1
|
|
cat stderr
|
|
diff stderr input.exp
|
|
diff expected input.out
|
|
|
|
# Error recovery
|
|
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {a} /* not a digit */
|
|
[t] 1
|
|
State: 1
|
|
[a] 0 /* not a digit */
|
|
--END--
|
|
HOA: v1
|
|
Acceptance: 1 Inf(0)
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
--BODY--
|
|
State: 0 {0}
|
|
[t] "f" 1 /* WTF? */
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
some garbage HOA: v1
|
|
Acceptance: 1 Inf(0)
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
--BODY--
|
|
Stat: 0 {0} /* not State: */
|
|
[t] 1
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
this is complete garbage!
|
|
--END--
|
|
and even more garbage
|
|
EOF
|
|
|
|
se='syntax error, unexpected' # this is just to keep lines short
|
|
end='end of file or HOA: or never or LBTT header'
|
|
expecterr input <<EOF
|
|
input:8.11: $se identifier, expecting integer or '}'
|
|
input:8.10-12: ignoring this invalid acceptance set
|
|
input:11.2: $se identifier
|
|
input:11.1-3: ignoring this invalid label
|
|
input:21.5-7: $se string, expecting integer
|
|
input:25.1: $se \$undefined, expecting $end
|
|
input:25.1-12: ignoring leading garbage
|
|
input:32.1-5: $se header name, expecting --END-- or State:
|
|
input:37.1: $se 't', expecting $end
|
|
autfilt: failed to read automaton from input
|
|
EOF
|
|
|
|
# A comment can contain --BODY-- or --END--, so we do not want to be
|
|
# smart about it.
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi /* unclosed comment
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[t] 1
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[t] 1
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:5.17-25.1: unclosed comment
|
|
input:5.17-25.1: syntax error, unexpected end of file
|
|
autfilt: failed to read automaton from input
|
|
EOF
|
|
|
|
# Likewise for strings
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
tool: "unterminated string
|
|
AP: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[t] 1
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[t] 1
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
EOF
|
|
|
|
expecterr input <<EOF
|
|
input:4.7-26.1: unclosed string
|
|
input:26.1: syntax error, unexpected end of file
|
|
autfilt: failed to read automaton from input
|
|
EOF
|
|
|
|
expecterr non-existant<<EOF
|
|
autfilt: Cannot open file non-existant
|
|
EOF
|
|
|
|
run 2 ../ltl2tgba -XH foob 2>output.err
|
|
grep 'foob:1.1: Cannot open file foob' output.err
|
|
|
|
# Make sure we can read multiple automata from stdin
|
|
../../bin/ltl2tgba 'a U b' 'GFa' --hoa | grep -v '^name:' > input
|
|
../../bin/autfilt --hoa < input | ../../bin/autfilt --hoa > output
|
|
diff input output
|
|
|
|
|
|
|
|
# Parse something in debug mode, to exercise the %printer
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
--BODY--
|
|
State: 0 {0}
|
|
[t] 1
|
|
State: 1
|
|
[t] 0
|
|
--END--
|
|
EOF
|
|
|
|
run 0 ../ltl2tgba -d -XH input 2> output.err
|
|
grep -- "--BODY--" output.err
|
|
grep "identifier.*v1" output.err
|
|
|
|
|
|
|
|
# This was generated by
|
|
# randaut -n 10 -Hl 3 -d 0.055 --seed=3 | fmt
|
|
cat > input <<EOF
|
|
HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance:
|
|
0 t properties: trans-labels explicit-labels state-acc deterministic
|
|
--BODY-- State: 0 [0&!1&2] 0 [0&1&2] 1 State: 1 [0&1&2] 2 State: 2
|
|
[!0&1&!2] 3 State: 3 [!0&1&!2] 4 State: 4 [!0&1&2] 1 [0&!1&!2] 5 State:
|
|
5 [!0&1&2] 6 State: 6 [!0&1&2] 7 State: 7 [0&1&2] 8 State: 8 [!0&!1&2]
|
|
9 State: 9 [0&1&2] 2 [!0&!1&!2] 6 [!0&1&!2] 1 --END-- HOA: v1 States: 10
|
|
Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance: 0 t properties:
|
|
trans-labels explicit-labels state-acc deterministic --BODY-- State: 0
|
|
[!0&1&2] 1 State: 1 [0&!1&!2] 2 State: 2 [!0&1&!2] 3 State: 3 [0&!1&2]
|
|
4 [!0&!1&!2] 5 [!0&1&!2] 6 State: 4 [!0&!1&!2] 7 [0&!1&2] 0 State: 5
|
|
[0&1&!2] 8 State: 6 [!0&1&!2] 7 State: 7 [!0&1&!2] 9 State: 8 [!0&1&2]
|
|
2 State: 9 [0&1&2] 6 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0"
|
|
"p1" "p2" acc-name: all Acceptance: 0 t properties: trans-labels
|
|
explicit-labels state-acc deterministic --BODY-- State: 0 [0&1&!2]
|
|
1 State: 1 [0&1&!2] 2 [0&!1&!2] 3 State: 2 [!0&1&!2] 1 [!0&!1&!2] 4
|
|
State: 3 [0&1&!2] 5 State: 4 [!0&1&2] 3 [!0&!1&2] 6 State: 5 [0&1&!2]
|
|
7 State: 6 [!0&!1&!2] 8 State: 7 [!0&!1&!2] 5 State: 8 [!0&!1&!2] 9
|
|
[0&1&!2] 6 State: 9 [!0&1&2] 8 [0&!1&2] 4 [!0&!1&!2] 7 --END-- HOA:
|
|
v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance:
|
|
0 t properties: trans-labels explicit-labels state-acc --BODY-- State:
|
|
0 [0&1&2] 1 State: 1 [0&1&2] 2 State: 2 [0&!1&!2] 3 [0&!1&2] 4 [0&!1&2]
|
|
0 State: 3 [!0&1&2] 1 [0&!1&2] 2 [!0&!1&2] 5 State: 4 [0&1&!2] 6 State: 5
|
|
[!0&1&!2] 7 State: 6 [0&!1&!2] 2 State: 7 [!0&!1&2] 8 State: 8 [0&!1&!2]
|
|
9 State: 9 [!0&1&!2] 7 [!0&1&!2] 6 --END-- HOA: v1 States: 10 Start: 0 AP:
|
|
3 "p0" "p1" "p2" acc-name: all Acceptance: 0 t properties: trans-labels
|
|
explicit-labels state-acc --BODY-- State: 0 [!0&!1&2] 1 State: 1 [!0&!1&2]
|
|
2 State: 2 [0&1&!2] 3 State: 3 [!0&1&!2] 4 State: 4 [!0&1&2] 5 State:
|
|
5 [0&!1&!2] 6 State: 6 [!0&!1&!2] 5 [!0&!1&!2] 7 State: 7 [!0&!1&!2] 7
|
|
[!0&!1&2] 6 [0&!1&2] 8 State: 8 [0&1&2] 8 [0&1&!2] 9 State: 9 [0&!1&2]
|
|
2 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name:
|
|
all Acceptance: 0 t properties: trans-labels explicit-labels state-acc
|
|
deterministic --BODY-- State: 0 [!0&!1&2] 1 State: 1 [0&!1&!2] 2 State: 2
|
|
[!0&!1&2] 3 State: 3 [!0&!1&!2] 4 State: 4 [!0&1&!2] 5 State: 5 [!0&1&2]
|
|
6 State: 6 [0&1&!2] 1 [!0&!1&!2] 3 [!0&1&2] 7 State: 7 [0&1&2] 8 State:
|
|
8 [0&!1&!2] 7 [0&1&!2] 9 State: 9 [0&1&2] 0 --END-- HOA: v1 States: 10
|
|
Start: 0 AP: 3 "p0" "p1" "p2" acc-name: all Acceptance: 0 t properties:
|
|
trans-labels explicit-labels state-acc deterministic --BODY-- State: 0
|
|
[0&1&!2] 1 State: 1 [!0&1&2] 2 State: 2 [0&1&2] 3 State: 3 [0&1&!2] 4
|
|
State: 4 [!0&!1&2] 5 State: 5 [!0&!1&!2] 6 State: 6 [!0&1&!2] 7 State: 7
|
|
[!0&!1&!2] 3 [!0&1&2] 8 State: 8 [0&!1&2] 9 State: 9 [!0&!1&!2] 9 [0&!1&2]
|
|
3 [!0&1&!2] 2 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2"
|
|
acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels
|
|
state-acc --BODY-- State: 0 [0&!1&!2] 1 State: 1 [!0&!1&2] 2 [0&!1&2] 3
|
|
State: 2 [0&!1&2] 4 State: 3 [0&!1&!2] 5 [0&!1&!2] 6 State: 4 [0&!1&!2] 7
|
|
[0&!1&2] 3 State: 5 [!0&!1&!2] 8 State: 6 [!0&!1&2] 4 [0&!1&2] 6 State: 7
|
|
[0&!1&2] 4 [!0&!1&!2] 1 State: 8 [!0&1&2] 6 [0&1&2] 9 State: 9 [0&1&!2]
|
|
3 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2" acc-name:
|
|
all Acceptance: 0 t properties: trans-labels explicit-labels state-acc
|
|
--BODY-- State: 0 [!0&1&2] 1 State: 1 [!0&!1&!2] 2 [!0&!1&2] 3 [!0&1&2]
|
|
4 [!0&1&2] 5 State: 2 [0&1&!2] 2 [0&!1&2] 6 State: 3 [0&1&2] 3 [0&!1&2] 7
|
|
[!0&1&2] 2 State: 4 [!0&!1&!2] 8 State: 5 [0&!1&!2] 2 [!0&!1&2] 6 State:
|
|
6 [!0&!1&2] 2 [!0&1&!2] 7 State: 7 [0&1&2] 9 State: 8 [!0&1&2] 7 State:
|
|
9 [!0&1&2] 2 --END-- HOA: v1 States: 10 Start: 0 AP: 3 "p0" "p1" "p2"
|
|
acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels
|
|
state-acc deterministic --BODY-- State: 0 [!0&!1&!2] 1 State: 1 [0&1&!2] 2
|
|
[!0&!1&!2] 3 [0&!1&2] 4 State: 2 [0&1&!2] 5 State: 3 [!0&!1&!2] 6 State:
|
|
4 [!0&!1&!2] 7 State: 5 [!0&1&2] 2 State: 6 [!0&!1&2] 8 State: 7 [0&1&2]
|
|
9 State: 8 [0&!1&!2] 7 State: 9 [!0&1&!2] 1 [0&1&!2] 7 --END--
|
|
EOF
|
|
|
|
expectok input --is-deter --stats='%F:%L: %c' <<EOF
|
|
input:1.1-6.53: 2
|
|
input:6.55-12.28: 2
|
|
input:12.30-18.62: 5
|
|
input:30.11-35.51: 1
|
|
input:35.53-41.21: 3
|
|
input:53.22-58.62: 3
|
|
EOF
|
|
|
|
expectok input -v --is-deter --stats='%F:%L: %n' <<EOF
|
|
input:18.64-24.42: 2
|
|
input:24.44-30.9: 1
|
|
input:41.23-47.9: 1
|
|
input:47.11-53.20: 1
|
|
EOF
|
|
|
|
# An example from ltl3ba
|
|
cat >input <<EOF
|
|
HOA: v1
|
|
tool: "ltl3ba" "1.1.0 - working copy"
|
|
name: "BA for GFa && GF(b&&c) && GF(d||e) || x"
|
|
States: 6
|
|
Start: 0
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
AP: 6 "a" "b" "c" "d" "e" "x"
|
|
properties: trans-labels explicit-labels state-acc no-univ-branch
|
|
--BODY--
|
|
State: 0 "T0_init"
|
|
[(5)] 5
|
|
[t] 4
|
|
[(0)] 3
|
|
[(0 & 1 & 2)] 2
|
|
[(0 & 1 & 2 & !3 & 4) | (0 & 1 & 2 & 3)] 1
|
|
State: 1 "accept_S1" {0}
|
|
[t] 4
|
|
[(0)] 3
|
|
[(0 & 1 & 2)] 2
|
|
[(0 & 1 & 2 & !3 & 4) | (0 & 1 & 2 & 3)] 1
|
|
State: 2 "T2_S1"
|
|
[t] 2
|
|
[(!3 & 4) | (3)] 1
|
|
State: 3 "T1_S1"
|
|
[t] 3
|
|
[(1 & 2)] 2
|
|
[(1 & 2 & !3 & 4) | (1 & 2 & 3)] 1
|
|
State: 4 "T0_S1"
|
|
[t] 4
|
|
[(0)] 3
|
|
[(0 & 1 & 2)] 2
|
|
[(0 & 1 & 2 & !3 & 4) | (0 & 1 & 2 & 3)] 1
|
|
State: 5 "accept_all" {0}
|
|
[t] 5
|
|
--END--
|
|
EOF
|
|
|
|
expectok input <<EOF
|
|
HOA: v1
|
|
name: "BA for GFa && GF(b&&c) && GF(d||e) || x"
|
|
States: 6
|
|
Start: 0
|
|
AP: 6 "a" "b" "c" "d" "e" "x"
|
|
acc-name: Buchi
|
|
Acceptance: 1 Inf(0)
|
|
properties: trans-labels explicit-labels state-acc complete
|
|
--BODY--
|
|
State: 0
|
|
[5] 5
|
|
[t] 4
|
|
[0] 3
|
|
[0&1&2] 2
|
|
[0&1&2&3 | 0&1&2&4] 1
|
|
State: 1 {0}
|
|
[t] 4
|
|
[0] 3
|
|
[0&1&2] 2
|
|
[0&1&2&3 | 0&1&2&4] 1
|
|
State: 2
|
|
[t] 2
|
|
[3 | 4] 1
|
|
State: 3
|
|
[t] 3
|
|
[1&2] 2
|
|
[1&2&3 | 1&2&4] 1
|
|
State: 4
|
|
[t] 4
|
|
[0] 3
|
|
[0&1&2] 2
|
|
[0&1&2&3 | 0&1&2&4] 1
|
|
State: 5 {0}
|
|
[t] 5
|
|
--END--
|
|
EOF
|