ltlsynt: improve documentation

This addresses a few points from #479.

* doc/org/ltlsynt.tex: New file.
* doc/Makefile.am: Add it.
* doc/org/ltlsynt.org: Show the architecture, and mention more
options.
* bin/spot-x.cc: Document ltlsynt's -x options.
* bin/ltlsynt.cc: Fix default value of --aiger, and typo in its
documentation.

bin/ltlsynt.cc

@@ -91,7 +91,7 @@ static const argp_option options[] =
       "\"isop\" for irreducible sum of producs; "
       "\"both\" tries both encodings and keeps the smaller one. "
       "The other options further "
-      "refine the encoding, see aiger:::encode_bdd.", 0},
+      "refine the encoding, see aiger::encode_bdd.", 0},
     { "verbose", OPT_VERBOSE, nullptr, 0,
       "verbose mode", -1 },
     { "verify", OPT_VERIFY, nullptr, 0,
@@ -594,7 +594,7 @@ parse_opt(int key, char *arg, struct argp_state *)
       opt_print_hoa_args = arg;
       break;
     case OPT_PRINT_AIGER:
-      opt_print_aiger = arg ? arg : "INF";
+      opt_print_aiger = arg ? arg : "ite";
       break;
     case OPT_REAL:
       opt_real = true;

bin/spot-x.cc

@@ -237,6 +237,20 @@ sets.  By default this is only enabled when options -B or -S are used.") },
           "Chose which simulation based reduction to use: 1 force the \
 signature-based BDD implementation, 2 force matrix-based and 0, the default, \
 is a heristic wich choose which implementation to use.") },
+    { nullptr, 0, nullptr, 0, "Synthesis options:", 0 },
+    { DOC("specification-decomposition",
+          "Set to 0 to disable specification decomposition.  Default is 1.") },
+    { DOC("minimization-level",
+          "Specify how AIGER circuits should be simplified.  "
+          "(0) no simplification, "
+          "(1) bisimulation-based reduction, "
+          "(2) simplification using language inclusion and output assignments, "
+          "(3) exact minimization using a SAT solver, "
+          "(4) bisimulation-based reduction before exact minimization via "
+          "SAT solver, "
+          "(5) simplification using output assignments before exact "
+          "minimization via SAT solver.  "
+          "The default value is 1.") },
     { nullptr, 0, nullptr, 0, nullptr, 0 }
   };
 

doc/Makefile.am

@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2010-2011, 2013-2020 Laboratoire de Recherche et
+## Copyright (C) 2010-2011, 2013-2021 Laboratoire de Recherche et
 ## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003-2005 Laboratoire d'Informatique de Paris 6
 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -103,6 +103,7 @@ ORG_FILES = \
   org/ltlfilt.org \
   org/ltlgrind.org \
   org/ltlsynt.org \
+  org/ltlsynt.tex \
   org/oaut.org \
   org/randaut.org \
   org/randltl.org \
@@ -136,6 +137,7 @@ ORG_FILES = \
 PICTURES_EXTRA = \
   $(srcdir)/org/arch.svg \
   $(srcdir)/org/hierarchy.svg \
+  $(srcdir)/org/ltlsynt.svg \
   $(srcdir)/org/satmin.svg
 
 $(srcdir)/org/satmin.svg: org/satmin.tex
@@ -156,6 +158,12 @@ $(srcdir)/org/hierarchy.svg: org/hierarchy.tex
 	pdf2svg hierarchy.pdf hierarchy.svg && \
 	rm -f hierarchy.pdf hierarchy.aux hierarchy.log
 
+$(srcdir)/org/ltlsynt.svg: org/ltlsynt.tex
+	cd $(srcdir)/org && \
+	pdflatex ltlsynt.tex && \
+	pdf2svg ltlsynt.pdf ltlsynt.svg && \
+	rm -f ltlsynt.pdf ltlsynt.aux ltlsynt.log
+
 $(srcdir)/org-stamp: $(ORG_FILES) $(configure_ac)
 	$(MAKE) org && touch $@
 

