LTL simplification: GFp0 U Gp0 should be FGp0
% ltlfilt --simplify -f 'GFp0 U Gp0'
GFp0 U Gp0
We should have GFa U b
rewritten as F b
whenever b
implies GFa
.
% ltlfilt --simplify -f 'GFp0 U Gp0'
GFp0 U Gp0
We should have GFa U b
rewritten as F b
whenever b
implies GFa
.