Commit 63cb925f authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

* src/tgbaalgos/degen.cc: Fix style.

parent 73ee5044
// Copyright (C) 2012 Laboratoire de Recherche et // Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// Développement de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -199,7 +199,7 @@ namespace spot ...@@ -199,7 +199,7 @@ namespace spot
{ {
std::vector<bdd>::iterator i; std::vector<bdd>::iterator i;
std::cout << "Order_" << scc << ":\t"; std::cout << "Order_" << scc << ":\t";
for (i=order_.begin(); i!=order_.end(); i++) for (i = order_.begin(); i != order_.end(); i++)
{ {
bdd_print_acc(std::cout, dict, *i); bdd_print_acc(std::cout, dict, *i);
std::cout << ", "; std::cout << ", ";
...@@ -337,7 +337,8 @@ namespace spot ...@@ -337,7 +337,8 @@ namespace spot
std::map<const state*, int>names; std::map<const state*, int>names;
names[s.first] = 1; names[s.first] = 1;
ds2num[s] = 10000 * names[s.first] + 100 * s.second + m.scc_of_state(s.first); ds2num[s] =
10000 * names[s.first] + 100 * s.second + m.scc_of_state(s.first);
#else #else
ds2num[s] = 0; ds2num[s] = 0;
#endif #endif
...@@ -414,7 +415,7 @@ namespace spot ...@@ -414,7 +415,7 @@ namespace spot
// degeralize it without ignoring *prev, you'll get // degeralize it without ignoring *prev, you'll get
// two copies of states 2, depending on whether we // two copies of states 2, depending on whether we
// reach it using 1=>2 or from 2->2. If this // reach it using 1=>2 or from 2->2. If this
// example was not clear, uncomment this following // example was not clear, uncomment the following
// "if" block, and play with the "degenid.test" // "if" block, and play with the "degenid.test"
// test case. // test case.
// //
...@@ -459,11 +460,12 @@ namespace spot ...@@ -459,11 +460,12 @@ namespace spot
if (is_scc_acc) if (is_scc_acc)
{ {
acc |= otheracc; acc |= otheracc;
// If use_z_lvl is on, start with level zero 0 when swhitching SCCs // If use_z_lvl is on, start with level zero 0 when
// swhitching SCCs
unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0; unsigned next = (!use_z_lvl || s_scc == scc) ? slevel : 0;
// If lvl_cache is used and switching SCCs, use level from cache // If lvl_cache is used and switching SCCs, use level from cache
if (use_lvl_cache && s_scc != scc if (use_lvl_cache && s_scc != scc
&& lvl_cache.find(d.first) != lvl_cache.end()) && lvl_cache.find(d.first) != lvl_cache.end())
{ {
d.second = lvl_cache[d.first]; d.second = lvl_cache[d.first];
...@@ -521,7 +523,8 @@ namespace spot ...@@ -521,7 +523,8 @@ namespace spot
// degen_acc on all outgoing transitions. (We are still // degen_acc on all outgoing transitions. (We are still
// building a TGBA; we only assure that it can be used as // building a TGBA; we only assure that it can be used as
// an SBA.) // an SBA.)
t->acceptance_conditions = is_acc ? degen_acc : bddfalse; if (is_acc)
t->acceptance_conditions = degen_acc;
} }
else else
{ {
...@@ -535,7 +538,7 @@ namespace spot ...@@ -535,7 +538,7 @@ namespace spot
#ifdef DEGEN_DEBUG #ifdef DEGEN_DEBUG
std::vector<bdd>::iterator i; std::vector<bdd>::iterator i;
std::cout << "Orig. order: \t"; std::cout << "Orig. order: \t";
for (i=order.begin(); i!=order.end(); i++) for (i = order.begin(); i != order.end(); i++)
{ {
bdd_print_acc(std::cout, dict, *i); bdd_print_acc(std::cout, dict, *i);
std::cout << ", "; std::cout << ", ";
......
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