Commit 8c8c2f0b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

hoa: allocate the states once, after parsing the header

* src/hoaparse/hoaparse.yy: Allocate state after parsing the entire
header, not right after passing "States:".
* src/tgbatest/hoaparse.test: Reflect improved error message
about initial state.
parent 71d21b37
...@@ -126,7 +126,7 @@ ...@@ -126,7 +126,7 @@
%left '&' %left '&'
%nonassoc '!' %nonassoc '!'
%type <num> state-num acc-set %type <num> checked-state-num state-num acc-set
%type <b> label-expr %type <b> label-expr
%type <mark> acc-sig_opt acc-sets %type <mark> acc-sig_opt acc-sets
...@@ -152,6 +152,21 @@ BOOLEAN: 't' | 'f' ...@@ -152,6 +152,21 @@ BOOLEAN: 't' | 'f'
header: format-version header-items header: format-version header-items
{ {
// Preallocate the states if we know their number.
if (res.states != -1)
{
unsigned states = res.states;
if (res.start != -1 &&
res.states <= res.start)
{
error(res.start_loc,
"initial state number is larger than state count...");
error(res.states_loc, "... declared here.");
states = res.start + 1;
}
res.h->aut->new_states(states);
res.declared_states.resize(states);
}
if (res.accset < 0) if (res.accset < 0)
{ {
error(@$, "missing 'Acceptance:' header"); error(@$, "missing 'Acceptance:' header");
...@@ -184,17 +199,6 @@ header-item: "States:" INT ...@@ -184,17 +199,6 @@ header-item: "States:" INT
YYABORT; YYABORT;
} }
res.states = std::max(res.states, (int) $2); res.states = std::max(res.states, (int) $2);
if (res.states <= res.start)
{
error(res.start_loc,
"initial state number is larger than state count...");
error(@$, "... declared here.");
}
int missing = std::max(res.states, res.start + 1)
- res.h->aut->num_states();
assert(missing >= 0);
res.h->aut->new_states(missing);
res.declared_states.resize(res.declared_states.size() + missing);
} }
| "Start:" state-conj-2 | "Start:" state-conj-2
{ {
...@@ -336,7 +340,8 @@ header-spec: | header-spec BOOLEAN ...@@ -336,7 +340,8 @@ header-spec: | header-spec BOOLEAN
delete $2; delete $2;
} }
state-conj-2: state-num '&' state-num | state-conj-2 '&' state-num state-conj-2: checked-state-num '&' checked-state-num
| state-conj-2 '&' checked-state-num
label-expr: 't' label-expr: 't'
{ {
...@@ -459,24 +464,31 @@ state-num: INT ...@@ -459,24 +464,31 @@ state-num: INT
error(@1, "state number is too large for this implementation"); error(@1, "state number is too large for this implementation");
YYABORT; YYABORT;
} }
if ((int) $1 >= res.states)
{
if (res.states >= 0)
{
error(@1, "state number is larger than state count...");
error(res.states_loc, "... declared here.");
}
int missing = ((int) $1) - res.h->aut->num_states() + 1;
if (missing >= 0)
{
res.h->aut->new_states(missing);
res.declared_states.resize(res.declared_states.size()
+ missing);
}
}
$$ = $1; $$ = $1;
} }
checked-state-num: state-num
{
if ((int) $1 >= res.states)
{
if (res.states >= 0)
{
error(@1, "state number is larger than state "
"count...");
error(res.states_loc, "... declared here.");
}
int missing =
((int) $1) - res.h->aut->num_states() + 1;
if (missing >= 0)
{
res.h->aut->new_states(missing);
res.declared_states.resize
(res.declared_states.size() + missing);
}
}
$$ = $1;
}
states: | states state states: | states state
state: state-name labeled-edges state: state-name labeled-edges
| state-name unlabeled-edges | state-name unlabeled-edges
...@@ -488,7 +500,7 @@ state: state-name labeled-edges ...@@ -488,7 +500,7 @@ state: state-name labeled-edges
res.cur_guard = res.guards.begin(); res.cur_guard = res.guards.begin();
} }
} }
state-name: "State:" state-label_opt state-num string_opt acc-sig_opt state-name: "State:" state-label_opt checked-state-num string_opt acc-sig_opt
{ {
res.cur_state = $3; res.cur_state = $3;
if (res.declared_states[$3]) if (res.declared_states[$3])
...@@ -547,7 +559,7 @@ acc-sets: ...@@ -547,7 +559,7 @@ acc-sets:
$$ = $1 | res.h->aut->acc().mark($2); $$ = $1 | res.h->aut->acc().mark($2);
} }
labeled-edges: | labeled-edges labeled-edge labeled-edges: | labeled-edges labeled-edge
labeled-edge: trans-label state-num acc-sig_opt labeled-edge: trans-label checked-state-num acc-sig_opt
{ {
res.h->aut->new_transition(res.cur_state, $2, res.h->aut->new_transition(res.cur_state, $2,
res.cur_label, $3 | res.acc_state); res.cur_label, $3 | res.acc_state);
...@@ -561,7 +573,7 @@ labeled-edge: trans-label state-num acc-sig_opt ...@@ -561,7 +573,7 @@ labeled-edge: trans-label state-num acc-sig_opt
/* We never have zero unlabeled edges, these are considered as zero /* We never have zero unlabeled edges, these are considered as zero
labeled edges. */ labeled edges. */
unlabeled-edges: unlabeled-edge | unlabeled-edges unlabeled-edge unlabeled-edges: unlabeled-edge | unlabeled-edges unlabeled-edge
unlabeled-edge: state-num acc-sig_opt unlabeled-edge: checked-state-num acc-sig_opt
{ {
bdd cond; bdd cond;
if (res.has_state_label) if (res.has_state_label)
......
...@@ -143,7 +143,7 @@ State: 0 {0 1} ...@@ -143,7 +143,7 @@ State: 0 {0 1}
EOF EOF
expecterr input <<EOF expecterr input <<EOF
input:4.8: state number is larger than state count... input:4.1-8: initial state number is larger than state count...
input:3.1-9: ... declared here. input:3.1-9: ... declared here.
input:1.1-4.8: missing 'Acceptance:' header input:1.1-4.8: missing 'Acceptance:' header
input:6.8: state number is larger than state count... input:6.8: state number is larger than state count...
......
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