From 3076c3da4e932beb4d34f354cd1e3b5d59781609 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 15 Sep 2013 22:37:55 +0200 Subject: [PATCH] org: document SAT-based minimization * doc/org/satmin.org, doc/org/satmin.tex: New files. * doc/Makefile.am: Add them. * doc/org/tools.org: Point to satmin.org. * NEWS: Mention satmin.html. --- NEWS | 2 + doc/Makefile.am | 10 +- doc/org/satmin.org | 403 +++++++++++++++++++++++++++++++++++++++++++++ doc/org/satmin.tex | 101 ++++++++++++ doc/org/tools.org | 4 + 5 files changed, 519 insertions(+), 1 deletion(-) create mode 100644 doc/org/satmin.org create mode 100644 doc/org/satmin.tex diff --git a/NEWS b/NEWS index 20fa6254b..7d4077c5c 100644 --- a/NEWS +++ b/NEWS @@ -68,6 +68,8 @@ New in spot 1.1.4a (not relased) deterministic automaton more efficiently) and is disabled by default. See the spot-x(7) man page for documentation about the related options: sat-minimize, sat-states, sat-acc, state-based. + See also http://spot.lip6.fr/userdoc/satmin.html for some + examples. - ltlfilt, genltl, and randltl now have a --latex option to output formulas in a way that its easier to embed in a LaTeX document. diff --git a/doc/Makefile.am b/doc/Makefile.am index 38dfb122c..9cb42479d 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -68,7 +68,15 @@ ORG_FILES = \ org/ltlcross.org \ org/ltlfilt.org \ org/randltl.org \ - org/tools.org + org/tools.org \ + org/satmin.org \ + org/satmin.tex \ + $(srcdir)/org/satmin.png + +$(srcdir)/org/satmin.png: org/satmin.tex + cd $(srcdir)/org && \ + pdflatex -shell-escape satmin.tex && \ + rm -f satmin.pdf satmin.aux satmin.log $(srcdir)/org-stamp: $(ORG_FILES) $(configure_ac) make org && touch $@ diff --git a/doc/org/satmin.org b/doc/org/satmin.org new file mode 100644 index 000000000..d68132944 --- /dev/null +++ b/doc/org/satmin.org @@ -0,0 +1,403 @@ +#+TITLE: SAT-based Minimization of Deterministic (Generalized) Büchi Automata +#+EMAIL spot@lrde.epita.fr +#+OPTIONS: H:2 num:nil toc:t +#+LINK_UP: file:tools.html + +This page explains how to use [[file:ltl2tgba.org][=ltl2tgba=]] or [[file:dstar2tgba.org][=dstar2tgba=]] to minimize +deterministic automata using a SAT solver. + +Let us first state a few facts about this minimization procedure. + +1) The procedure works only on *deterministic* Büchi automata: any + recurrence property can be converted into a deterministic Büchi + automaton, and sometimes there are several ways of doing so. +2) Spot actually implement two SAT-based minimization procedures: one + that builds a deterministic transition-based Büchi automaton + (DTBA), and one the builds a deterministic transition-based + generalized Büchi automaton (DTGBA). For the latter, we can supply + the number $m$ of acceptance sets to use. +3) These two procedures can optionally constrain their output to + use state-based acceptance. (They simply restrict all the outgoing + transitions of a state to belong to the same acceptance sets.) +4) A SAT solver should be installed for this to work. (Spot does not + distribute any SAT solver.) +5) [[file:ltl2tgba.org][=ltl2tgba=]] and [[file:dstar2tgba.org][=dstar2tgba=]] will always try to output an automaton + If they fail to determinize the property, they will simply output a + nondeterministic automaton, if they managed to obtain a + deterministic automaton but failed to minimize it (e.g., the + requested number of states in the final automaton is too low), they + will return that "unminimized" deterministic automaton. There are + only two cases where these tool will abort without returning an + automaton: when the number of clauses output by Spot (and to be fed + to the SAT solver) exceeds $2^{31}$, or when the SAT-solver was + killed by a signal. + +* How change the SAT solver used + +The environment variable =SPOT_SATSOLVER= can be used to change the +SAT solver used by Spot. The default is "=glucose %I >%O=", therefore +if you have installed [[https://www.lri.fr/~simon/?page=glucose][=glucose=]] in your =$PATH=, it should work right +away. Otherwise you may redefine this variable to point the correct +location or to another SAT solver. The =%I= and =%O= sequences will be +replaced by the names of temporary files containing the input for the +SAT solver and receiving its output. We assume that the SAT solver +should follow the conventions of the [[http://www.satcompetition.org/][SAT competition]] for input and +output. + +* Enabling SAT-based minimization for deterministic automata + +Both tools follow the same interface, because they use the same +post-processing steps internally (i.e., the =spot::postprocessor= +class). + +First, option =-D= should be used to declare that you are looking for +more determinism. This will tweak the translation algorithm used by +=ltl2tgba= to improve determinism, and will also instruct the +post-processing routine used by both tools to prefer a +deterministic automaton over a smaller equivalent nondeterministic +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 +non-deterministic automaton. + +#+BEGIN_SRC sh :results verbatim :exports both +ltl2tgba -D "GF(a <-> XXb)" --stats='states=%s, det=%d' +#+END_SRC +#+RESULTS: +: states=9, det=0 + +Option =-x tba-det= enables an additional +determinization procedure, that would otherwise not be used by =-D= +alone. This procedure will work on any automaton that can be +represented by a DTBA; if the automaton to process use multiple +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' +#+END_SRC +#+RESULTS: +: states=7, 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' +#+END_SRC +#+RESULTS: +: states=4, det=1 + +We can draw it: + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1"] + 1 -> 1 [label="a & !b\n"] + 1 -> 2 [label="!b & !a\n"] + 1 -> 2 [label="b & !a\n{Acc[1]}"] + 1 -> 3 [label="a & b\n{Acc[1]}"] + 2 [label="2"] + 2 -> 4 [label="!b & !a\n"] + 2 -> 4 [label="b & !a\n{Acc[1]}"] + 2 -> 3 [label="a & !b\n"] + 2 -> 3 [label="a & b\n{Acc[1]}"] + 3 [label="4"] + 3 -> 1 [label="a & !b\n{Acc[1]}"] + 3 -> 1 [label="a & b\n"] + 3 -> 2 [label="!b & !a\n{Acc[1]}"] + 3 -> 2 [label="b & !a\n"] + 4 [label="3"] + 4 -> 2 [label="!b & !a\n{Acc[1]}"] + 4 -> 4 [label="b & !a\n"] + 4 -> 3 [label="a & !b\n{Acc[1]}"] + 4 -> 3 [label="a & b\n"] +} +#+end_example + +#+NAME: gfaexxb3 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -D -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: gfaexxb3 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1"] + 1 -> 1 [label="a & !b\\n"] + 1 -> 1 [label="a & b\\n{Acc[1]}"] + 1 -> 2 [label="!b & !a\\n"] + 1 -> 2 [label="b & !a\\n{Acc[1]}"] + 2 [label="2"] + 2 -> 3 [label="!b & !a\\n"] + 2 -> 3 [label="b & !a\\n{Acc[1]}"] + 2 -> 4 [label="a & !b\\n"] + 2 -> 4 [label="a & b\\n{Acc[1]}"] + 3 [label="3"] + 3 -> 1 [label="a & !b\\n{Acc[1]}"] + 3 -> 3 [label="b & !a\\n"] + 3 -> 4 [label="!b & !a\\n{Acc[1]}"] + 3 -> 4 [label="a & b\\n"] + 4 [label="4"] + 4 -> 1 [label="a & !b\\n{Acc[1]}"] + 4 -> 1 [label="a & b\\n"] + 4 -> 2 [label="!b & !a\\n{Acc[1]}"] + 4 -> 2 [label="b & !a\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file gfaexxb3.png :cmdline -Tpng :var txt=gfaexxb3 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:gfaexxb3.png]] + +Clearly this is automaton benefit from the transition-based +acceptance. If we want a traditional Büchi automaton, with +state-based acceptance, we only need to add the =-B= option. The +result will of course be slightly bigger. + +#+BEGIN_SRC sh :results verbatim :exports code +ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" +#+END_SRC +#+RESULTS: +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1", peripheries=2] + 1 -> 2 [label="!a\n{Acc[1]}"] + 1 -> 3 [label="a & !b\n{Acc[1]}"] + 1 -> 4 [label="a & b\n{Acc[1]}"] + 2 [label="2", peripheries=2] + 2 -> 1 [label="!b & !a\n{Acc[1]}"] + 2 -> 4 [label="a\n{Acc[1]}"] + 2 -> 5 [label="b & !a\n{Acc[1]}"] + 3 [label="4"] + 3 -> 1 [label="a & b\n"] + 3 -> 2 [label="b & !a\n"] + 3 -> 3 [label="a & !b\n"] + 3 -> 6 [label="!b & !a\n"] + 4 [label="3"] + 4 -> 1 [label="!b\n"] + 4 -> 3 [label="a & b\n"] + 4 -> 6 [label="b & !a\n"] + 5 [label="6"] + 5 -> 1 [label="!b\n"] + 5 -> 4 [label="a & b\n"] + 5 -> 5 [label="b & !a\n"] + 6 [label="5"] + 6 -> 1 [label="a & b\n"] + 6 -> 2 [label="b & !a\n"] + 6 -> 4 [label="a & !b\n"] + 6 -> 5 [label="!b & !a\n"] +} +#+end_example + +#+NAME: gfaexxb4 +#+BEGIN_SRC sh :results verbatim :exports none +ltl2tgba -BD -x sat-minimize "GF(a <-> XXb)" | sed 's/\\/\\\\/' +#+END_SRC +#+RESULTS: gfaexxb4 +#+begin_example +digraph G { + 0 [label="", style=invis, height=0] + 0 -> 1 + 1 [label="1", peripheries=2] + 1 -> 1 [label="!b & !a\\n{Acc[1]}"] + 1 -> 2 [label="b & !a\\n{Acc[1]}"] + 1 -> 3 [label="a\\n{Acc[1]}"] + 2 [label="2"] + 2 -> 1 [label="!b & !a\\n"] + 2 -> 2 [label="b & !a\\n"] + 2 -> 3 [label="a & !b\\n"] + 2 -> 4 [label="a & b\\n"] + 3 [label="3", peripheries=2] + 3 -> 5 [label="!a\\n{Acc[1]}"] + 3 -> 6 [label="a\\n{Acc[1]}"] + 4 [label="5"] + 4 -> 1 [label="!b & !a\\n"] + 4 -> 5 [label="b & !a\\n"] + 4 -> 3 [label="a & !b\\n"] + 4 -> 6 [label="a & b\\n"] + 5 [label="4"] + 5 -> 1 [label="b & !a\\n"] + 5 -> 2 [label="!b & !a\\n"] + 5 -> 3 [label="a & b\\n"] + 5 -> 4 [label="a & !b\\n"] + 6 [label="6"] + 6 -> 1 [label="b & !a\\n"] + 6 -> 5 [label="!b & !a\\n"] + 6 -> 3 [label="a & b\\n"] + 6 -> 6 [label="a & !b\\n"] +} +#+end_example + +#+BEGIN_SRC dot :file gfaexxb4.png :cmdline -Tpng :var txt=gfaexxb4 :exports results +$txt +#+END_SRC +#+RESULTS: +[[file:gfaexxb4.png]] + + +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 +ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d' +#+END_SRC +#+RESULTS: +: states=4, det=0 + +The question, of course, is whether there exist a deterministic +automaton for this formula, in other words: is this a recurrence +property? There are two ways to answer this question using Spot (and +some help from [[http://www.ltl2dstar.de/][=ltl2dstar=]]). + +The first is purely syntactic. If a formula belongs to the class of +"syntactic recurrence formulas", it expresses a syntactic property. +(Of course there are formulas that expresses a syntactic properties +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 +ltlfilt --syntactic-recurrence -f "Ga R (F!b & (c U b))" +#+END_SRC +#+RESULTS: +: Ga R (F!b & (c U b)) + +Since our input formula was output, it expresses a recurrence property. + +The second way to check whether a formula is a recurrence is by +converting a deterministic Rabin automaton using [[file:dstar2tgba.org][=dstar2tgba=]]. The +output is guaranteed to be deterministic if and only if the input DRA +expresses a recurrence property. + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | +dstar2tgba -D --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' +#+END_SRC +#+RESULTS: +: input(states=11) output(states=9, acc-sets=1, det=1) + +In the above command, =ltlfilt= is used to convert the LTL formula +into =ltl2dstar='s syntax. Then =ltl2dstar= creates a deterministic +Rabin automaton (using =ltl2tgba= as an LTL to BA translator), and the +resulting 11-state DRA is converted into a 9-state DTBA by +=dstar2tgba=. Since that result is deterministic, we can conclude +that the formula was a recurrence. + +As far as SAT-based minimization goes, =dstar2tgba= will take the same +options as =ltl2tgba=, so we for instance check that the smallest DTBA +has 6 states: + +#+BEGIN_SRC sh :results verbatim :exports both +ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | +dstar2tgba -D -x sat-minimize --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' +#+END_SRC +#+RESULTS: +: input(states=11) output(states=6, acc-sets=1, det=1) + +* More acceptance sets + +The formula "=Ga R (F!b & (c 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 +acceptance set) before further processing, it does not know if using +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 +ltlfilt -f "Ga R (F!b & (c U b))" -l | +ltl2dstar --ltl2nba=spin:../../src/bin/ltl2tgba@-Ds - - | +dstar2tgba -D -x sat-minimize,sat-acc=2 --stats='input(states=%S) output(states=%s, acc-sets=%a, det=%d)' +#+END_SRC +#+RESULTS: +: input(states=11) output(states=5, acc-sets=2, det=1) + +Beware that the size of the SAT problem is exponential in the number of acceptance sets. + +The case of =ltl2tgba= is slightly different because it can remember +the number of acceptance sets used by the translation algorithm, and +reuse that for SAT-minimization even if the automaton had to be +degeneralized in the meantime for the purpose of determinization. + +* Low-level details + +The following figure gives an overview of the processing chains that +can be used to turn an LTL formula into a minimal DBA/DTBA/DTGBA. The +blue area at the top describes =ltl2tgba -D -x sat-minimize=, while +the purple area at the bottom corresponds to =dstar2tgba -D -x +stat-minimize=. + +[[file:satmin.png]] + +The picture is slightly inaccurate in the sense that both =ltl2tgba= +and =dstar2tgba= are actually using the same post-processing chain: +only the initial translation to TGBA or conversion to DBA differs, the +rest is the same. However in the case of =dstar2tgba=, no +degeneration or determinization are needed. + +Also the picture does not show what happens when =-B= is used: any +DTBA is degeneralized into a DBA, before being sent to "DTBA SAT +minimization", with a special option to request state-based output. + +The WDBA-minimization boxes are able to produce minimal Weak DBA from +any TGBA representing an obligation property. In that case using +transition-based or generalized acceptance will not allow further +reduction. This minimal WDBA is always used when =-D= is given +(otherwise, for the default =--small= option, the minimal WDBA is only +used if it is smaller than the nondeterministic automaton it has been +built from). + +The "simplify" boxes are actually simulation-based reductions, and +SCC-based simplifications. + +The red boxes "not in TCONG" or "not a recurrence" correspond to +situations where the tools will produce non-deterministic automata. + +The following options can be used to fine-tune this procedure: + +- =-x tba-det= :: attempt a powerset construction and check if + there exists a acceptance set such that the + resulting DTBA is equivalent to the input +- =-x sat-minimize= :: enable SAT-based minimization. By default it + tries to reduce the size of the automaton one state at a time. + This option implies =-x tba-det=. +- =-x sat-minimize=2= :: enabled SAT-based minimization, but perform a + dichotomy to locate the correct automaton size. Use this only if + you suspect that the optimal size is far away from the input + size. This option implies =-x tba-det=. +- =-x sat-acc=$m$= :: attempt to build a minimal DTGBA with $m$ acceptance sets. + This options implies =-x sat-minimize=. +- =-x sat-states=$n$= :: attempt to build an equivalent DTGBA with $n$ + states. This also implies =-x sat-minimize= but won't perform + any loop to lower the number of states. Note that $n$ should be + the number of states in a complete automaton, while =ltl2tgba= + and =dstar2tgba= both remove sink states in their output by + default (use option =--complete=) to output a complete automaton. + Also note that even with the =--complete= option, the output + automaton may have appear to have less states because the other + are unreachable. +- =-x state-based= :: for all outgoing transition of each state + to belong to the same acceptance sets. +- =-x !wdba-minimize= :: disable WDBA minimization. + +When options =-B= and =-x sat-minimize= both used, =-x state-based= and +=-x sat-acc=1= are implied. diff --git a/doc/org/satmin.tex b/doc/org/satmin.tex new file mode 100644 index 000000000..06b43e9d8 --- /dev/null +++ b/doc/org/satmin.tex @@ -0,0 +1,101 @@ +\documentclass[convert={size=640}]{standalone} +\usepackage{tikz} +\usetikzlibrary{arrows} +\usetikzlibrary{shadows} +\usetikzlibrary{positioning} +\usetikzlibrary{calc} +\usetikzlibrary{shapes} +\usetikzlibrary{patterns} +\usetikzlibrary{backgrounds} +\usetikzlibrary{shapes.callouts} +\newcommand{\CF}{\ensuremath{\mathcal{F}}} + +\newcommand{\pin}[1]{\tikz[baseline=0]\node[fill=yellow,draw,circle,thin,inner sep=0.5pt,above left] {\footnotesize #1};} + +\begin{document} + +\tikzstyle{dstep}=[align=center,minimum height=3em] +\tikzstyle{pstep}=[draw,dstep,drop shadow,fill=white] +\tikzstyle{iostep}=[dstep,rounded corners=1mm] +\tikzstyle{instep}=[iostep,fill=yellow!20] +\tikzstyle{outstep}=[iostep,fill=green!20] +\tikzstyle{errstep}=[iostep,fill=red!20] + +\begin{tikzpicture}[shorten >=1pt,>=stealth',semithick,node distance=5.5mm] +%\tikzset{callout/.style={ellipse callout, callout pointer arc=30, +% callout absolute pointer={#1},fill=blue!30,draw}} +%\tikzstyle{ + +\node[pstep] (trans) {translate\\to TGBA}; +\node[pstep,right=of trans.0,xshift=-2mm] (wdba) {attempt\\WDBA\\minim.}; +\draw[->] (trans) -- (wdba); +\node[pstep,right=of wdba.0] (simp) {simplify\\TGBA}; +\draw[->] (wdba) -- node[above]{fail} (simp); +\node[instep,below=of trans,yshift=-2mm] (ltl1) {LTL\\formula}; +\draw[->] (ltl1) -- (trans); + +\node[pstep,right=of simp,yshift=8mm,xshift=1mm] (degen) {degen\\to TBA}; +\draw[->] (simp) -- ($(simp.east)+(2mm,0mm)$) |- node[above left,align=right,at end]{nondet. or\\$|\CF|>m=1$} (degen); +\coordinate[pstep,right=of degen,yshift=-8mm,xshift=-1mm] (isdet); +%\coordinate[pstep,right=of degen,yshift=-2em] (isdet2); +\draw[->] (simp) -- ($(simp.east)+(2mm,0mm)$) -- node[below right,at start]{else} (isdet); +\coordinate (degen2) at ($(degen.east)+(2mm,0mm)$); +\draw[->] (degen) -- (degen2) -- ($(simp.east -| degen2)$); +\node[pstep,right=of degen,xshift=2.5em] (tbadet) {attempt\\ powerset\\to DTBA}; +\draw[->] (isdet) |- node[at end,above left]{nondet.} (tbadet); +\coordinate (tbadet2) at ($(tbadet.east)+(2mm,0mm)$); +\node[errstep,right=of tbadet.0,xshift=2mm,yshift=2mm] (nottcong) {not in\\$\mathsf{TCONG}$}; +\draw[->] (tbadet) -- node[at end,above left,align=center]{fail} ($(nottcong.180 |- tbadet)$); +\coordinate (turn) at ($(nottcong.-130 |- simp.0)$); +\draw[->] (isdet) -- node[below right,at start]{det.} (turn); +\draw[->] (tbadet2) -- node[right,pos=.6]{success} ($(tbadet2 |- turn)$); +\node[pstep,below=of tbadet.-125,yshift=-3mm] (dtbasat) {DTBA SAT\\minimization}; +\node[pstep,below=of dtbasat,yshift=5mm] (dtgbasat) {DTGBA SAT\\minimization}; +\draw[->] (turn) |- node[above left]{$m=1$} (dtbasat); +\draw[->] (turn) |- node[above left]{$m>1$} (dtgbasat); +\node[outstep,left=of dtgbasat] (mindtgba) {minimal\\DTGBA}; +\node[outstep] at ($(mindtgba |- dtbasat)$) (mindtba) {minimal\\DTBA}; +\node[outstep,left=of mindtba,xshift=5mm] (wdbaok) {minimal\\WDBA}; +\draw[->] (wdba) |- coordinate(c1) node[above right]{success} (wdbaok); + +\draw[->] (dtgbasat) -- (mindtgba); +\draw[->] (dtbasat) -- (mindtba); +\node[pstep,below=of ltl1,yshift=-2mm,xshift=1mm] (ltl2dstar) {\texttt{ltl2dstar}\\(DRA)}; +\draw[->] (ltl1) -- ($(ltl1 |- ltl2dstar.90)$); +\node[pstep,right=of ltl2dstar] (dra2dba) {attempt\\conversion\\to DBA}; +\draw[->] (ltl2dstar) -- (dra2dba); +\node[pstep,right=of dra2dba,xshift=3em] (wdba2) {attempt\\WDBA\\minim.}; +\node[pstep,right=of wdba2,xshift=2em] (simp2) {simplify as\\DBA or DTBA}; +\draw[->] (dra2dba) -- node[at start,below right]{success} (wdba2); +\draw[->] (wdba2) -- node[at start,below right]{fail} (simp2); +\coordinate (turn2) at ($(turn |- simp2)$); +\draw[->] (simp2) -- (turn2); +\draw[] (turn2) -- (turn); +\node[errstep] (notrec) at ($(ltl1 -| dra2dba)$) {not a\\ recurrence}; +\draw[->] (dra2dba) -- node[right]{fail} (notrec); +\draw[->] (wdba2.160) -| node[below right,sloped]{success} (wdbaok); + +\begin{scope}[on background layer] +\coordinate (pt1) at ($(tbadet.north east)+(3mm,2mm)$); +\coordinate (pt2) at ($(mindtba.north east)+(3mm,0mm)$); +\coordinate (pt3) at ($(mindtgba.south east)+(0mm,-1mm)$); +\coordinate[xshift=1mm,yshift=1mm] (turn3) at (turn); +\path[pattern color=blue!30,pattern=north west lines] ($(trans.west |- pt1)$) |- (pt2) |- (pt3) -| (turn3) -| (pt1) -- cycle; +\node[below right] at ($(trans.west |- pt1)$) {\texttt{ltl2tgba}}; + + +\coordinate[yshift=1mm,xshift=1mm] (pt4) at ($(pt2 -| turn3)$); +\coordinate[yshift=-3mm,xshift=-1mm] (pt5) at ($(dra2dba.south west)$); +\coordinate[yshift=1mm,xshift=-1mm] (pt6) at ($(dra2dba.north west)$); +\path[pattern color=blue!30!red!30,pattern=north east lines] (pt5) -| (pt4) -- ($(pt2) + (1mm,1mm)$) |- (pt6) -- cycle; +\node[above left,yshift=-1mm] at ($(pt5 -| pt4)$) {\texttt{dstar2tgba}}; +\end{scope} + +%\node[fill=yellow,draw,ellipse callout,thin,inner sep=0.5pt,callout pointer arc=30,,yshift=6mm,callout absolute pointer={(c1)}] at (c1) {\footnotesize 1}; + +\end{tikzpicture} +\end{document} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/doc/org/tools.org b/doc/org/tools.org index 6d332eb51..67b54710b 100644 --- a/doc/org/tools.org +++ b/doc/org/tools.org @@ -44,6 +44,10 @@ corresponding commands are hidden. - [[file:dstar2tgba.org][=dstar2tgba=]] Convert deterministic Rabin or Streett automata into Büchi automata. +* Advanced uses + +- [[file:satmin.org][SAT-based minimization of Deterministic (Generalized) Büchi automata]] + # LocalWords: num toc helloworld SRC LTL PSL randltl ltlfilt genltl # LocalWords: scalable ltl tgba Büchi automata tgta ltlcross eval # LocalWords: setenv concat getenv setq