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

dot: display Rabin-like and Streett-like acceptances

Browse source 
* spot/twaalgos/dot.cc (print_acceptance_for_human): Add Rabin-like
and Streett-like checks.
* tests/core/sccdot.test, tests/python/decompose.ipynb,
tests/python/randaut.ipynb, tests/core/alternating.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2017-08-30 13:52:20 +02:00
parent ed361bb0a9
commit 205294c2c2
5 changed files with 120 additions and 108 deletions
Download patch file Download diff file Expand all files Collapse all files

23
spot/twaalgos/dot.cc
View file

@ -466,10 +466,25 @@ namespace spot
bool max = false;
bool odd = false;
if (aut_->acc().is_parity(max, odd))
os_ << nl << "[parity "
<< (max ? "max " : "min ")
<< (odd ? "odd " : "even ")
<< aut_->num_sets() << ']';
{
os_ << nl << "[parity "
<< (max ? "max " : "min ")
<< (odd ? "odd " : "even ")
<< aut_->num_sets() << ']';
}
else
{
std::vector<acc_cond::rs_pair> r_pairs;
bool r_like = aut_->acc().is_rabin_like(r_pairs);
unsigned rsz = r_pairs.size();
std::vector<acc_cond::rs_pair> s_pairs;
bool s_like = aut_->acc().is_streett_like(s_pairs);
unsigned ssz = s_pairs.size();
if (r_like && (!s_like || (rsz <= ssz)))
os_ << nl << "[Rabin-like " << rsz << ']';
else if (s_like && (!r_like || (ssz < rsz)))
os_ << nl << "[Streett-like " << ssz << ']';
}
}
}
}