* src/tgba/tgbacomplement.cc, src/tgbatest/complementation.cc: Fix style.
This commit is contained in:
parent
7817f325eb
commit
4d4fc641b5
3 changed files with 22 additions and 13 deletions
|
|
@ -1,3 +1,7 @@
|
||||||
|
2009-06-09 Guillaume Sadegh <sadegh@lrde.epita.fr>
|
||||||
|
|
||||||
|
* src/tgba/tgbacomplement.cc, src/tgbatest/complementation.cc: Fix style.
|
||||||
|
|
||||||
2009-06-07 Guillaume Sadegh <sadegh@lrde.epita.fr>
|
2009-06-07 Guillaume Sadegh <sadegh@lrde.epita.fr>
|
||||||
|
|
||||||
* src/tgba/tgbacomplement.cc (state_complement::hash): Improve
|
* src/tgba/tgbacomplement.cc (state_complement::hash): Improve
|
||||||
|
|
|
||||||
|
|
@ -245,7 +245,9 @@ namespace spot
|
||||||
for (subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
|
for (subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
|
||||||
hash ^= (*i)->hash();
|
hash ^= (*i)->hash();
|
||||||
|
|
||||||
for (child_list::const_iterator i = children.begin(); i != children.end(); ++i)
|
for (child_list::const_iterator i = children.begin();
|
||||||
|
i != children.end();
|
||||||
|
++i)
|
||||||
hash ^= (*i)->hash();
|
hash ^= (*i)->hash();
|
||||||
|
|
||||||
return hash;
|
return hash;
|
||||||
|
|
@ -332,7 +334,7 @@ namespace spot
|
||||||
(*i)->branch_accepting(a);
|
(*i)->branch_accepting(a);
|
||||||
|
|
||||||
subset_t subset;
|
subset_t subset;
|
||||||
for(subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
|
for (subset_t::const_iterator i = nodes.begin(); i != nodes.end(); ++i)
|
||||||
if (a.state_is_accepting(*i))
|
if (a.state_is_accepting(*i))
|
||||||
subset.insert(*i);
|
subset.insert(*i);
|
||||||
|
|
||||||
|
|
@ -367,11 +369,11 @@ namespace spot
|
||||||
t_it != transitions.end();
|
t_it != transitions.end();
|
||||||
++t_it)
|
++t_it)
|
||||||
{
|
{
|
||||||
if (((*t_it).first & condition) != bddfalse)
|
if ((t_it->first & condition) != bddfalse)
|
||||||
{
|
{
|
||||||
if (new_subset.find((*t_it).second) == new_subset.end())
|
if (new_subset.find(t_it->second) == new_subset.end())
|
||||||
{
|
{
|
||||||
const state* s = (*t_it).second->clone();
|
const state* s = t_it->second->clone();
|
||||||
new_subset.insert(s);
|
new_subset.insert(s);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -795,7 +797,7 @@ namespace spot
|
||||||
}
|
}
|
||||||
std::cout << conditions;
|
std::cout << conditions;
|
||||||
if (this_node->marked)
|
if (this_node->marked)
|
||||||
std::cout << "\",style=filled,fillcolor=\"gray";
|
std::cout << "\", style=filled, fillcolor=\"gray";
|
||||||
|
|
||||||
std::cout << "\"];" << std::endl;
|
std::cout << "\"];" << std::endl;
|
||||||
|
|
||||||
|
|
@ -805,7 +807,7 @@ namespace spot
|
||||||
print_safra_tree(*i, node_names, current_node,
|
print_safra_tree(*i, node_names, current_node,
|
||||||
nb_accepting_conditions);
|
nb_accepting_conditions);
|
||||||
std::cout << "node" << this_node << " -> node" << *i
|
std::cout << "node" << this_node << " -> node" << *i
|
||||||
<< "[color=\"red\",arrowhead=\"none\"];"
|
<< "[color=\"red\", arrowhead=\"none\"];"
|
||||||
<< std::endl;
|
<< std::endl;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -1069,7 +1071,7 @@ namespace spot
|
||||||
for (automaton_t::const_iterator i = automaton.begin();
|
for (automaton_t::const_iterator i = automaton.begin();
|
||||||
i != automaton.end();
|
i != automaton.end();
|
||||||
++i)
|
++i)
|
||||||
max = std::max(max, (*i).first->max_name());
|
max = std::max(max, i->first->max_name());
|
||||||
return max_nb_pairs_ = max + 1;
|
return max_nb_pairs_ = max + 1;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1243,7 +1245,7 @@ namespace spot
|
||||||
bdd res = bddtrue;
|
bdd res = bddtrue;
|
||||||
trans_it i;
|
trans_it i;
|
||||||
for (i = node->second.begin(); i != node->second.end(); ++i)
|
for (i = node->second.begin(); i != node->second.end(); ++i)
|
||||||
res |= (*i).first;
|
res |= i->first;
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1263,7 +1265,7 @@ namespace spot
|
||||||
bdd res = bddtrue;
|
bdd res = bddtrue;
|
||||||
trans_it i;
|
trans_it i;
|
||||||
for (i = node->second.begin(); i != node->second.end(); ++i)
|
for (i = node->second.begin(); i != node->second.end(); ++i)
|
||||||
res &= bdd_support((*i).first);
|
res &= bdd_support(i->first);
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -67,9 +67,12 @@ int main(int argc, char* argv[])
|
||||||
|
|
||||||
switch (argv[i][1])
|
switch (argv[i][1])
|
||||||
{
|
{
|
||||||
case 's': print_safra = true; break;
|
case 's':
|
||||||
case 'a': print_automaton = true; break;
|
print_safra = true; break;
|
||||||
case 'f': check = true; break;
|
case 'a':
|
||||||
|
print_automaton = true; break;
|
||||||
|
case 'f':
|
||||||
|
check = true; break;
|
||||||
default:
|
default:
|
||||||
std::cerr << "unrecognized option `-" << argv[i][1]
|
std::cerr << "unrecognized option `-" << argv[i][1]
|
||||||
<< "'" << std::endl;
|
<< "'" << std::endl;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue