diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 208c6d41a..55fd17a8e 100644 --- a/bin/ltlsynt.cc +++ b/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; diff --git a/bin/spot-x.cc b/bin/spot-x.cc index c4905c2e9..9ab5f5e57 100644 --- a/bin/spot-x.cc +++ b/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 } }; diff --git a/doc/Makefile.am b/doc/Makefile.am index 717a4275d..09444187a 100644 --- a/doc/Makefile.am +++ b/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 $@ diff --git a/doc/org/ltlsynt.org b/doc/org/ltlsynt.org index af1bcba9f..da80dc9ce 100644 --- a/doc/org/ltlsynt.org +++ b/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 -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. +#+NAME: exampledot +#+BEGIN_SRC sh :exports none :noweb yes +sed 1d <> +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 -parity game is described in the following paper: -- *Reactive Synthesis from LTL Specification with Spot*, /Thibaud Michaud/, - /Maximilien Colange/. In Proc. of SYNT@CAV'18. to appear. +game using Zielonka's recursive algorithm. The process can be pictured as follows. + +[[file:ltlsynt.svg]] + +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 -=--print-pg=. Note that this flag deactivates the resolution of the parity -game, which is to be deferred to one of the solvers from PGSolver. +[[https://github.com/tcsprojects/pgsolver][PGSolver]] format, with the flag =--print-pg=, or in the HOA format, +using =--print-game-hoa=. These flag deactivate the resolution of the +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 diff --git a/doc/org/ltlsynt.tex b/doc/org/ltlsynt.tex new file mode 100644 index 000000000..ad9dac962 --- /dev/null +++ b/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}