30 Jun
2019
30 Jun
'19
7:10 p.m.
Dear Scott,
On Sun, Jun 30, 2019 at 11:41 AM Scott M. Staley <smstaley(a)comcast.net> wrote:
A quick (?) question. When I put the following LTL
formula into SPOT online: G (G (p => Gp ) => Gp) => (FG p => Gp) SPOT says it
is equivalent to 1. Therefore I assume it’s a theorem of LTL.
If you turn on "expert mode" on the "rewrite" tab of this page, you
can play with a few options and discover that the formula is not
reduced to 1 unless you tick "reduction based on automata-based
containements".
Without this option the formula is just rewritten to Gp | GF!p | F(F!p
& G(!p | Gp)).
From that formula, automata-based tests can establish
that "GF!p |
F(F!p & G(!p | Gp))" implies "!Gp" (its
actually equivalent, but
implication is enough), therefore the entire formula is necessarily
true.
The list of rules implemented is given in
https://spot.lrde.epita.fr/tl.pdf, and this one is the first of the
implication-based simplifications (Section 5.4.3)
My question: Is there anyway to see the series of
rewrites of the formula to show how it gets form the original formula to “true”?
Not easily.
If you compile the source of Spot yourelf, you can to modify the
rewriting code to trace its execution for debugging
https://gitlab.lrde.epita.fr/spot/spot/blob/ad2f5524/spot/tl/simplify.cc#L22
but that won't really detail each steps as the code sometimes performs
multiple rewritings at once.
Best regards,
Alexandre Duret-Lutz