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

postproc: fix default for acd and interaction with colored

Browse source 
* spot/twaalgos/postproc.hh (postprocess::acd_): Default to true.
* spot/twaalgos/postproc.cc (postprocess::run): When acd is used
to color an automaton, do not run scc_filter to remove color
from transiant edges.
* tests/python/acd.py: New file.
* tests/Makefile.am: Add it.
This commit is contained in:
Alexandre Duret-Lutz 2024-02-06 14:09:42 +01:00
parent dc5a569582
commit 27b8e5aa73
5 changed files with 90 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

22
spot/twaalgos/postproc.cc
View file

@ -407,7 +407,7 @@ namespace spot
// ignored.
a = scc_filter_states(a);
else
a = do_scc_filter(a, (PREF_ == Any));
a = do_scc_filter(a, (PREF_ == Any) && !COLORED_);
if (type_ == Monitor)
{
@ -721,23 +721,11 @@ namespace spot
sim = nullptr;
}
if (level_ == High && scc_filter_ != 0)
{
if (dba)
{
// Do that even for WDBA, to remove marks from transitions
// leaving trivial SCCs.
dba = do_scc_filter(dba, true);
assert(!sim);
}
else if (sim)
{
sim = do_scc_filter(sim, true);
assert(!dba);
}
}
sim = dba ? dba : sim;
if (level_ == High && scc_filter_ != 0 && !(acd_was_used_ && COLORED_))
// Do that even for WDBA, to remove marks from transitions
// leaving trivial SCCs.
sim = do_scc_filter(sim, true);
if (type_ == CoBuchi)
{

2
spot/twaalgos/postproc.hh
View file

@ -269,7 +269,7 @@ namespace spot
int simul_max_ = 4096;
int merge_states_min_ = 128;
int wdba_det_max_ = 4096;
bool acd_ = false;
bool acd_ = true;
bool acd_was_used_;
};
/// @}