doc/org/ltlsynt.org

@@ -11,11 +11,16 @@ This tool synthesizes controllers from LTL/PSL formulas.
 
 Consider a set $I$ of /input/ atomic propositions, a set $O$ of output atomic
 propositions, and a PSL formula \phi over the propositions in $I \cup O$.  A
-=controller= realizing \phi is a function $c: 2^{I \cup O} \times 2^I \mapsto
+=controller= realizing \phi is a function $c: (2^{I})^\star \times 2^I \mapsto
 2^O$ such that, for every \omega-word $(u_i)_{i \in N} \in (2^I)^\omega$ over
 the input propositions, the word $(u_i \cup c(u_0 \dots u_{i-1}, u_i))_{i \in
 N}$ satisfies \phi.
 
+If a controller exists, then one with finite memory exists. Such controllers
+are easily represented as automata (or more specifically as I/O automata or
+transducers).  In the automaton representing the controller, the acceptance
+condition is irrelevant and trivially true.
+
 =ltlsynt= has three mandatory options:
 - =--ins=: a comma-separated list of input atomic propositions;
 - =--outs=: a comma-separated list of output atomic propositions;
@@ -27,23 +32,25 @@ as input can be assumed to be an output and vice-versa.
 The following example illustrates the synthesis of a controller acting as an
 =AND= gate. We have two inputs =a= and =b= and one output =c=, and we want =c=
 to always be the =AND= of the two inputs:
+
+#+NAME: example
 #+BEGIN_SRC sh :exports both
 ltlsynt --ins=a,b -f 'G (a & b <=> c)'
 #+END_SRC
 
-#+RESULTS:
+#+RESULTS: example
 #+begin_example
 REALIZABLE
 HOA: v1
 States: 1
 Start: 0
-AP: 3 "b" "c" "a"
+AP: 3 "a" "b" "c"
 acc-name: all
 Acceptance: 0 t
 properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0
-[!0&!1 | !1&!2] 0
+[!0&!2 | !1&!2] 0
 [0&1&2] 0
 --END--
 #+end_example
@@ -54,10 +61,22 @@ The output is composed of two parts:
   In this example, the controller has a single
   state, with two loops labeled by =a & b & c= and =(!a | !b) & !c=.
 
-If a controller exists, then one with finite memory exists. Such controllers
+#+NAME: exampledot
-are easily represented as automata (or more specifically as I/O automata or
+#+BEGIN_SRC sh :exports none :noweb yes
-transducers).  In the automaton representing the controller, the acceptance
+sed 1d <<EOF | autfilt --dot=.A
-condition is irrelevant and trivially true.
+<<example()>>
+EOF
+#+END_SRC
+
+#+BEGIN_SRC dot :file ltlsyntex.svg :var txt=exampledot :exports results
+  $txt
+#+END_SRC
+
+#+RESULTS:
+[[file:ltlsyntex.svg]]
+
+The label =a & b & c= should be understood as: "if the input is =a&b=,
+the output should be =c=".
 
 The following example illustrates the case of an unrealizable specification. As
 =a= is an input proposition, there is no way to guarantee that it will
@@ -70,7 +89,6 @@ ltlsynt --ins=a -f 'F a'
 #+RESULTS:
 : UNREALIZABLE
 
-
 By default, the controller is output in HOA format, but it can be
 output as an [[http://fmv.jku.at/aiger/][AIGER]] circuit thanks to the =--aiger= flag. This is the
 output format required for the [[http://syntcomp.org/][SYNTCOMP]] competition.
@@ -96,18 +114,74 @@ OUT=$(syfco FILE --print-output-signals)
 ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"
 #+END_SRC
 
-* Algorithm
+* Internal details
 
 The tool reduces the synthesis problem to a parity game, and solves the parity
-game using Zielonka's recursive algorithm.  The full reduction from LTL to
+game using Zielonka's recursive algorithm.  The process can be pictured as follows.
-parity game is described in the following paper:
+
-- *Reactive Synthesis from LTL Specification with Spot*, /Thibaud Michaud/,
+[[file:ltlsynt.svg]]
-  /Maximilien Colange/.  In Proc. of SYNT@CAV'18. to appear.
+
+LTL decomposition is described by [[https://arxiv.org/abs/2103.08459][Finkbeiner, Geier, and Passing]], and
+can be disabled by passing option =-x specification-decomposition=0=.
+The idea is to split the specification into multiple smaller
+constraints on disjoint subsets of the output values, solve those
+constraints separately, and then combine them while encoding the AIGER
+circuit.
+
+The ad hoc construction on the top is just a shortcut for some type of
+constraints that can be solved directly by converting the constraint
+into a DBA.
+
+Otherwise, conversion to parity game (represented by the blue zone) is
+done using one of several algorithms specified by the =--algo= option.
+The game is then solved, producing a strategy if the game is realizable.
+
+If an =ltlsynt= is in =--realizability= mode, the process stops here
+
+In =--aiger= mode, the strategy is first simplified.  How this is done
+is controled by option =-x minimize-level=N=.  See the [[./man/spot-x.7.html][=spot-x=]](7)
+manpage for details.
+Finally, the strategy is encoded into [[http://fmv.jku.at/aiger/][AIGER]].  The =--aiger= option can
+take an argument to specify a type of encoding to use: by default
+it is =ite= for if-then-else, because it follows the structure of BDD
+used to encode the conditions in the strategy.  An alternative encoding
+is =isop= where condition are first put into irredundant-sum-of-product,
+or =both= if both encodings should be tried.  Additionally, these optiosn
+can accept the suffix =+ud= (use dual) to attempt to encode each condition
+and its negation and keep the smallest one, =+dc= (don't care) to take
+advantage of /don't care/ values in the output, and one of =+sub0=,
+=+sub1=, or =+sub2= to test various grouping of variables in the encoding.
+Multiple encodings can be tried by separating them using commas.
+For instance =--aiger=isop,isop+dc,isop+ud= will try three different encodings.
+
+* Other useful options
 
 You can also ask =ltlsynt= to print to obtained parity game into
-[[https://github.com/tcsprojects/pgsolver][PGSolver]] format, with the flag
+[[https://github.com/tcsprojects/pgsolver][PGSolver]] format, with the flag =--print-pg=, or in the HOA format,
-=--print-pg=.  Note that this flag deactivates the resolution of the parity
+using =--print-game-hoa=.  These flag deactivate the resolution of the
-game, which is to be deferred to one of the solvers from PGSolver.
+parity game.
+
+For benchmarking purpose, the =--csv= option can be used to record
+intermediate statistics about the resolution.
+
+The =--verify= option requests that the produced strategy or aiger
+circuit are compatible with the specification.  This is done by
+ensuring that they do not intersect the negation of the specification.
+
+* References
+
+The initial reduction from LTL to parity game is described in the
+following paper:
+
+- *Reactive Synthesis from LTL Specification with Spot*, /Thibaud Michaud/,
+  /Maximilien Colange/.  Presented in SYNT@CAV'18.  ([[https://www.lrde.epita.fr/dload/papers/michaud.18.synt.pdf][pdf]] | [[https://www.lrde.epita.fr/~max/bibtexbrowser.php?key=michaud.18.synt&bib=perso.bib][bib]])
+
+Further improvements are described in the following paper:
+
+- *Improvements to =ltlsynt=*, /Florian Renkin/, /Philipp Schlehuber/,
+  /Alexandre Duret-Lutz/, and /Adrien Pommellet/.  Presented at the
+  SYNT'21 workshop.  ([[https://www.lrde.epita.fr/~adl/dl/adl/renkin.21.synt.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#renkin.21.synt][bib]])
+
 
 #  LocalWords:  utf ltlsynt AIGER html args mapsto SRC acc aiger TLSF
 #  LocalWords:  UNREALIZABLE unrealizable SYNTCOMP realizability Proc

doc/org/ltlsynt.tex

@@ -0,0 +1,113 @@
+\documentclass{standalone}
+\usepackage{tikz}
+\usetikzlibrary{arrows}
+\usetikzlibrary{arrows.meta}
+\usetikzlibrary{bending}
+\usetikzlibrary{shadows}
+\usetikzlibrary{positioning}
+\usetikzlibrary{calc}
+\usetikzlibrary{decorations.text}
+\usetikzlibrary{backgrounds}
+\usepackage[hidelinks]{hyperref}
+
+\begin{document}
+\scalebox{1.2}{
+  \begin{tikzpicture}[thick,font=\sffamily,>={Stealth[round,bend]},
+                      node distance=4mm and 5mm,
+                      data/.style={text width=1.3cm,minimum height=2em,align=center,draw,fill=magenta!15},
+                      wproc/.style={fill=yellow!20,align=center,draw,rounded corners=2mm},
+                      proc/.style={wproc,text width=1.5cm,minimum height=2em},
+                      lproc/.style={proc,text width=2cm},
+                      choice/.style={circle,fill=yellow!20,inner sep=0,minimum size=2mm,draw},
+                      algoopt/.style={postaction={decorate,decoration={text along path, raise=1mm,text={|\ttfamily\small|#1}}}},
+                      outopt/.style={postaction={decorate,decoration={text along path, text align=right,raise=1mm,text={|\ttfamily\small|#1}}}},
+                      ]
+    \node[proc] (transSD) {translate to NBA};
+    \node[proc,right=of transSD] (splitSD) {split I/O};
+    \node[lproc,right=of splitSD] (detSD) {determinize to DPA};
+    \draw[->] (transSD) edge (splitSD)
+              (splitSD) edge (detSD);
+    \node[proc,below=of transSD] (transDS) {translate to NBA};
+    \node[lproc,right=of transDS] (detDS) {determinize to DPA};
+    \node[proc,right=of detDS,xshift=2mm] (splitDS) {split I/O};
+    \draw[->] (transDS) edge (detDS)
+              (detDS) edge coordinate(middetsplit) (splitDS);
+    \node[proc,below=of transDS] (transLARold) {translate to DELA};
+    \node[lproc,right=of transLARold] (paritizeLARold) {paritize (pure CAR)};
+    \draw[->] (transLARold) edge (paritizeLARold)
+              (paritizeLARold) edge (middetsplit |- paritizeLARold);
+    \node[proc,below=of transLARold] (transLAR) {translate to DELA};
+    \node[lproc,right=of transLAR] (paritizeLAR) {paritize (CAR,IAR,{\tiny ...})};
+    \draw[->] (transLAR) edge (paritizeLAR)
+              (paritizeLAR) edge (middetsplit |- paritizeLAR);
+    \node[proc,below=of transLAR] (transPS) {translate to DPA};
+    \draw[rounded corners,->] (transPS) -| (middetsplit);
+    \coordinate (choicecenter) at ($(current bounding box.west) - (3.3cm,0)$);
+    \path[draw] (choicecenter) node[choice](algoin){}
+          +(60:8mm) node[choice](algosd){}
+          +(30:8mm) node[choice](algods){}
+          +(0:8mm) node[choice](algolarold){}
+          +(-30:8mm) node[choice](algolar){}
+          +(-60:8mm) node[choice](algops){};
+
+    \draw[->,algoopt={-{}-algo=sd}] (algosd) to[out=60,in=180] (transSD);
+    \draw[->,algoopt={-{}-algo=ds}] (algods) to[out=30,in=180] (transDS);
+    \draw[->,algoopt={-{}-algo=lar.old}] (algolarold) -- (transLARold);
+    \draw[->,algoopt={-{}-algo=lar}] (algolar) to[out=-30,in=180] (transLAR);
+    \draw[->,algoopt={-{}-algo=ps}] (algops) to[out=-60,in=180] (transPS);
+    \draw[ultra thick] (algoin) -- (algolar.north);
+
+    \node[choice,left=of algoin] (bypassin) {};
+    \node[proc,left=of bypassin,yshift=1cm,text width=1.6cm] (decomp) {decompose};
+    \node[data,above=of decomp] (input) {LTL input};
+    \draw[->] (input) -- (decomp);
+    \draw[->] (decomp) to[out=-45,in=180] (bypassin);
+    \draw[->,gray] (decomp) to[out=-55,in=180] ($(bypassin.west)+(0,-0.33)$);
+    \draw[->,gray] (decomp) to[out=-65,in=180] ($(bypassin.west)+(0,-0.66)$);
+    \draw[->,gray] (decomp) to[out=-75,in=180] ($(bypassin.west)+(0,-1)$);
+    \draw[->] (bypassin) -- (algoin);
+
+    \node[lproc, right=of detSD, xshift=4mm] (solve) {solve\linebreak parity game};
+
+    \node[below=of solve,choice] (reachoice) {};
+    \node[below right=of reachoice,choice,xshift=-3mm,yshift=-1mm] (realize) {};
+    \node[below left=of reachoice,choice,xshift=3mm,yshift=-1mm] (aiger) {};
+    \draw[ultra thick] (reachoice) -- (realize.west);
+    \draw[->] (solve) -- (reachoice);
+
+
+    \node[data] (yesno) at ($(transPS -| realize)+(0,-2mm)$) {Y/N output};
+    \node[data, text width=1.2cm, left=of yesno] (output) {AIGER output};
+    \node[proc, above=of output,yshift=-1mm] (encode) {encode in AIGER};
+    \node[proc, above=of encode,yshift=+1mm] (minimize) {simplify\linebreak strategy};
+
+    \draw[->] (detSD) -- coordinate(middetsolve) (solve);
+    \draw[rounded corners,->] (splitDS) -| (middetsolve);
+
+    \draw[<-,outopt={-{}-aiger}] (minimize) to[out=90,in=-160]  (aiger);
+    \draw[->] (minimize) -- (encode);
+    \draw[gray,->] ($(encode.north)+(2mm,3mm)$) -- ($(encode.north)+(2mm,0)$);
+    \draw[gray,->] ($(encode.north)+(4mm,3mm)$) -- ($(encode.north)+(4mm,0)$);
+    \draw[gray,->] ($(encode.north)+(6mm,3mm)$) -- ($(encode.north)+(6mm,0)$);
+    \draw[<-,outopt={-{}-realizability~}] (yesno) -- (realize);
+    \draw[gray,->] ($(yesno.north)+(2mm,3mm)$) -- ($(yesno.north)+(2mm,0)$);
+    \draw[gray,->] ($(yesno.north)+(4mm,3mm)$) -- ($(yesno.north)+(4mm,0)$);
+    \draw[gray,->] ($(yesno.north)+(6mm,3mm)$) -- ($(yesno.north)+(6mm,0)$);
+
+    %\draw[->] (solve) -- (encode);
+    \draw[->] (encode) -- (output);
+
+  \begin{scope}[on background layer,overlay]
+    \fill[cyan!20,rounded corners=5mm]
+    ($(algoin |- transPS.south)+(-.4,-.2)$) |-
+    ($(detSD.north -| middetsolve)+(.2,.2)$) |-
+    ($(splitDS.south west)+(.2,-.2)$) |- cycle;
+  \end{scope}
+
+  \coordinate (solveright) at ($(solve.east)+(2mm,0)$);
+  \path (bypassin) -- coordinate(medblue) (solveright);
+  \node[wproc,above,xshift=-1mm,yshift=4mm] (bypass) at (medblue |- detSD.north) {specialized strategy construction for formulas of the form $\mathsf{G}(b_1) \land (\varphi \leftrightarrow \mathsf{G}\mathsf{F} b_2)$};
+  \draw[rounded corners,->] (bypassin) |- (bypass);
+  \draw[rounded corners,->] (bypass) -| (solveright) |- (reachoice);
+  \end{tikzpicture}}
+\end{document}