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

hoa: mordenize printer slightly

Browse source 
* src/tgbaalgos/hoa.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2014-12-08 23:33:23 +01:00
parent 45db1c5fb9
commit f37ff8407c
1 changed files with 16 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/tgbaalgos/hoa.cc
View file

@ -70,6 +70,12 @@ namespace spot
number_all_ap(); number_all_ap();
} }
~metadata()
{
for (auto s: nm)
s->destroy();
}
std::ostream& std::ostream&
emit_acc(std::ostream& os, emit_acc(std::ostream& os,
const const_tgba_ptr& aut, const const_tgba_ptr& aut,
@ -162,8 +168,8 @@ namespace spot
{ {
sup_map::iterator i; sup_map::iterator i;
bdd all = bddtrue; bdd all = bddtrue;
for (i = sup.begin(); i != sup.end(); ++i) for (auto& i: sup)
all &= bdd_support(i->first); all &= bdd_support(i.first);
while (all != bddtrue) while (all != bddtrue)
{ {
@ -173,17 +179,17 @@ namespace spot
vap.push_back(v); vap.push_back(v);
} }
for (i = sup.begin(); i != sup.end(); ++i) for (auto& i: sup)
{ {
bdd cond = i->first; bdd cond = i.first;
if (cond == bddtrue) if (cond == bddtrue)
{ {
i->second = "t"; i.second = "t";
continue; continue;
} }
if (cond == bddfalse) if (cond == bddfalse)
{ {
i->second = "f"; i.second = "f";
continue; continue;
} }
std::ostringstream s; std::ostringstream s;
@ -216,7 +222,7 @@ namespace spot
} }
notfirstor = true; notfirstor = true;
} }
i->second = s.str(); i.second = s.str();
} }
} }
@ -237,8 +243,7 @@ namespace spot
metadata md(aut); metadata md(aut);
if (acceptance == Hoa_Acceptance_States if (acceptance == Hoa_Acceptance_States && !md.state_acc)
&& !md.state_acc)
acceptance = Hoa_Acceptance_Transitions; acceptance = Hoa_Acceptance_Transitions;
unsigned num_states = md.nm.size(); unsigned num_states = md.nm.size();
@ -251,10 +256,9 @@ namespace spot
<< "Start: 0" << nl << "Start: 0" << nl
<< "AP: " << md.vap.size(); << "AP: " << md.vap.size();
auto d = aut->get_dict(); auto d = aut->get_dict();
for (metadata::vap_t::const_iterator i = md.vap.begin(); for (auto& i: md.vap)
i != md.vap.end(); ++i)
{ {
auto f = ltl::is_atomic_prop(d->bdd_map[*i].f); auto f = ltl::is_atomic_prop(d->bdd_map[i].f);
assert(f); assert(f);
escape_str(os << " \"", f->name()) << '"'; escape_str(os << " \"", f->name()) << '"';
} }
@ -318,8 +322,6 @@ namespace spot
aut->release_iter(j); aut->release_iter(j);
} }
os << "--END--"; // No newline. Let the caller decide. os << "--END--"; // No newline. Let the caller decide.
for (unsigned i = 0; i < num_states; ++i)
md.nm[i]->destroy();
return os; return os;
} }