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

* src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result):

Browse source 
Indent output as in the magic search.
This commit is contained in:
Alexandre Duret-Lutz 2003-10-23 12:16:04 +00:00
parent 46756c9589
commit 008056f279
2 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2003-10-23 Alexandre Duret-Lutz <adl@src.lip6.fr> 2003-10-23 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result):
Indent output as in the magic search.
* src/tgbatest/spotlbtt.test: Add notice about long run time. * src/tgbatest/spotlbtt.test: Add notice about long run time.
Merge emptinesscheckexplicit into ltl2tgba. Merge emptinesscheckexplicit into ltl2tgba.

22
src/tgbaalgos/emptinesscheck.cc
View file

@ -188,16 +188,15 @@ namespace spot
emptiness_check::print_result(std::ostream& os, const spot::tgba* aut, emptiness_check::print_result(std::ostream& os, const spot::tgba* aut,
const tgba* restrict) const const tgba* restrict) const
{ {
os << "======================" << std::endl;
os << "Prefix:" << std::endl; os << "Prefix:" << std::endl;
os << "======================" << std::endl;
const bdd_dict* d = aut->get_dict(); const bdd_dict* d = aut->get_dict();
for (state_sequence::const_iterator i_se = suffix.begin(); for (state_sequence::const_iterator i_se = suffix.begin();
i_se != suffix.end(); ++i_se) i_se != suffix.end(); ++i_se)
{ {
os << " ";
if (restrict) if (restrict)
{ {
os << restrict->format_state(aut->project_state((*i_se), restrict)) os << restrict->format_state(aut->project_state(*i_se, restrict))
<< std::endl; << std::endl;
} }
else else
@ -205,23 +204,22 @@ namespace spot
os << aut->format_state((*i_se)) << std::endl; os << aut->format_state((*i_se)) << std::endl;
} }
} }
os << "======================" << std::endl;
os << "Cycle:" <<std::endl; os << "Cycle:" <<std::endl;
os << "======================" << std::endl;
for (cycle_path::const_iterator it = period.begin(); for (cycle_path::const_iterator it = period.begin();
it != period.end(); ++it) it != period.end(); ++it)
{ {
os << " ";
if (restrict) if (restrict)
{ {
os << " | " << bdd_format_set(d, (*it).second) <<std::endl ; os << " | " << bdd_format_set(d, it->second) <<std::endl ;
os << restrict->format_state(aut->project_state((*it).first, os << restrict->format_state(aut->project_state(it->first,
restrict)) restrict))
<< std::endl; << std::endl;
} }
else else
{ {
os << " | " << bdd_format_set(d, (*it).second) <<std::endl ; os << " | " << bdd_format_set(d, it->second) <<std::endl ;
os << aut->format_state((*it).first) << std::endl; os << aut->format_state(it->first) << std::endl;
} }
} }
return os; return os;
@ -261,7 +259,7 @@ namespace spot
for (seen::iterator iter_map = seen_state_num.begin(); for (seen::iterator iter_map = seen_state_num.begin();
iter_map != seen_state_num.end(); ++iter_map) iter_map != seen_state_num.end(); ++iter_map)
{ {
q_index = (*iter_map).second; q_index = iter_map->second;
tmp_int = 0; tmp_int = 0;
if (q_index > 0) if (q_index > 0)
{ {
@ -269,9 +267,9 @@ namespace spot
&& (vec_component[tmp_int].index <= q_index)) && (vec_component[tmp_int].index <= q_index))
tmp_int = tmp_int+1; tmp_int = tmp_int+1;
if (tmp_int < comp_size) if (tmp_int < comp_size)
vec_component[tmp_int - 1].state_set.insert((*iter_map).first); vec_component[tmp_int - 1].state_set.insert(iter_map->first);
else else
vec_component[comp_size - 1].state_set.insert((*iter_map).first); vec_component[comp_size - 1].state_set.insert(iter_map->first);
} }
} }