org: add syntax highlighting for three HOA examples
* doc/org/concepts.org, doc/org/ltl2tgba.org, doc/org/ltldo.org: Here.
This commit is contained in:
parent
11262d0495
commit
f29eb91192
3 changed files with 14 additions and 14 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue