From be408850104e259a0b4a2fa9ddce60ba1a9b9ebf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 13 Feb 2015 17:07:48 +0100 Subject: [PATCH] * doc/org/ltlfilt.org: Update description of --stutter-invariant. --- doc/org/ltlfilt.org | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 408404d83..66aad9d04 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -327,10 +327,7 @@ ltlfilt -f 'F(a & X(!a & Gb))' --remove-x | ltlfilt --equivalent-to 'F(a & X(!a #+RESULTS: : F(a & ((a & (a U (!a & Gb)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & Gb)) & ((!b U a) | (b U a))) | (b & (b U (!a & Gb & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b & Gb)) & ((!a U b) | (a U b))) | (!a & Gb & (G!a | Ga) & (Gb | G!b)))) -It is therefore equivalent, but that is not a surprise since the -=--stutter-invariant= filter is actually implemented using exactly -[[http://homepages.inf.ed.ac.uk/kousha/note_on_stut_tl_lpi.ps][this procedure]] (calling the =remove_x()= function, and building automata -to check the equivalence of the resulting formula with the original one). +It is therefore equivalent (otherwise the output would have been empty). * Using =--format=