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

hoa: catch redefinition of states

Browse source 
* src/hoaparse/hoaparse.yy: Here.
* src/tgbatest/hoaparse.test: More test.
This commit is contained in:
Alexandre Duret-Lutz 2014-11-21 10:49:58 +01:00
parent 69678152b6
commit 691ab05926
2 changed files with 35 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/hoaparse/hoaparse.yy
View file

@ -47,6 +47,7 @@
std::vector<int> ap; std::vector<int> ap;
std::vector<bdd> guards; std::vector<bdd> guards;
std::vector<bdd>::const_iterator cur_guard; std::vector<bdd>::const_iterator cur_guard;
std::vector<bool> declared_states; // States that have been declared.
spot::location states_loc; spot::location states_loc;
spot::location ap_loc; spot::location ap_loc;
spot::location state_label_loc; spot::location state_label_loc;
@ -189,6 +190,7 @@ header-item: "States:" INT
- res.h->aut->num_states(); - res.h->aut->num_states();
assert(missing >= 0); assert(missing >= 0);
res.h->aut->new_states(missing); res.h->aut->new_states(missing);
res.declared_states.resize(res.declared_states.size() + missing);
} }
| "Start:" state-conj-2 | "Start:" state-conj-2
{ {
@ -443,7 +445,11 @@ state-num: INT
} }
int missing = ((int) $1) - res.h->aut->num_states() + 1; int missing = ((int) $1) - res.h->aut->num_states() + 1;
if (missing >= 0) if (missing >= 0)
res.h->aut->new_states(missing); {
res.h->aut->new_states(missing);
res.declared_states.resize(res.declared_states.size()
+ missing);
}
} }
$$ = $1; $$ = $1;
} }
@ -462,6 +468,13 @@ state: state-name labeled-edges
state-name: "State:" state-label_opt state-num string_opt acc-sig_opt state-name: "State:" state-label_opt state-num string_opt acc-sig_opt
{ {
res.cur_state = $3; res.cur_state = $3;
if (res.declared_states[$3])
{
std::ostringstream o;
o << "redeclaration of state " << $3;
error(@1 + @3, o.str());
}
res.declared_states[$3] = true;
res.acc_state = $5; res.acc_state = $5;
} }
label: '[' label-expr ']' label: '[' label-expr ']'
@ -614,7 +627,9 @@ namespace spot
if (!r.h->aut) if (!r.h->aut)
return nullptr; return nullptr;
if (r.start != -1) if (r.start != -1)
r.h->aut->set_init_state(r.start); {
r.h->aut->set_init_state(r.start);
}
else else
{ {
// If no initial state has been declared, add one, because // If no initial state has been declared, add one, because

18
src/tgbatest/hoaparse.test
View file

@ -85,6 +85,24 @@ input:10.5: state number is larger than state count...
input:2.1-9: ... declared here. input:2.1-9: ... declared here.
EOF EOF
cat >input <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[0] 0
State: 0 {0}
[t] 0
--END--
EOF
expecterr input <<EOF
input:9.1-8: redeclaration of state 0
EOF
cat >input <<EOF cat >input <<EOF
HOA: v1 HOA: v1
States: 0 States: 0