1b69ed96f9
* bin/ltlsynt.cc: Implement it. * NEWS, doc/org/ltlsynt.org: Document it. * tests/core/ltlsynt.test: Test it.
115 lines
4.4 KiB
Org Mode
115 lines
4.4 KiB
Org Mode
# -*- coding: utf-8 -*-
|
|
#+TITLE: =ltlsynt=
|
|
#+DESCRIPTION: Spot command-line tool for synthesizing AIGER circuits from LTL/PSL formulas.
|
|
#+INCLUDE: setup.org
|
|
#+HTML_LINK_UP: tools.html
|
|
#+PROPERTY: header-args:sh :results verbatim :exports both
|
|
|
|
* Basic usage
|
|
|
|
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
|
|
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.
|
|
|
|
=ltlsynt= has three mandatory options:
|
|
- =--ins=: a comma-separated list of input atomic propositions;
|
|
- =--outs=: a comma-separated list of output atomic propositions;
|
|
- =--formula= or =--file=: a specification in LTL or PSL.
|
|
|
|
One of =--ins= or =--outs= may be omitted, as any atomic proposition not listed
|
|
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:
|
|
#+BEGIN_SRC sh :exports both
|
|
ltlsynt --ins=a,b -f 'G (a & b <=> c)'
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
#+begin_example
|
|
REALIZABLE
|
|
HOA: v1
|
|
States: 1
|
|
Start: 0
|
|
AP: 3 "b" "c" "a"
|
|
acc-name: all
|
|
Acceptance: 0 t
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
--BODY--
|
|
State: 0
|
|
[!0&!1 | !1&!2] 0
|
|
[0&1&2] 0
|
|
--END--
|
|
#+end_example
|
|
|
|
The output is composed of two parts:
|
|
- the first one is a single line =REALIZABLE= or =UNREALIZABLE;=
|
|
- the second one, only present in the =REALIZABLE= case is an automaton describing the controller.
|
|
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.
|
|
|
|
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
|
|
eventually hold.
|
|
|
|
#+BEGIN_SRC sh :epilogue true
|
|
ltlsynt --ins=a -f 'F a'
|
|
#+END_SRC
|
|
|
|
#+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.
|
|
|
|
The generation of a controller can be disabled with the flag =--realizability=.
|
|
In this case, =ltlsynt= output is limited to =REALIZABLE= or =UNREALIZABLE=.
|
|
|
|
* TLSF
|
|
|
|
=ltlsynt= was made with the [[http://syntcomp.org/][SYNTCOMP]] competition in mind, and more
|
|
specifically the TLSF track of this competition. TLSF is a high-level
|
|
specification language created for the purpose of this competition.
|
|
Fortunately, the SYNTCOMP organizers also provide a tool called
|
|
[[https://github.com/reactive-systems/syfco][=syfco=]] which can translate a TLSF specification to an LTL formula.
|
|
|
|
The following four steps show you how a TLSF specification called =FILE= can
|
|
be synthesized using =syfco= and =ltlsynt=:
|
|
|
|
#+BEGIN_SRC sh :export code
|
|
LTL=$(syfco FILE -f ltlxba -m fully)
|
|
IN=$(syfco FILE --print-input-signals)
|
|
OUT=$(syfco FILE --print-output-signals)
|
|
ltlsynt --formula="$LTL" --ins="$IN" --outs="$OUT"
|
|
#+END_SRC
|
|
|
|
* Algorithm
|
|
|
|
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.
|
|
|
|
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.
|
|
|
|
# LocalWords: utf ltlsynt AIGER html args mapsto SRC acc aiger TLSF
|
|
# LocalWords: UNREALIZABLE unrealizable SYNTCOMP realizability Proc
|
|
# LocalWords: syfco ltlxba Zielonka's Thibaud Michaud Maximilien
|
|
# LocalWords: Colange PGSolver
|