missing simplification rule
This is simplified from a report by Simon Jantsch:
% ltlfilt --unabbrev=W -f 'a W Gb' # (1)
Gb R (a | Gb)
% ltlfilt --simplify --unabbrev=W -f 'a W Gb' # (2)
Gb R (a | Gb)
% ltlfilt --simplify --unabbrev=W -f 'a W Gb' | ltlfilt --simplify # (3)
G(a | Gb)
Simplification is always performed before unabbrevation of LTL operators such as W, because some of the simplification rules detect patterns that can be rewritten more compactly using W. So using simplifications after unabbrevations can actually cancel the unabbreviation, as in:
% ltlfilt --unabbrev=W -f 'a W b'
b R (a | b)
% ltlfilt --unabbrev=W -f 'a W b' | ltlfilt --simplify
a W b
However in the reported case, it seems that we have other simplification rules that are applied to Gb R (a | Gb)
before detecting that this is a W pattern. This seems to be the rule that u R g = G(g)
when u
is a purely universal formula, and u
implies g
.
One way to ensure that the output of (2) is the same as (3) would be to add more simplifications rules. Maybe something like f W u = G(f | u)
when u
is a purely universal formula. It's not clear to me whether this is desirable. How would we justify that G(f | u)
is simpler than f W u
?
Another option is to teach that rule to the unabbreviate()
function. Clearly if the G
operator is allowed, unabbreviating f W u
as G(f | u)
seems much simpler than using u R (f | u)
. We'd have to generalize that to the other unabbreviations as well.
(For the record, the original formula submitted by Simon is !p0 W (p0 W (!p0 W (p0 W G!p0)))
, and he would like to simplify it to G(!p0 | G(p0 | G(!p0 | G(p0 | G!p0))))
.)