alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

parseaut: better error recovery for dstar automata

Browse source 
* src/parseaut/parseaut.yy: Here.
* src/tests/parseaut.test: More tests.
This commit is contained in:
Alexandre Duret-Lutz 2015-09-08 00:51:04 +02:00
parent 17a18f2890
commit 3b72826e6d
2 changed files with 66 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/parseaut/parseaut.yy
View file

@ -261,6 +261,12 @@
aut: aut-1 { res.h->loc = @$; YYACCEPT; }
| ENDOFFILE { YYABORT; }
| error ENDOFFILE { YYABORT; }
| error aut-1
{
error(@1, "leading garbage was ignored");
res.h->loc = @2;
YYACCEPT;
}
aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; }
| never { res.h->type = spot::parsed_aut_type::NeverClaim; }
@ -272,7 +278,7 @@ aut-1: hoa { res.h->type = spot::parsed_aut_type::HOA; }
/**********************************************************************/
hoa: header "--BODY--" body "--END--"
hoa: error "--END--"
| "HOA:" error "--END--"
string_opt: { $$ = nullptr; }
| STRING { $$ = $1; }
@ -420,10 +426,6 @@ version: IDENTIFIER
}
format-version: "HOA:" { res.h->loc = @1; } version
| error "HOA:"
{ error(@1, "ignoring leading garbage");
res.h->loc = @2; }
version
aps: "AP:" INT {
if (res.ignore_more_ap)
@ -1102,7 +1104,11 @@ incorrectly-labeled-edge: trans-label unlabeled-edge
/* Rules for LTL2DSTAR's format */
/**********************************************************************/
dstar: dstar_header "---" dstar_states ENDDSTAR
dstar: dstar_type "v2" "explicit" dstar_header "---" dstar_states ENDDSTAR
| dstar_type error ENDDSTAR
{
error(@$, "failed to parse this as an ltl2dstar automaton");
}
dstar_type: "DRA"
{
@ -1117,27 +1123,27 @@ dstar_type: "DRA"
res.minus = 1;
}
dstar_header: dstar_type "v2" "explicit" dstar_sizes
dstar_header: dstar_sizes
{
bool err = false;
if (res.states < 0)
{
error(@4, "missing state count");
error(@1, "missing state count");
err = true;
}
if (!res.ignore_more_acc)
{
error(@4, "missing acceptance-pair count");
error(@1, "missing acceptance-pair count");
err = true;
}
if (res.start.empty())
{
error(@4, "missing start-state number");
error(@1, "missing start-state number");
err = true;
}
if (!res.ignore_more_ap)
{
error(@4, "missing atomic proposition definition");
error(@1, "missing atomic proposition definition");
err = true;
}
if (err)
@ -1155,11 +1161,7 @@ dstar_header: dstar_type "v2" "explicit" dstar_sizes
}
dstar_sizes:
/* | dstar_sizes error eols
{
error(@2, "unknown header ignored");
}
*/
| dstar_sizes error
| dstar_sizes "Acceptance-Pairs:" INT
{
if (res.ignore_more_acc)
@ -1260,6 +1262,7 @@ dstar_transitions:
}
dstar_states:
| dstar_states error
| dstar_states dstar_state_id dstar_state_accsig dstar_transitions
{
for (auto i: res.dest_map)

48
src/tests/parseaut.test
View file

@ -962,6 +962,48 @@ State: 1
this is complete garbage!
--END--
and even more garbage
DRA v2 explicit
Comment: "Safra[NBA=2]"
States: 2
garbage /* <<--- */
Acceptance-Pairs: 1
Start: 0
AP: 1 "a"
---
State: 0
Acc-Sig:
0
1
State: 1
Acc-Sig: +0
0
1
more garbage
DRA v2 explicit
Comment: "Safra[NBA=2]"
States: 2
Acceptance-Pairs: 1
Start: 0
AP: 1 "a"
---
State: 0
Acc-Sig:
0
1
State: 1
Acc-Sig: +0
0
1
HOA: v1
States: 1
Start: 0
AP: 0
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[t] 0
--END--
garbage
EOF
se='syntax error, unexpected' # this is just to keep lines short
@ -972,10 +1014,14 @@ 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
input:25.1-12: ignoring leading garbage
input:32.1-5: $se header name, expecting --END-- or State:
input:28.1-8: initial state 0 has no definition
input:25.1-12: leading garbage was ignored
input:37.1: $se 't'
input:43.1: $se \$undefined
input:56.1: $se \$undefined, expecting State: or end of DSTAR automaton
input:37.1-39.21: leading garbage was ignored
input:81.1: $se \$undefined
autfilt: failed to read automaton from input
EOF