From 372a086cb7d67273959a7c2c02f59a92aed28695 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 9 Jun 2013 18:55:57 +0200 Subject: [PATCH] Improve ltlfilt.org * doc/org/ltlfilt.org: Mention that the --stutter-invariant check use automata. Fix a typo. --- doc/org/ltlfilt.org | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/org/ltlfilt.org b/doc/org/ltlfilt.org index 743a6fbb5..03a7be78e 100644 --- a/doc/org/ltlfilt.org +++ b/doc/org/ltlfilt.org @@ -221,7 +221,7 @@ two formulas are equivalent. It would print nothing and set the exit status to 1, were the two formulas not equivalent. -If the formula =F(a & X(!a & Gb))= stutter-invariant? +Is the formula =F(a & X(!a & Gb))= stutter-invariant? #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f 'F(a & X(!a & Gb))' --stutter-invariant @@ -250,8 +250,8 @@ ltlfilt -f 'F(a & X(!a & Gb))' --remove-x | ltlfilt --equivalent-to 'F(a & X(!a 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 checking the -equivalence of the resulting formula with the original one). +[[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). # LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck