Skip to content

`autfilt --check=stutter` should work for non-deterministic automata

% ltl2tgba -f 'F(a & X(!a & Gb))' --check | grep properties
properties: trans-labels explicit-labels state-acc stutter-invariant
properties: weak
% ltl2tgba -f 'F(a & X(!a & Gb))' | autfilt --check | grep properties:
properties: trans-labels explicit-labels state-acc weak

we can now determinize the input in this case