cases where --medium helps determinization
Here are two cases where ltl2tgba --med -GD
is better than ltl2tgba --high -GD
.
% genltl --neg --dac=50 | ltl2tgba --high -G -D --stats=%s
11
% genltl --neg --dac=50 | ltl2tgba --med -G -D --stats=%s
10
% genltl --dac=51 | ltl2tgba --high -G -D --stats=%s
7
% genltl --dac=51 | ltl2tgba --med -G -D --stats=%s
6
I suspect it has to do with the fact that keeping the useless marks that naturally appear on edges between SCCs can help the BDD-based implication checks in tgba_determinize()
.
Of the entire DAC patterns, these are the only two cases where I observe a difference between --high
and --med
, so maybe it make sense to modify postprocessor
to always keep these extra marks before calling tgba_determinize()
?