Tobias Meggendorfer <tobias.meggendorfer@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.