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

Use SPOT_ASSERT() instead of assert() in public headers

Browse source 
* spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/utils.hh: here.
This commit is contained in:
Etienne Renault 2016-09-29 15:59:29 +02:00
parent c515ee92e2
commit fb4ef40d11
4 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/mc/ec.hh
View file

@ -124,7 +124,7 @@ namespace spot
std::string trace() std::string trace()
{ {
assert(counterexample_found()); SPOT_ASSERT(counterexample_found());
std::string res = "Prefix:\n"; std::string res = "Prefix:\n";
// Compute the prefix of the accepting run // Compute the prefix of the accepting run

9
spot/mc/intersect.hh
View file

@ -62,7 +62,7 @@ namespace spot
twacube_ptr twa): twacube_ptr twa):
sys_(sys), twa_(twa) sys_(sys), twa_(twa)
{ {
assert(is_a_kripkecube(sys)); SPOT_ASSERT(is_a_kripkecube(sys));
map.reserve(2000000); map.reserve(2000000);
todo.reserve(100000); todo.reserve(100000);
} }
@ -178,8 +178,9 @@ namespace spot
/// is slightly different. /// is slightly different.
void forward_iterators(bool just_pushed) void forward_iterators(bool just_pushed)
{ {
assert(!todo.empty()); SPOT_ASSERT(!todo.empty());
assert(!(todo.back().it_prop->done() && todo.back().it_kripke->done())); SPOT_ASSERT(!(todo.back().it_prop->done() &&
todo.back().it_kripke->done()));
// Sometimes kripke state may have no successors. // Sometimes kripke state may have no successors.
if (todo.back().it_kripke->done()) if (todo.back().it_kripke->done())
@ -187,7 +188,7 @@ namespace spot
// The state has just been push and the 2 iterators intersect. // The state has just been push and the 2 iterators intersect.
// There is no need to move iterators forward. // There is no need to move iterators forward.
assert(!(todo.back().it_prop->done())); SPOT_ASSERT(!(todo.back().it_prop->done()));
if (just_pushed && twa_->get_cubeset() if (just_pushed && twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_, .intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition())) todo.back().it_kripke->condition()))

2
spot/mc/reachability.hh
View file

@ -35,7 +35,7 @@ namespace spot
seq_reach_kripke(kripkecube<State, SuccIterator>& sys): seq_reach_kripke(kripkecube<State, SuccIterator>& sys):
sys_(sys) sys_(sys)
{ {
assert(is_a_kripkecube(sys)); SPOT_ASSERT(is_a_kripkecube(sys));
visited.reserve(2000000); visited.reserve(2000000);
todo.reserve(100000); todo.reserve(100000);
} }

4
spot/mc/utils.hh
View file

@ -67,7 +67,7 @@ namespace spot
{ {
unsigned st = res_->new_state(); unsigned st = res_->new_state();
names_->push_back(this->sys_.to_string(s)); names_->push_back(this->sys_.to_string(s));
assert(st == i); SPOT_ASSERT(st == i);
} }
void edge(unsigned src, unsigned dst) void edge(unsigned src, unsigned dst)
@ -167,7 +167,7 @@ namespace spot
unsigned st = res_->new_state(); unsigned st = res_->new_state();
names_->push_back(this->sys_.to_string(s.st_kripke) + names_->push_back(this->sys_.to_string(s.st_kripke) +
('*' + std::to_string(s.st_prop))); ('*' + std::to_string(s.st_prop)));
assert(st+1 == i); SPOT_ASSERT(st+1 == i);
return true; return true;
} }