org: simplify babel blocks using #+PROPERTY: header-args
This feature is in Org 9, which is already required. * doc/org/autcross.org, doc/org/autfilt.org, doc/org/compile.org, doc/org/concepts.org, doc/org/csv.org, doc/org/dstar2tgba.org, doc/org/genaut.org, doc/org/genltl.org, doc/org/hierarchy.org, doc/org/hoa.org, doc/org/ioltl.org, doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org, doc/org/ltldo.org, doc/org/ltlfilt.org, doc/org/ltlgrind.org, doc/org/ltlsynt.org, doc/org/oaut.org, doc/org/randaut.org, doc/org/randltl.org, doc/org/satmin.org, doc/org/setup.org, doc/org/tools.org, doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org, doc/org/tut04.org, doc/org/tut10.org, doc/org/tut11.org, doc/org/tut12.org, doc/org/tut20.org, doc/org/tut21.org, doc/org/tut22.org, doc/org/tut23.org, doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org, doc/org/upgrade2.org: Simplify SRC block setups for sh, python and C++. Also fix a few typos and examples along the way.
This commit is contained in:
Alexandre Duret-Lutz
parent
0c8e6a38a8
commit
8a96828d85
40 changed files with 2193 additions and 2281 deletions
|
|
@ -3,6 +3,7 @@
|
|||
#+DESCRIPTION: Spot command-line tools for minimizing ω-automata
|
||||
#+INCLUDE: setup.org
|
||||
#+HTML_LINK_UP: tools.html
|
||||
#+PROPERTY: header-args:sh :results verbatim :exports both
|
||||
|
||||
#+NAME: version
|
||||
#+BEGIN_SRC sh :exports none
|
||||
|
|
@ -50,7 +51,7 @@ Let us first state a few facts about this minimization procedure.
|
|||
|
||||
* How to change the SAT solver used
|
||||
|
||||
By default Spot uses PicoSAT call_version()[:results raw]), this SAT-solver
|
||||
By default Spot uses PicoSAT call_version()[:results raw], this SAT-solver
|
||||
is built into the Spot library, so that no temporary files are used to
|
||||
store the problem.
|
||||
|
||||
|
|
@ -59,7 +60,7 @@ SAT solver used by Spot. This variable should describe a shell command
|
|||
to run the SAT-solver on an input file called =%I= so that a model satisfying
|
||||
the formula will be written in =%O=. For instance to use [[http://www.labri.fr/perso/lsimon/glucose/][Glucose 3.0]], instead
|
||||
of the builtin version of PicoSAT, define
|
||||
#+BEGIN_SRC sh
|
||||
#+BEGIN_SRC sh :exports code
|
||||
export SPOT_SATSOLVER='glucose -verb=0 -model %I >%O'
|
||||
#+END_SRC
|
||||
We assume the SAT solver follows the input/output conventions of the
|
||||
|
|
@ -80,14 +81,14 @@ automaton.
|
|||
|
||||
However =-D= is not a guarantee to obtain a deterministic automaton,
|
||||
even if one exists. For instance, =-D= fails to produce a
|
||||
deterministic automaton for =GF(a <-> XXb)=. Instead we get a 9-state
|
||||
deterministic automaton for =a U X(b | GF!b)=. Instead we get a 4-state
|
||||
non-deterministic automaton.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltl2tgba -D 'GF(a <-> XXb)' --stats='states=%s, det=%d'
|
||||
#+BEGIN_SRC sh
|
||||
ltl2tgba -D 'a U X(b | GF!b)' --stats='states=%s, det=%d'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: states=9, det=0
|
||||
: states=4, det=0
|
||||
|
||||
Option =-x tba-det= enables an additional
|
||||
determinization procedure, that would otherwise not be used by =-D=
|
||||
|
|
@ -98,60 +99,27 @@ acceptance conditions, it will be degeneralized first.
|
|||
On our example, =-x tba-det= successfully produces a deterministic
|
||||
TBA, but a non-minimal one:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltl2tgba -D -x tba-det 'GF(a <-> XXb)' --stats='states=%s, det=%d'
|
||||
#+BEGIN_SRC sh
|
||||
ltl2tgba -D -x tba-det 'a U X(b | GF!b)' --stats='states=%s, det=%d'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: states=7, det=1
|
||||
: states=9, det=1
|
||||
|
||||
Option =-x sat-minimize= will turn-on SAT-based minimization. It also
|
||||
implies =-x tba-det=, so there is no need to supply both options.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
ltl2tgba -D -x sat-minimize 'GF(a <-> XXb)' --stats='states=%s, det=%d'
|
||||
#+BEGIN_SRC sh
|
||||
ltl2tgba -D -x sat-minimize 'a U X(b | GF!b)' --stats='states=%s, det=%d'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: states=4, det=1
|
||||
: states=5, det=1
|
||||
|
||||
We can draw it:
|
||||
|
||||
#+NAME: gfaexxb3
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltl2tgba -D -x sat-minimize 'GF(a <-> XXb)' -d
|
||||
#+BEGIN_SRC sh :exports code
|
||||
ltl2tgba -D -x sat-minimize 'a U X(b | GF!b)' -d
|
||||
#+END_SRC
|
||||
#+RESULTS: gfaexxb3
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 1 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
0 -> 2 [label=<!a & b>]
|
||||
0 -> 3 [label=<a & b>]
|
||||
0 -> 3 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<a & b>]
|
||||
1 -> 0 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
1 -> 1 [label=<!a & b>]
|
||||
1 -> 1 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label=<a & !b>]
|
||||
2 -> 1 [label=<!a & b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
2 -> 1 [label=<!a & !b>]
|
||||
2 -> 3 [label=<a & b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
3 [label="3"]
|
||||
3 -> 2 [label=<!a & b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
3 -> 2 [label=<!a & !b>]
|
||||
3 -> 3 [label=<a & b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
3 -> 3 [label=<a & !b>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file gfaexxb3.svg :var txt=gfaexxb3 :exports results
|
||||
$txt
|
||||
|
|
@ -166,46 +134,8 @@ result will of course be slightly bigger.
|
|||
|
||||
#+NAME: gfaexxb4
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltl2tgba -BD -x sat-minimize 'GF(a <-> XXb)' -d
|
||||
ltl2tgba -BD -x sat-minimize 'a U X(b | GF!b)' -d
|
||||
#+END_SRC
|
||||
#+RESULTS: gfaexxb4
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label=<!a & b>]
|
||||
0 -> 1 [label=<!b>]
|
||||
0 -> 2 [label=<a & b>]
|
||||
1 [label="1", peripheries=2]
|
||||
1 -> 4 [label=<!a>]
|
||||
1 -> 5 [label=<a>]
|
||||
2 [label="2"]
|
||||
2 -> 1 [label=<!b>]
|
||||
2 -> 4 [label=<!a & b>]
|
||||
2 -> 5 [label=<a & b>]
|
||||
3 [label="3", peripheries=2]
|
||||
3 -> 0 [label=<!a>]
|
||||
3 -> 1 [label=<a & !b>]
|
||||
3 -> 2 [label=<a & b>]
|
||||
4 [label="4"]
|
||||
4 -> 0 [label=<!a & !b>]
|
||||
4 -> 1 [label=<a & b>]
|
||||
4 -> 2 [label=<a & !b>]
|
||||
4 -> 3 [label=<!a & b>]
|
||||
5 [label="5"]
|
||||
5 -> 1 [label=<a & b>]
|
||||
5 -> 3 [label=<!a & b>]
|
||||
5 -> 4 [label=<!a & !b>]
|
||||
5 -> 5 [label=<a & !b>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file gfaexxb4.svg :var txt=gfaexxb4 :exports results
|
||||
$txt
|
||||
|
|
@ -214,10 +144,11 @@ $txt
|
|||
[[file:gfaexxb4.svg]]
|
||||
|
||||
|
||||
There are cases where =ltl2tgba='s =tba-det= algorithm fails to produce a deterministic automaton.
|
||||
In that case, SAT-based minimization is simply skipped. For instance:
|
||||
There are cases where =ltl2tgba='s =tba-det= algorithm fails to
|
||||
produce a deterministic automaton. In that case, SAT-based
|
||||
minimization is simply skipped. For instance:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+BEGIN_SRC sh
|
||||
ltl2tgba -D -x sat-minimize 'G(F(!b & (X!a M (F!a & F!b))) U !b)' --stats='states=%s, det=%d'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
|
|
@ -234,7 +165,7 @@ The first is purely syntactic. If a formula belongs to the class of
|
|||
without being syntactic recurrences.) [[file:ltlfilt.org][=ltlfilt=]] can be instructed to
|
||||
print only formulas that are syntactic recurrences:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+BEGIN_SRC sh
|
||||
ltlfilt --syntactic-recurrence -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
|
|
@ -247,7 +178,7 @@ converting a deterministic Rabin automaton using [[file:dstar2tgba.org][=dstar2t
|
|||
output is guaranteed to be deterministic if and only if the input DRA
|
||||
expresses a recurrence property.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+BEGIN_SRC sh
|
||||
ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l |
|
||||
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
|
||||
dstar2tgba -D --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
|
||||
|
|
@ -274,7 +205,7 @@ As far as SAT-based minimization goes, =dstar2tgba= will take the same
|
|||
options as =ltl2tgba=. For instance we can see that the smallest DTBA
|
||||
has call_size(arg="%s -x sat-minimize")[:results raw] states:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+BEGIN_SRC sh
|
||||
ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l |
|
||||
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
|
||||
dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
|
||||
|
|
@ -284,8 +215,9 @@ dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-se
|
|||
|
||||
* More acceptance sets
|
||||
|
||||
The formula "=G(F(!b & (X!a M (F!a & F!b))) U !b)=" can in fact be minimized into an
|
||||
even smaller automaton if we use multiple acceptance sets.
|
||||
The formula "=G(F(!b & (X!a M (F!a & F!b))) U !b)=" can in fact be
|
||||
minimized into an even smaller automaton if we use multiple acceptance
|
||||
sets.
|
||||
|
||||
Unfortunately because =dstar2tgba= does not know the formula being
|
||||
translated, and it always convert a DRA into a DBA (with a single
|
||||
|
|
@ -294,7 +226,7 @@ more acceptance sets could be useful to further minimize it. This
|
|||
number of acceptance sets can however be specified on the command-line
|
||||
with option =-x sat-acc=M=. For instance:
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+BEGIN_SRC sh
|
||||
ltlfilt --remove-wm -f 'G(F(!b & (X!a M (F!a & F!b))) U !b)' -l |
|
||||
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
|
||||
dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
|
||||
|
|
@ -408,51 +340,16 @@ acceptance.
|
|||
For our example, let us first generate a deterministic Rabin
|
||||
automaton with [[http://www.ltl2dstar.de/][=ltl2dstar=]].
|
||||
|
||||
#+BEGIN_SRC sh :results silent :exports both
|
||||
#+BEGIN_SRC sh :results silent
|
||||
ltlfilt -f 'FGa | FGb' -l |
|
||||
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds --output-format=hoa - - > output.hoa
|
||||
#+END_SRC
|
||||
|
||||
Let's draw it:
|
||||
#+NAME: autfiltsm1
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt output.hoa --dot
|
||||
#+END_SRC
|
||||
#+RESULTS: autfiltsm1
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label=<(Fin(<font color="#5DA5DA">â¿</font>) & Inf(<font color="#F17CB0">â¶</font>)) | (Fin(<font color="#FAA43A">â·</font>) & Inf(<font color="#B276B2">â¸</font>))>
|
||||
labelloc="t"
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label=<0<br/><font color="#5DA5DA">â¿</font><font color="#FAA43A">â·</font>>]
|
||||
0 -> 0 [label=<!a & !b>]
|
||||
0 -> 1 [label=<a & !b>]
|
||||
0 -> 2 [label=<!a & b>]
|
||||
0 -> 3 [label=<a & b>]
|
||||
1 [label=<1<br/><font color="#F17CB0">â¶</font><font color="#FAA43A">â·</font>>]
|
||||
1 -> 0 [label=<!a & !b>]
|
||||
1 -> 1 [label=<a & !b>]
|
||||
1 -> 2 [label=<!a & b>]
|
||||
1 -> 3 [label=<a & b>]
|
||||
2 [label=<2<br/><font color="#5DA5DA">â¿</font><font color="#B276B2">â¸</font>>]
|
||||
2 -> 0 [label=<!a & !b>]
|
||||
2 -> 1 [label=<a & !b>]
|
||||
2 -> 2 [label=<!a & b>]
|
||||
2 -> 3 [label=<a & b>]
|
||||
3 [label=<3<br/><font color="#F17CB0">â¶</font><font color="#B276B2">â¸</font>>]
|
||||
3 -> 0 [label=<!a & !b>]
|
||||
3 -> 1 [label=<a & !b>]
|
||||
3 -> 2 [label=<!a & b>]
|
||||
3 -> 3 [label=<a & b>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file autfiltsm1.svg :var txt=autfiltsm1 :exports results
|
||||
$txt
|
||||
|
|
@ -466,7 +363,7 @@ transition-based version (the output may change depending on the SAT
|
|||
solver used):
|
||||
|
||||
#+NAME: autfiltsm2
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt --sat-minimize output.hoa --dot
|
||||
#+END_SRC
|
||||
|
||||
|
|
@ -479,7 +376,7 @@ $txt
|
|||
We can also attempt to build a state-based version with
|
||||
|
||||
#+NAME: autfiltsm3
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt -S --sat-minimize output.hoa --dot
|
||||
#+END_SRC
|
||||
|
||||
|
|
@ -500,32 +397,10 @@ You can however force a specific acceptance to be used as output.
|
|||
Let's try with generalized co-Büchi for instance:
|
||||
|
||||
#+NAME: autfiltsm4
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt -S --sat-minimize='acc="generalized-co-Buchi 2"' output.hoa --dot
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: autfiltsm4
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label=<Fin(<font color="#5DA5DA">⓿</font>)|Fin(<font color="#F17CB0">❶</font>)>
|
||||
labelloc="t"
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label=<0<br/><font color="#5DA5DA">⓿</font>>]
|
||||
0 -> 0 [label=<a>]
|
||||
0 -> 1 [label=<!a>]
|
||||
1 [label=<1<br/><font color="#F17CB0">❶</font>>]
|
||||
1 -> 0 [label=<!b>]
|
||||
1 -> 1 [label=<b>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file autfiltsm4.svg :var txt=autfiltsm4 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -539,7 +414,7 @@ give an acceptance formula in the [[http://adl.github.io/hoaf/#acceptance][HOA s
|
|||
attempt to create a co-Büchi automaton with
|
||||
|
||||
#+NAME: autfiltsm5
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt -S --sat-minimize='acc="Fin(0)"' output.hoa --dot
|
||||
#+END_SRC
|
||||
#+RESULTS: autfiltsm5
|
||||
|
|
@ -571,32 +446,11 @@ Here is an example demonstrating the case where the input automaton is
|
|||
smaller than the output. Let's take this small TGBA as input:
|
||||
|
||||
#+NAME: autfiltsm6
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
ltl2tgba 'GFa & GFb' >output2.hoa
|
||||
autfilt output2.hoa --dot
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: autfiltsm6
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label=<Inf(<font color="#5DA5DA">⓿</font>)&Inf(<font color="#F17CB0">❶</font>)>
|
||||
labelloc="t"
|
||||
node [shape="circle"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label=<a & b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
||||
0 -> 0 [label=<!a & !b>]
|
||||
0 -> 0 [label=<!a & b<br/><font color="#F17CB0">❶</font>>]
|
||||
0 -> 0 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file autfiltsm6.svg :var txt=autfiltsm6 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -607,10 +461,10 @@ $txt
|
|||
|
||||
If we attempt to minimize it into a transition-based Büchi automaton,
|
||||
with fewer states, it will fail, output no result, and return with a
|
||||
non-zero exit code (because no automata where output).
|
||||
non-zero exit code (because no automata were output).
|
||||
|
||||
#+NAME: autfiltsm7
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+BEGIN_SRC sh
|
||||
autfilt --sat-minimize='acc="Buchi"' output2.hoa
|
||||
echo $?
|
||||
#+END_SRC
|
||||
|
|
@ -620,7 +474,7 @@ echo $?
|
|||
However if we allow more states, it will work:
|
||||
|
||||
#+NAME: autfiltsm8
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt --sat-minimize='acc="Buchi",max-states=3' output2.hoa --dot
|
||||
#+END_SRC
|
||||
|
||||
|
|
@ -692,7 +546,7 @@ Compare the following, where parity acceptance is used, but the
|
|||
automaton is not colored:
|
||||
|
||||
#+NAME: autfiltsm9
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt -S --sat-minimize='acc="parity max even 3"' output2.hoa --dot
|
||||
#+END_SRC
|
||||
|
||||
|
|
@ -707,7 +561,7 @@ $txt
|
|||
belong to exactly one acceptance set:
|
||||
|
||||
#+NAME: autfiltsm10
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
#+BEGIN_SRC sh :exports code
|
||||
autfilt -S --sat-minimize='acc="parity max even 3",colored' output2.hoa --dot
|
||||
#+END_SRC
|
||||
|
||||
|
|
@ -724,22 +578,31 @@ If the environment variable =SPOT_SATLOG= is set to the name of a
|
|||
file, the minimization function will append statistics about each of
|
||||
its iterations in this file.
|
||||
|
||||
#+BEGIN_SRC sh :results verbatim :exports both
|
||||
#+BEGIN_SRC sh
|
||||
rm -f stats.csv
|
||||
export SPOT_SATLOG=stats.csv
|
||||
ltlfilt -f 'Ga R (F!b & (c U b))' -l |
|
||||
ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - - |
|
||||
dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)'
|
||||
echo ==== stats.csv ====
|
||||
cat stats.csv
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
: input(states=11) output(states=5, acc-sets=2, det=1)
|
||||
: ==== stats.csv ====
|
||||
: input.states,target.states,reachable.states,edges,transitions,variables,clauses,enc.user,enc.sys,sat.user,sat.sys,automaton
|
||||
: 10,5,,,,13600,1543042,59,3,187,0,
|
||||
: 10,7,7,33,56,26656,4247441,162,7,775,0,"HOA: v1 States: 7 Start: 0 AP: 3 ""a"" ""b"" ""c"" acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete deterministic --BODY-- State: 0 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!0&!1&!2] 1 {0} [0&!1&!2] 1 [0&!1&2] 2 {1} [0&1&!2] 4 [0&1&2] 4 {0} State: 1 [0&!1] 1 {0} [!0&!1&!2 | 0&1] 1 [!0&1 | !0&2] 3 {0} State: 2 [!0&!1&2] 0 {1} [!0&1] 0 {0 1} [!0&!1&!2] 1 [0&!1&2] 2 [0&!1&!2] 3 {1} [0&1] 5 {0 1} State: 3 [!1&!2] 3 [1 | 2] 3 {0} State: 4 [!0&!1&2] 0 {0 1} [!0&1] 0 {0} [!0&!1&!2] 1 [0&1] 4 {0} [0&!1&2] 5 {0} [0&!1&!2] 6 State: 5 [!0&1 | !0&2] 0 {0 1} [!0&!1&!2] 1 [0&1 | 0&2] 5 {0 1} [0&!1&!2] 6 {0} State: 6 [!0&!1&!2] 1 [!0&1&!2] 1 {0 1} [!0&1&2] 1 {1} [!0&!1&2] 3 {0 1} [0] 6 {0 1} --END--"
|
||||
: 7,6,6,26,48,10512,1376507,50,0,269,0,"HOA: v1 States: 6 Start: 0 AP: 3 ""a"" ""b"" ""c"" acc-name: generalized-Buchi 2 Acceptance: 2 Inf(0)&Inf(1) properties: trans-labels explicit-labels trans-acc complete deterministic --BODY-- State: 0 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!0&!1&!2] 1 [0&!1&!2] 1 {0 1} [0&!1&2] 2 {1} [0&1] 3 {0} State: 1 [t] 1 State: 2 [!0&!1&2] 0 {1} [!0&1] 0 {0} [!1&!2] 1 [0&!1&2] 2 {1} [0&1] 4 {1} State: 3 [!0&!1&2] 0 {1} [!0&1] 0 [!0&!1&!2] 1 [0&1] 3 [0&!1&2] 4 {1} [0&!1&!2] 5 {1} State: 4 [!0&!1&2 | !0&1&!2] 0 {0 1} [!0&1&2] 0 {0} [!0&!1&!2] 1 [0&1 | 0&2] 4 {0 1} [0&!1&!2] 5 State: 5 [!0&!1&!2] 1 [!0&1 | !0&2] 1 {0 1} [0] 5 {0 1} --END--"
|
||||
|
||||
Here is the contents of the =stats.csv= file:
|
||||
#+begin_src sh :exports results :results output raw
|
||||
sed '1a\
|
||||
|-|
|
||||
s/^/|/
|
||||
s/$/|/
|
||||
s/,/|/g
|
||||
s/"HOA:.*--END--"/HOA:.../' stats.csv
|
||||
#+end_src
|
||||
#+RESULTS:
|
||||
| input.states | target.states | reachable.states | edges | transitions | variables | clauses | enc.user | enc.sys | sat.user | sat.sys | automaton |
|
||||
|--------------+---------------+------------------+-------+-------------+-----------+---------+----------+---------+----------+---------+-----------|
|
||||
| 8 | 4 | | | | 5120 | 446320 | 22 | 1 | 17 | 0 | |
|
||||
| 8 | 6 | 6 | 29 | 48 | 11520 | 1515749 | 50 | 4 | 234 | 0 | HOA:... |
|
||||
| 8 | 5 | | | | 8000 | 874992 | 29 | 0 | 67 | 0 | |
|
||||
|
||||
The generated CSV file use the following columns:
|
||||
- =input.states=: the number of states of the reference automaton at this step
|
||||
|
|
@ -759,14 +622,17 @@ file follows RFC4180 in escaping double-quote by doubling them.
|
|||
|
||||
In the above example, the DRA produced by =ltl2dstar= had 11 states.
|
||||
In the first line of the =stats.csv= file, you can see the
|
||||
minimization function had a 10-state input, which means that
|
||||
=dstar2tgba= first reduced the 11-state (complete) DRA into a 10-state
|
||||
(complete) DBA before calling the SAT-based minimization. This first
|
||||
line shows the SAT-based minimization for a (complete) 5-state DTGBA
|
||||
and failing to find one. Then on the next line it looks for a 7-state
|
||||
solution, finds one. Finally, it finds a (complete) 6-state solution,
|
||||
now using the 7-state version as reference automaton to further
|
||||
simplify the problem.
|
||||
minimization function had a 8-state input, which means that
|
||||
=dstar2tgba= first reduced the 11-state (complete) DRA into a 8-state
|
||||
(complete) DBA before calling the SAT-based minimization (the fact
|
||||
that the input was reduced to a *DBA* is not very obvious from this
|
||||
trace), This first line shows the SAT-based minimization for a
|
||||
(complete) 5-state DTGBA and failing to find one. Then on the next
|
||||
line it looks for a 6-state solution, finds one. Finally, it looks
|
||||
for a 5-state solution, and cannot find one. The reason the 5-state
|
||||
attempt uses the 8-state automaton as input rather than the 6-state
|
||||
automaton is because the 8-state automaton uses 1 acceptance states
|
||||
(it's a DBA) while the 6-state automaton uses 2.
|
||||
|
||||
The final output is reported with 5 states, because by default we
|
||||
output trim automata. If the =--complete= option had been given, the
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue