Commit 08509a2c authored by Etienne Renault's avatar Etienne Renault
Browse files

sanity: replace tabulars by spaces

* spot/ltsmin/ltsmin.cc,
spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/unionfind.cc,
spot/mc/utils.hh, spot/twacube/cube.cc,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh,
tests/core/bricks.cc,
tests/core/cube.cc,
tests/core/twacube.cc,
tests/ltsmin/modelcheck.cc: here.
parent 71da5b75
This diff is collapsed.
......@@ -31,24 +31,24 @@ namespace spot
/// emptiness check that has been proposed we opted to implement
/// the Gabow's one.
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
typename StateHash, typename StateEqual>
class ec_renault13lpar : public intersect<State, SuccIterator,
StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>
StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>
{
// Ease the manipulation
using typename intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
ec_renault13lpar<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
public:
ec_renault13lpar(kripkecube<State, SuccIterator>& sys,
twacube* twa)
: intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>(sys, twa),
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>(sys, twa),
acc_(twa->acc())
{
}
......@@ -84,13 +84,13 @@ namespace spot
/// to true and both \a newtop and \a newtop_dfsnum have inconsistency
/// values.
bool pop_state(product_state, unsigned top_dfsnum, bool,
product_state, unsigned)
product_state, unsigned)
{
if (top_dfsnum == roots_.back().dfsnum)
{
roots_.pop_back();
uf_.markdead(top_dfsnum);
}
{
roots_.pop_back();
uf_.markdead(top_dfsnum);
}
return true;
}
......@@ -101,7 +101,7 @@ namespace spot
acc_cond::mark_t cond)
{
if (uf_.isdead(dst_dfsnum))
return false;
return false;
while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum))
{
......@@ -127,18 +127,18 @@ namespace spot
// Compute the prefix of the accepting run
for (auto& s : this->todo)
res += " " + std::to_string(s.st.st_prop) +
+ "*" + this->sys_.to_string(s.st.st_kripke) + "\n";
res += " " + std::to_string(s.st.st_prop) +
+ "*" + this->sys_.to_string(s.st.st_kripke) + "\n";
// Compute the accepting cycle
res += "Cycle:\n";
struct ctrx_element
{
const product_state* prod_st;
ctrx_element* parent_st;
SuccIterator* it_kripke;
std::shared_ptr<trans_index> it_prop;
const product_state* prod_st;
ctrx_element* parent_st;
SuccIterator* it_kripke;
std::shared_ptr<trans_index> it_prop;
};
std::queue<ctrx_element*> bfs;
......@@ -148,65 +148,65 @@ namespace spot
this->sys_.succ(this->todo.back().st.st_kripke),
this->twa_->succ(this->todo.back().st.st_prop)}));
while (true)
{
here:
auto* front = bfs.front();
bfs.pop();
// PUSH all successors of the state.
while (!front->it_kripke->done())
{
while (!front->it_prop->done())
{
if (this->twa_->get_cubeset().intersect
(this->twa_->trans_data(front->it_prop).cube_,
front->it_kripke->condition()))
{
const product_state dst = {
front->it_kripke->state(),
this->twa_->trans_storage(front->it_prop).dst
};
{
here:
auto* front = bfs.front();
bfs.pop();
// PUSH all successors of the state.
while (!front->it_kripke->done())
{
while (!front->it_prop->done())
{
if (this->twa_->get_cubeset().intersect
(this->twa_->trans_data(front->it_prop).cube_,
front->it_kripke->condition()))
{
const product_state dst = {
front->it_kripke->state(),
this->twa_->trans_storage(front->it_prop).dst
};
// Skip Unknown states or not same SCC
auto it = this->map.find(dst);
if (it == this->map.end() ||
!uf_.sameset(it->second,
this->map[this->todo.back().st]))
{
front->it_prop->next();
continue;
}
// Skip Unknown states or not same SCC
auto it = this->map.find(dst);
if (it == this->map.end() ||
!uf_.sameset(it->second,
this->map[this->todo.back().st]))
{
front->it_prop->next();
continue;
}
// This is a valid transition. If this transition
// is the one we are looking for, update the counter-
// -example and flush the bfs queue.
auto mark = this->twa_->trans_data(front->it_prop).acc_;
if (!acc.has(mark))
{
ctrx_element* current = front;
while (current != nullptr)
{
// FIXME also display acc?
res = res + " " +
std::to_string(current->prod_st->st_prop) +
+ "*" +
this->sys_. to_string(current->prod_st
->st_kripke) +
"\n";
current = current->parent_st;
}
// This is a valid transition. If this transition
// is the one we are looking for, update the counter-
// -example and flush the bfs queue.
auto mark = this->twa_->trans_data(front->it_prop).acc_;
if (!acc.has(mark))
{
ctrx_element* current = front;
while (current != nullptr)
{
// FIXME also display acc?
res = res + " " +
std::to_string(current->prod_st->st_prop) +
+ "*" +
this->sys_. to_string(current->prod_st
->st_kripke) +
"\n";
current = current->parent_st;
}
// empty the queue
while (!bfs.empty())
{
auto* e = bfs.front();
bfs.pop();
delete e;
}
// empty the queue
while (!bfs.empty())
{
auto* e = bfs.front();
bfs.pop();
delete e;
}
// update acceptance
acc |= mark;
if (this->twa_->acc().accepting(acc))
return res;
// update acceptance
acc |= mark;
if (this->twa_->acc().accepting(acc))
return res;
const product_state* q = &(it->first);
ctrx_element* root = new ctrx_element({
......@@ -242,15 +242,15 @@ namespace spot
virtual std::string stats() override
{
return
std::to_string(this->dfs_number) + " unique states visited\n" +
std::to_string(roots_.size()) +
" strongly connected components in search stack\n" +
std::to_string(this->transitions) + " transitions explored\n";
std::to_string(this->dfs_number) + " unique states visited\n" +
std::to_string(roots_.size()) +
" strongly connected components in search stack\n" +
std::to_string(this->transitions) + " transitions explored\n";
}
private:
bool found_ = false; ///< \brief A counterexample is detected?
bool found_ = false; ///< \brief A counterexample is detected?
struct root_element {
unsigned dfsnum;
......
......@@ -42,8 +42,8 @@ namespace spot
/// The other template parameters allows to consider any kind
/// of state (and so any kind of kripke structures).
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename EmptinessCheck>
typename StateHash, typename StateEqual,
typename EmptinessCheck>
class SPOT_API intersect
{
public:
......@@ -78,64 +78,64 @@ namespace spot
self().setup();
product_state initial = {sys_.initial(), twa_->get_initial()};
if (SPOT_LIKELY(self().push_state(initial, dfs_number+1, 0U)))
{
todo.push_back({initial, sys_.succ(initial.st_kripke),
twa_->succ(initial.st_prop)});
{
todo.push_back({initial, sys_.succ(initial.st_kripke),
twa_->succ(initial.st_prop)});
// Not going further! It's a product with a single state.
if (todo.back().it_prop->done())
return false;
// Not going further! It's a product with a single state.
if (todo.back().it_prop->done())
return false;
forward_iterators(true);
map[initial] = ++dfs_number;
}
forward_iterators(true);
map[initial] = ++dfs_number;
}
while (!todo.empty())
{
// Check the kripke is enough since it's the outer loop. More
// details in forward_iterators.
if (todo.back().it_kripke->done())
{
bool is_init = todo.size() == 1;
auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
if (SPOT_LIKELY(self().pop_state(todo.back().st,
map[todo.back().st],
is_init,
newtop,
map[newtop])))
{
sys_.recycle(todo.back().it_kripke);
// FIXME a local storage for twacube iterator?
todo.pop_back();
if (SPOT_UNLIKELY(self().counterexample_found()))
return true;
}
}
else
{
++transitions;
product_state dst = {
todo.back().it_kripke->state(),
twa_->trans_storage(todo.back().it_prop).dst
};
auto acc = twa_->trans_data(todo.back().it_prop).acc_;
forward_iterators(false);
auto it = map.find(dst);
if (it == map.end())
{
if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc)))
{
map[dst] = ++dfs_number;
todo.push_back({dst, sys_.succ(dst.st_kripke),
twa_->succ(dst.st_prop)});
forward_iterators(true);
}
}
else if (SPOT_UNLIKELY(self().update(todo.back().st,
dfs_number,
dst, map[dst], acc)))
return true;
}
}
{
// Check the kripke is enough since it's the outer loop. More
// details in forward_iterators.
if (todo.back().it_kripke->done())
{
bool is_init = todo.size() == 1;
auto newtop = is_init? todo.back().st: todo[todo.size() -2].st;
if (SPOT_LIKELY(self().pop_state(todo.back().st,
map[todo.back().st],
is_init,
newtop,
map[newtop])))
{
sys_.recycle(todo.back().it_kripke);
// FIXME a local storage for twacube iterator?
todo.pop_back();
if (SPOT_UNLIKELY(self().counterexample_found()))
return true;
}
}
else
{
++transitions;
product_state dst = {
todo.back().it_kripke->state(),
twa_->trans_storage(todo.back().it_prop).dst
};
auto acc = twa_->trans_data(todo.back().it_prop).acc_;
forward_iterators(false);
auto it = map.find(dst);
if (it == map.end())
{
if (SPOT_LIKELY(self().push_state(dst, dfs_number+1, acc)))
{
map[dst] = ++dfs_number;
todo.push_back({dst, sys_.succ(dst.st_kripke),
twa_->succ(dst.st_prop)});
forward_iterators(true);
}
}
else if (SPOT_UNLIKELY(self().update(todo.back().st,
dfs_number,
dst, map[dst], acc)))
return true;
}
}
return false;
}
......@@ -158,8 +158,8 @@ namespace spot
virtual std::string stats()
{
return
std::to_string(dfs_number) + " unique states visited\n" +
std::to_string(transitions) + " transitions explored\n";
std::to_string(dfs_number) + " unique states visited\n" +
std::to_string(transitions) + " transitions explored\n";
}
protected:
......@@ -175,37 +175,37 @@ namespace spot
// Sometimes kripke state may have no successors.
if (todo.back().it_kripke->done())
return;
return;
// The state has just been push and the 2 iterators intersect.
// There is no need to move iterators forward.
assert(!(todo.back().it_prop->done()));
if (just_pushed && twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition()))
return;
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition()))
return;
// Otherwise we have to compute the next valid successor (if it exits).
// This requires two loops. The most inner one is for the twacube since
// its costless
if (todo.back().it_prop->done())
todo.back().it_prop->reset();
todo.back().it_prop->reset();
else
todo.back().it_prop->next();
todo.back().it_prop->next();
while (!todo.back().it_kripke->done())
{
while (!todo.back().it_prop->done())
{
if (SPOT_UNLIKELY(twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition())))
return;
todo.back().it_prop->next();
}
todo.back().it_prop->reset();
todo.back().it_kripke->next();
}
{
while (!todo.back().it_prop->done())
{
if (SPOT_UNLIKELY(twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition())))
return;
todo.back().it_prop->next();
}
todo.back().it_prop->reset();
todo.back().it_kripke->next();
}
}
public:
......@@ -219,11 +219,11 @@ namespace spot
{
bool
operator()(const product_state lhs,
const product_state rhs) const
const product_state rhs) const
{
StateEqual equal;
return (lhs.st_prop == rhs.st_prop) &&
equal(lhs.st_kripke, rhs.st_kripke);
StateEqual equal;
return (lhs.st_prop == rhs.st_prop) &&
equal(lhs.st_kripke, rhs.st_kripke);
}
};
......@@ -232,10 +232,10 @@ namespace spot
size_t
operator()(const product_state that) const
{
// FIXME! wang32_hash(that.st_prop) could have
// been pre-calculated!
StateHash hasher;
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
// FIXME! wang32_hash(that.st_prop) could have
// been pre-calculated!
StateHash hasher;
return wang32_hash(that.st_prop) ^ hasher(that.st_kripke);
}
};
......@@ -249,8 +249,8 @@ namespace spot
twacube* twa_;
std::vector<todo_element> todo;
typedef std::unordered_map<const product_state, int,
product_state_hash,
product_state_equal> visited_map;
product_state_hash,
product_state_equal> visited_map;
visited_map map;
unsigned int dfs_number = 0;
unsigned int transitions = 0;
......
......@@ -27,8 +27,8 @@ namespace spot
/// of a kripkecube. The algorithm uses a single DFS since it
/// is the most efficient in a sequential setting
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual,
typename Visitor>
typename StateHash, typename StateEqual,
typename Visitor>
class SPOT_API seq_reach_kripke
{
public:
......@@ -59,32 +59,32 @@ namespace spot
visited[initial] = ++dfs_number;
self().push(initial, dfs_number);
while (!todo.empty())
{
if (todo.back().it->done())
{
sys_.recycle(todo.back().it);
todo.pop_back();
}
else
{
++transitions;
State dst = todo.back().it->state();
auto it = visited.insert({dst, dfs_number+1});
if (it.second)
{
++dfs_number;
self().push(dst, dfs_number);
self().edge(visited[todo.back().s], dfs_number);
todo.back().it->next();
todo.push_back({dst, sys_.succ(dst)});
}
else
{
self().edge(visited[todo.back().s], visited[dst]);
todo.back().it->next();
}
}
}
{
if (todo.back().it->done())
{
sys_.recycle(todo.back().it);
todo.pop_back();
}
else
{
++transitions;
State dst = todo.back().it->state();
auto it = visited.insert({dst, dfs_number+1});
if (it.second)
{
++dfs_number;
self().push(dst, dfs_number);
self().edge(visited[todo.back().s], dfs_number);
todo.back().it->next();
todo.push_back({dst, sys_.succ(dst)});
}
else
{
self().edge(visited[todo.back().s], visited[dst]);
todo.back().it->next();
}
}
}
self().finalize();
}
......@@ -109,7 +109,7 @@ namespace spot
// FIXME: The system already handle a set of visited states so
// this map is redundant: an we avoid this new map?
typedef std::unordered_map<const State, int,
StateHash, StateEqual> visited_map;
StateHash, StateEqual> visited_map;
visited_map visited;
unsigned int dfs_number = 0;
unsigned int transitions = 0;
......
......@@ -69,7 +69,7 @@ namespace spot
else {
id[root2] = root1;
if (rk1 == rk2)
id[root1] = -(rk1 + 1);
id[root1] = -(rk1 + 1);
}
return true;
}
......
......@@ -27,18 +27,18 @@
namespace spot
{
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
typename StateHash, typename StateEqual>
class SPOT_API kripke_to_twa :
public seq_reach_kripke<State, SuccIterator,
StateHash, StateEqual,
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>
StateHash, StateEqual,
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>
{
public:
kripke_to_twa(kripkecube<State, SuccIterator>& sys, bdd_dict_ptr dict)
: seq_reach_kripke<State, SuccIterator, StateHash, StateEqual,
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>(sys),
kripke_to_twa<State, SuccIterator,
StateHash, StateEqual>>(sys),
dict_(dict)
{}
......@@ -57,10 +57,10 @@ namespace spot
// Compute the reverse binder.
auto aps = this->sys_.get_ap();
for (unsigned i = 0; i < aps.size(); ++i)
{
auto k = res_->register_ap(aps[i]);
reverse_binder_.insert({i, k});
}
{
auto k = res_->register_ap(aps[i]);
reverse_binder_.insert({i, k});
}
}
void push(State s, unsigned i)
......@@ -74,7 +74,7 @@ namespace spot
{
cubeset cs(this->sys_.get_ap().size());
bdd cond = cube_to_bdd(this->todo.back().it->condition(),
cs, reverse_binder_);
cs, reverse_binder_);
res_->