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

acc::name(): recognize Fin-less acceptance

Browse source 
* spot/twa/acc.cc: Implement this.
* tests/python/automata.ipynb, tests/python/randaut.ipynb,
tests/python/stutter-inv.ipynb: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2017-11-04 12:44:43 +01:00
parent 75a1d6ac61
commit 3334d37bb5
4 changed files with 86 additions and 76 deletions
Download patch file Download diff file Expand all files Collapse all files

35
spot/twa/acc.cc
View file

@ -1627,23 +1627,30 @@ namespace spot
}
else if (like_names)
{
std::vector<acc_cond::rs_pair> r_pairs;
bool r_like = is_rabin_like(r_pairs);
unsigned rsz = r_pairs.size();
std::vector<acc_cond::rs_pair> s_pairs;
bool s_like = is_streett_like(s_pairs);
unsigned ssz = s_pairs.size();
if (r_like && (!s_like || (rsz <= ssz)))
if (!uses_fin_acceptance())
{
os << "Rabin-like";
if (!no_main_param)
os << ' ' << rsz;
os << "Fin-less" << sets();
}
else if (s_like && (!r_like || (ssz < rsz)))
else
{
os << "Streett-like";
if (!no_main_param)
os << ' ' << ssz;
std::vector<acc_cond::rs_pair> r_pairs;
bool r_like = is_rabin_like(r_pairs);
unsigned rsz = r_pairs.size();
std::vector<acc_cond::rs_pair> s_pairs;
bool s_like = is_streett_like(s_pairs);
unsigned ssz = s_pairs.size();
if (r_like && (!s_like || (rsz <= ssz)))
{
os << "Rabin-like";
if (!no_main_param)
os << ' ' << rsz;
}
else if (s_like && (!r_like || (ssz < rsz)))
{
os << "Streett-like";
if (!no_main_param)
os << ' ' << ssz;
}
}
}
}