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

org: Really fix example generation

Browse source 
* doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/hoa.org,
doc/org/ltlcross.org: Fix several typos.  In particular ":results" and
":exports" both end with s.
This commit is contained in:
Alexandre Duret-Lutz 2015-07-17 22:28:45 +02:00
parent 67d3553b12
commit 4e025ecd2b
4 changed files with 19 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

26
doc/org/autfilt.org
View file

@ -27,7 +27,7 @@ same stream, =autfilt= will process them in batch.
The output format can be controlled using [[file:oaut.org][the common output options]]
(like =--spin=, =--lbtt=, =--dot=, =--hoaf=...).
#+BEGIN_SRC sh :results silent :exports code
#+BEGIN_SRC sh :results silent :exports both
cat >example.hoa <<EOF
HOA: v1
States: 1
@ -288,7 +288,7 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
Here is an automaton with transition-based acceptance:
#+BEGIN_SRC sh :result silent :export code
#+BEGIN_SRC sh :results silent :exports both
cat >aut-ex1.hoa<<EOF
HOA: v1
States: 3
@ -313,14 +313,12 @@ State: 2
EOF
#+END_SRC
#+RESULTS:
(Note: the '=.=' argument passed to =--dot= below hides default
options discussed [[file:oaut.org::#default-dot][on another page]], while the '=a=' causes the
acceptance condition to be displayed.)
#+NAME: autfilt-ex1
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt aut-ex1.hoa --dot=.a
#+END_SRC
@ -361,7 +359,7 @@ $txt
Using =-S= will "push" the acceptance membership of the transitions to the states:
#+NAME: autfilt-ex2
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt -S aut-ex1.hoa --dot=.a
#+END_SRC
@ -423,7 +421,7 @@ $txt
Using =--cnf-acceptance= simply rewrites the acceptance condition in Conjunctive Normal Form:
#+NAME: autfilt-ex3
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --cnf-acceptance aut-ex1.hoa --dot=.a
#+END_SRC
@ -467,7 +465,7 @@ of Fin-acceptance: this usually requires adding non-deterministic jumps to
altered copies of strongly-connected components.
#+NAME: autfilt-ex4
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --remove-fin aut-ex1.hoa --dot=.a
#+END_SRC
@ -513,7 +511,7 @@ transitions they contain. The acceptance condition will be updated to
reflect the fact that these sets can never be visited.
#+NAME: autfilt-ex5
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --mask-acc=1,2 aut-ex1.hoa --dot=.a
#+END_SRC
@ -559,7 +557,7 @@ Atomic propositions can be removed from an automaton in three ways:
Here are the results of these three options on our example:
#+NAME: autfilt-ex6a
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --remove-ap=a aut-ex1.hoa --dot=.a
#+END_SRC
@ -598,7 +596,7 @@ $txt
[[file:autfilt-ex6a.png]]
#+NAME: autfilt-ex6b
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --remove-ap=a=0 aut-ex1.hoa --dot=.a
#+END_SRC
@ -631,7 +629,7 @@ $txt
[[file:autfilt-ex6b.png]]
#+NAME: autfilt-ex6c
#+BEGIN_SRC sh :results verbatim :export code
#+BEGIN_SRC sh :results verbatim :exports code
autfilt --remove-ap=a=1 aut-ex1.hoa --dot=.a
#+END_SRC
@ -662,3 +660,7 @@ $txt
#+RESULTS:
[[file:autfilt-ex6c.png]]
#+BEGIN_SRC sh :results silent :exports results
rm -f example.hoa aut-ex1.hoa
#+END_SRC

2
doc/org/dstar2tgba.org
View file

@ -24,7 +24,7 @@ The following command instructs =ltl2dstar= to:
Additionally we use =ltlfilt= to convert our formula to the
prefix format used by =ltl2dstar=.
#+BEGIN_SRC sh :results silent :exports code
#+BEGIN_SRC sh :results silent :exports both
ltlfilt -f 'Fa & GFb' -l | ltl2dstar --ltl2nba=spin:ltl2tgba@-sD - fagfb
#+END_SRC

2
doc/org/hoa.org
View file

@ -159,7 +159,7 @@ State: 2
will always be stored as a TωA with this transition structure:
#+BEGIN_SRC sh :results verbatim :export results
#+BEGIN_SRC sh :results verbatim :exports results
autfilt -Ht stvstracc.hoa | sed -n '/--BODY/,/--END/p' | grep -v -- --
#+END_SRC

6
doc/org/ltlcross.org
View file

@ -705,7 +705,7 @@ For instance the following will cross-compare =ltl2tgba= against
runs out of memory (the hash tables used by =randltl= and =ltlcross=
to remove duplicate formulas will keep growing).
#+BEGIN_SRC sh :export code :eval no
#+BEGIN_SRC sh :exports code :eval no
randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%O' 'ltl3ba -f %s >%O'
#+END_SRC
@ -722,14 +722,14 @@ generation of random formulas. For instance the following command
will run the translators on an infinite number of formulas, saving
any problematic formula in =bugs.ltl=.
#+BEGIN_SRC sh :export code :eval no
#+BEGIN_SRC sh :exports code :eval no
randltl -n -1 --tree-size 10..25 a b c | ltlcross --save-bogus=bugs.ltl 'ltl2tgba --lbtt %f >%O' 'ltl3ba -f %s >%O'
#+END_SRC
You can periodically check the contents of =bugs.ltl=, and then run
=ltlcross= only on those formulas to look at the problems:
#+BEGIN_SRC sh :export code :eval no
#+BEGIN_SRC sh :exports code :eval no
ltlcross -F bugs.ltl 'ltl2tgba --lbtt %f >%O' 'ltl3ba -f %s >%O'
#+END_SRC