ltlsynt: add options --dot and --hide-status
* bin/ltlsynt.cc: Implement these options. * bin/common_aoutput.hh, bin/common_aoutput.cc (automaton_format_opt): Make extern. * NEWS: Mention the new options. * doc/org/ltlsynt.org: Use dot output in documentation. * tests/core/ltlsynt.test: Quick test of the new options.
This commit is contained in:
Alexandre Duret-Lutz
parent
ef0aeed228
commit
c1c874b1a5
6 changed files with 205 additions and 67 deletions
|
|
@ -7,19 +7,19 @@
|
|||
|
||||
* Basic usage
|
||||
|
||||
This tool synthesizes controllers from LTL/PSL formulas.
|
||||
This tool synthesizes reactive 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})^\star \times 2^I \mapsto
|
||||
*reactive 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.
|
||||
If a reactive controller exists, then one with finite memory
|
||||
exists. Such controllers are easily represented as automata (or more
|
||||
specifically as Mealy machines). 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;
|
||||
|
|
@ -27,45 +27,52 @@ condition is irrelevant and trivially true.
|
|||
- =--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.
|
||||
as input can be assumed to be 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:
|
||||
The following example illustrates the synthesis of a controller
|
||||
ensuring that input =i1= and =i2= are both true initially if and only
|
||||
if eventually output =o1= will go from true to false at some point.
|
||||
Note that this is an equivalence, not an implication.
|
||||
|
||||
#+NAME: example
|
||||
#+BEGIN_SRC sh :exports both
|
||||
ltlsynt --ins=a,b -f 'G (a & b <=> c)'
|
||||
ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: example
|
||||
#+begin_example
|
||||
REALIZABLE
|
||||
HOA: v1
|
||||
States: 1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 3 "a" "b" "c"
|
||||
AP: 3 "i1" "i2" "o1"
|
||||
acc-name: all
|
||||
Acceptance: 0 t
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
controllable-AP: 2
|
||||
--BODY--
|
||||
State: 0
|
||||
[!0&!2 | !1&!2] 0
|
||||
[0&1&2] 0
|
||||
[0&1&2] 1
|
||||
[!0&2 | !1&2] 2
|
||||
State: 1
|
||||
[!2] 0
|
||||
State: 2
|
||||
[2] 2
|
||||
--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=.
|
||||
- The first one is a single line =REALIZABLE= or =UNREALIZABLE=; the presence of this
|
||||
line, required by the [[http://http://www.syntcomp.org/][SyntComp competition]], can be disabled with option =--hide-status=.
|
||||
- The second one, only present in the =REALIZABLE= case, is an automaton describing the controller.
|
||||
|
||||
The controller contains the line =controllable-AP: 2=, which means that this automaton
|
||||
should be interpreted as a Mealy machine where =o0= is part of the output.
|
||||
Using the =--dot= option, makes it easier to visualize this machine.
|
||||
|
||||
#+NAME: exampledot
|
||||
#+BEGIN_SRC sh :exports none :noweb yes
|
||||
sed 1d <<EOF | autfilt --dot=.A
|
||||
<<example()>>
|
||||
EOF
|
||||
#+BEGIN_SRC sh :exports code
|
||||
ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --hide-status --dot
|
||||
#+END_SRC
|
||||
|
||||
#+BEGIN_SRC dot :file ltlsyntex.svg :var txt=exampledot :exports results
|
||||
|
|
@ -75,9 +82,6 @@ EOF
|
|||
#+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
|
||||
eventually hold.
|
||||
|
|
@ -90,11 +94,68 @@ ltlsynt --ins=a -f 'F a'
|
|||
: 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.
|
||||
output as an And-Inverter-Graph in [[http://fmv.jku.at/aiger/][AIGER format]] using 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=.
|
||||
#+NAME: exampleaig
|
||||
#+BEGIN_SRC sh :exports both
|
||||
ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --aiger
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: exampleaig
|
||||
#+begin_example
|
||||
REALIZABLE
|
||||
aag 14 2 2 1 10
|
||||
2
|
||||
4
|
||||
6 14
|
||||
8 29
|
||||
7
|
||||
10 7 9
|
||||
12 4 10
|
||||
14 2 12
|
||||
16 7 8
|
||||
18 4 16
|
||||
20 5 7
|
||||
22 21 19
|
||||
24 2 23
|
||||
26 3 7
|
||||
28 27 25
|
||||
i0 i1
|
||||
i1 i2
|
||||
o0 o1
|
||||
#+end_example
|
||||
|
||||
The above format is not very human friendly. Again, by passing both
|
||||
=--aiger= and =--dot=, one can display the And-Inverter-Graph representing
|
||||
the controller:
|
||||
|
||||
#+NAME: exampleaigdot
|
||||
#+BEGIN_SRC sh :exports code
|
||||
ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --hide-status --aiger --dot
|
||||
#+END_SRC
|
||||
|
||||
#+BEGIN_SRC dot :file ltlsyntexaig.svg :var txt=exampleaigdot :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
[[file:ltlsyntexaig.svg]]
|
||||
|
||||
In the above diagram, round nodes represent AND gates. Small black
|
||||
circles represent inversions (or negations), colored triangles are
|
||||
used to represent input signals (at the bottom) and output signals (at
|
||||
the top), and finally rectangles represent latches. A latch is a one
|
||||
bit register that delays the signal by one step. Initially, all
|
||||
latches are assumed to contain =false=, and them emit their value from
|
||||
the =L0_out= and =L1_out= rectangles at the bottom. Their input value,
|
||||
to be emitted at the next step, is received via the =L0_in= and =L1_in=
|
||||
boxes at the top. In =ltlsynt='s encoding, the set of latches is used
|
||||
to keep track of the current state of the Mealy machine.
|
||||
|
||||
The generation of a controller can be disabled with the flag
|
||||
=--realizability=. In this case, =ltlsynt='s output is limited to
|
||||
=REALIZABLE= or =UNREALIZABLE=.
|
||||
|
||||
* TLSF
|
||||
|
||||
|
|
@ -177,7 +238,18 @@ be tried by separating them using commas. For instance
|
|||
You can also ask =ltlsynt= to print to obtained parity game into
|
||||
[[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.
|
||||
parity game. Note that if any of those flag is used with =--dot=, the game
|
||||
will be printed in the Dot format instead:
|
||||
|
||||
#+NAME: examplegamedot
|
||||
#+BEGIN_SRC sh :exports code
|
||||
ltlsynt --ins=i1,i2 -f '(i1 & i2) <-> F(o1 & X(!o1))' --print-game-hoa --dot
|
||||
#+END_SRC
|
||||
#+BEGIN_SRC dot :file ltlsyntexgame.svg :var txt=examplegamedot :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
[[file:ltlsyntexgame.svg]]
|
||||
|
||||
For benchmarking purpose, the =--csv= option can be used to record
|
||||
intermediate statistics about the resolution.
|
||||
|
|
@ -200,6 +272,11 @@ Further improvements are described in the following paper:
|
|||
/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]])
|
||||
|
||||
Simplification of Mealy machines is discussed in:
|
||||
|
||||
- *Effective reductions of Mealy machines*, /Florian Renkin/,
|
||||
/Philipp Schlehuber-Caissier/, /Alexandre Duret-Lutz/, and /Adrien Pommellet/.
|
||||
Presented at FORTE'22. ([[https://www.lrde.epita.fr/~adl/dl/adl/renkin.22.forte.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#renkin.22.forte][bib]])
|
||||
|
||||
# LocalWords: utf ltlsynt AIGER html args mapsto SRC acc aiger TLSF
|
||||
# LocalWords: UNREALIZABLE unrealizable SYNTCOMP realizability Proc
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue