diff --git a/doc/org/concepts.org b/doc/org/concepts.org index a94433ce4..2402f8b13 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -841,12 +841,12 @@ The [[http://adl.github.io/hoaf/][HOA format]] inherits several features from th extends it in many ways, including support for non-deterministic automata, alternating automata, and for arbitrary acceptance conditions. -#+BEGIN_SRC sh :exports results +#+BEGIN_SRC sh :exports results :wrap SRC hoa ltldo ltl2dstar -f 'FGp0 | GFp1' --name=%f #+END_SRC #+RESULTS: -#+begin_example +#+begin_SRC hoa HOA: v1 name: "FGp0 | GFp1" States: 4 @@ -878,7 +878,7 @@ State: 3 {1 3} [!0&1] 2 [0&1] 3 --END-- -#+end_example +#+end_SRC #+NAME: hoa1 #+BEGIN_SRC sh diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org index 0b7e48c73..5a332f5a9 100644 --- a/doc/org/ltl2tgba.org +++ b/doc/org/ltl2tgba.org @@ -32,16 +32,16 @@ less frequent.) Formulas to translate may be specified using [[file:ioltl.org][common input options for LTL/PSL formulas]]. -#+BEGIN_SRC sh +#+BEGIN_SRC sh :wrap SRC hoa ltl2tgba -f 'Fa & GFb' #+END_SRC #+RESULTS: -#+begin_example +#+begin_SRC hoa HOA: v1 name: "Fa & GFb" States: 2 -Start: 1 +Start: 0 AP: 2 "a" "b" acc-name: Buchi Acceptance: 1 Inf(0) @@ -49,13 +49,13 @@ properties: trans-labels explicit-labels trans-acc complete properties: deterministic stutter-invariant --BODY-- State: 0 -[1] 0 {0} -[!1] 0 +[!0] 0 +[0] 1 State: 1 -[0] 0 -[!0] 1 +[!1] 1 +[1] 1 {0} --END-- -#+end_example +#+end_SRC Actually, because =ltl2tgba= is often used with a single formula passed on the command line, the =-f= option can be omitted and any diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 775e7a9c9..5c3a3aba8 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -485,12 +485,12 @@ Instead of outputting the result of the translation of each formula by each translator, =ltldo= can also be configured to output the smallest automaton obtained for each formula: -#+BEGIN_SRC sh +#+BEGIN_SRC sh :wrap SRC hoa ltldo ltl2ba ltl3ba 'ltl2tgba -s' -f 'F(a & Xa | FGa)' --smallest #+END_SRC #+RESULTS: -#+begin_example +#+begin_SRC hoa HOA: v1 States: 3 Start: 0 @@ -507,7 +507,7 @@ State: 1 State: 2 {0} [t] 2 --END-- -#+end_example +#+end_SRC Therefore, in practice, =ltldo --smallest trans1 trans2 trans3...= acts like a portfolio of translators, always returning the smallest