alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Improve ltlfilt.org

Browse source 
* doc/org/ltlfilt.org: Mention that the --stutter-invariant check
use automata.  Fix a typo.
This commit is contained in:
Alexandre Duret-Lutz 2013-06-09 18:55:57 +02:00
parent 644b5f0152
commit 372a086cb7
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
doc/org/ltlfilt.org
View file

@ -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