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

hoa: add two asserts

Browse source 
* src/tgbaalgos/hoa.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-05 18:13:34 +01:00
parent 0b8b65f96f
commit 314993b201
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/tgbaalgos/hoa.cc
View file

@ -131,6 +131,11 @@ namespace spot
is_deterministic = deterministic; is_deterministic = deterministic;
is_complete = complete; is_complete = complete;
has_state_acc = state_acc; has_state_acc = state_acc;
// If the automaton declares that it is deterministic or
// state-based, make sure that it really is.
assert(!aut->is_deterministic() || deterministic);
assert(!aut->has_state_based_acc() || state_acc);
} }
void number_all_ap() void number_all_ap()