18 Mar
2021
18 Mar
'21
3:54 p.m.
Tobias Meggendorfer <tobias.meggendorfer(a)ist.ac.at> writes:
Btw, how does the "-x ..." switch compare to
"--low"? Adding "--low"
to "--parity --deterministic" does not seem to change much.
For deterministic input --low has no influence on the simulation-based
reduction. --low disables iterated simulations (running forward and
backward simulation-based reductions until nothing is simplified
anymore), and replaces it by a single forward simulation pass. However
when working on deterministic automata, backward simulation is not
necessary anyway (and therefore never done).
--low replaces "simplify-acceptance" by "cleanup-acceptance" in the
postprocessor (i.e., not the additional simplify-acceptance you are
calling in autfilt first). Basically this now only removes unused sets
without trying to find inclusion between sets or doing unit-propagation
on the formula. It's possible that cleanup-acceptance might be enough
on DRA.
--low disables WDBA minimization (i.e. detecting whether the
input language can be represented by a Weak DBA, and returning
the minimal WDBA if that's the case). So this implies -x wdba-minimize=0.
In the current development code --low disables remove_unused_ap(), but
in the current release I don't think it does.
You can see the documentation for -x simul and -x wdba-minimize in
https://spot.lrde.epita.fr/man/spot-x.7.html
These two are the usual culprits when a ltl2tgba or autfilt takes too long.