Commit 162e1143 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

org: fix SAT example

* doc/org/satmin.org: Do not use ":export code" on
code that must be run on export.
parent 9130cfa1
...@@ -367,11 +367,10 @@ acceptance. ...@@ -367,11 +367,10 @@ acceptance.
For our example, let us first generate a deterministic Rabin For our example, let us first generate a deterministic Rabin
automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]]. automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]].
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results silent
ltlfilt -f "FGa | FGb" -l | ltlfilt -f "FGa | FGb" -l |
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa
#+END_SRC #+END_SRC
#+RESULTS:
Let's draw it: Let's draw it:
#+NAME: autfiltsm1 #+NAME: autfiltsm1
...@@ -727,6 +726,6 @@ given, the useless sink state would have been kept and the output ...@@ -727,6 +726,6 @@ given, the useless sink state would have been kept and the output
automaton would have 6 states. automaton would have 6 states.
#+BEGIN_SRC sh :results verbatim :exports none #+BEGIN_SRC sh :results silent :exports results
rm -f output.hoa output2.hoa rm -f output.hoa output2.hoa
#+END_SRC #+END_SRC
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment