Commit e83bfd37 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

hoa: fix segfault when input has initial alternation

* src/hoaparse/hoaparse.yy: Do not check initial alternating state
number until we support alternation.
* src/tests/hoaparse.test: Add a test case.
parent a4b63e8e
......@@ -428,7 +428,7 @@ header-item: "States:" INT
}
res.states = std::max(res.states, (int) $2);
}
| "Start:" state-conj-2
| "Start:" init-state-conj-2
{
error(@2, "alternation is not yet supported");
YYABORT;
......@@ -587,6 +587,11 @@ header-spec: | header-spec BOOLEAN
state-conj-2: checked-state-num '&' checked-state-num
| state-conj-2 '&' checked-state-num
// Currently we do not check the number of these states
// since we do not support alternation.
init-state-conj-2: state-num '&' state-num
| init-state-conj-2 '&' state-num
label-expr: 't'
{
$$ = bddtrue.id();
......
......@@ -1672,3 +1672,62 @@ input:13.9: state 2 has no definition
input:17.7: state 5 has no definition
input:14.9: state 8 has no definition
EOF
# This input caused a segfault at some point.
# Not supporting alternation is not an excuse for segfaulting.
cat >input <<EOF
HOA: v1
tool: "ltl3ba" "1.1.2"
States: 12
Start: 8&6&2
Start: 8&4&2
Start: 8&6&0
Start: 8&4&0
acc-name: co-Buchi
Acceptance: 1 Fin(0)
AP: 4 "p2" "c1" "p1" "c2"
properties: trans-labels explicit-labels state-acc univ-branch very-weak
--BODY--
State: 0 "X (G(c2))"
[t] 1
State: 1 "G(c2)"
[(3)] 1
State: 2 "FG(c1)" {0}
[(1)] 3
[t] 2
State: 3 "G(c1)"
[(1)] 3
State: 4 "X (F!((c2)))"
[t] 5
State: 5 "F!((c2))" {0}
[(!3)] 11
[t] 5
State: 6 "GF!((c1))"
[(!1)] 6
[t] 7&6
State: 7 "F!((c1))" {0}
[(!1)] 11
[t] 7
State: 8 "((!((c1)) U (!((c1)) && !((p1)))) R F!((p2)))"
[(!0 & !1 & !2)] 11
[(!1 & !2)] 10
[(!0 & !1)] 9
[(!1)] 10&9
[(!0)] 8
[t] 10&8
State: 9 "(!((c1)) U (!((c1)) && !((p1))))" {0}
[(!1 & !2)] 11
[(!1)] 9
State: 10 "F!((p2))" {0}
[(!0)] 11
[t] 10
State: 11 "t"
[t] 11
--END--
EOF
expecterr input <<EOF
input:4.8-12: alternation is not yet supported
autfilt: failed to read automaton from input
EOF
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment