Commit 7f077a5a authored by Etienne Renault's avatar Etienne Renault
Browse files

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

* spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/utils.hh: here.
parent 58ee0d6e
...@@ -124,7 +124,7 @@ namespace spot ...@@ -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
......
...@@ -62,7 +62,7 @@ namespace spot ...@@ -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 ...@@ -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 ...@@ -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()))
......
...@@ -35,7 +35,7 @@ namespace spot ...@@ -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);
} }
......
...@@ -67,7 +67,7 @@ namespace spot ...@@ -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 ...@@ -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;
} }
......
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