1724d2b14c
* bin/ltlsynt.cc: Honnor -q properly. * doc/org/ltlsynt.org, tests/core/ltlsynt.test: Adjust. * NEWS: Mention this bug.
454 lines
28 KiB
Org Mode
454 lines
28 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 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
|
|
*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 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.
|
|
|
|
Here is a small example where $I=\{i_1,i_2\}$ and $O=\{o_1\}$. The
|
|
specification asks that $o_1$ hold at some point if and only if $i_1$
|
|
and $i_2$ hold one after the other at some point.
|
|
|
|
#+NAME: example
|
|
#+BEGIN_SRC sh :exports both
|
|
ltlsynt -f 'F(i1 & Xi2) <-> F(o1)'
|
|
#+END_SRC
|
|
|
|
#+RESULTS: example
|
|
#+begin_example
|
|
REALIZABLE
|
|
HOA: v1
|
|
States: 2
|
|
Start: 0
|
|
AP: 3 "i1" "o1" "i2"
|
|
acc-name: all
|
|
Acceptance: 0 t
|
|
properties: trans-labels explicit-labels state-acc deterministic
|
|
controllable-AP: 1
|
|
--BODY--
|
|
State: 0
|
|
[!0&!1] 0
|
|
[0&!1] 1
|
|
State: 1
|
|
[!0&!1&!2] 0
|
|
[0&!1&!2] 1
|
|
[1&2] 1
|
|
--END--
|
|
#+end_example
|
|
|
|
The output is composed of two parts:
|
|
- The first part is a single line stating =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 part, 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 code
|
|
ltlsynt -f 'F(i1 & Xi2) <-> F(o1)' --hide-status --dot
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC dot :file ltlsyntex.svg :var txt=exampledot :exports results
|
|
$txt
|
|
#+END_SRC
|
|
|
|
#+RESULTS:
|
|
[[file:ltlsyntex.svg]]
|
|
|
|
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
|
|
|
|
* Input options
|
|
:PROPERTIES:
|
|
:CUSTOM_ID: input-options
|
|
:END:
|
|
|
|
=ltlsynt= require two pieces of information two solve a reactive
|
|
LTL/PSL synthesis problem: an LTL (or PSL) formula, and a partition of
|
|
its atomic propositions as input and output.
|
|
|
|
The specification formula can be passed with =-f/--formula= or
|
|
=-F/--file=. If multiple specifications formulas are passed, they
|
|
will all be solved individually.
|
|
|
|
The input/output partition can be given in several ways. If it is
|
|
not specified, =ltlsynt= assumes that input variables should start
|
|
with =i=, and output variables should start with =o=.
|
|
|
|
Options =--ins= and =--outs= should be followed by a comma-separated
|
|
list of input atomic propositions, or input regexes enclosed in
|
|
slashes. E.g., =--ins=switch,/^in/,car=. If only one of these
|
|
options is given, atomic propositions not matched by that option
|
|
are assumed to belong to the other set.
|
|
|
|
Another way to specify the input/output partition is using a =*.part=
|
|
file passed to the =--part-file= option. Such a file is used by
|
|
several other synthesis tools. The format is space-separated list of
|
|
words representing atomic-propositions. Two keywords =.inputs= and
|
|
=.outputs= indicate the set of the atomic-propositions that follow.
|
|
For instance:
|
|
|
|
#+BEGIN_EXAMPLE
|
|
.inputs request cancel
|
|
.outputs grant ack
|
|
#+END_EXAMPLE
|
|
|
|
Using =--part-file=THEABOVEFILE= is equivalent to
|
|
=--ins=request,cancel --outs=grant,ack=.
|
|
|
|
As an extension to this simple =*.part= format, words enclosed in
|
|
slashes are interpreted as regexes, like for the =--ins= and =--outs=
|
|
options.
|
|
|
|
* TLSF input
|
|
|
|
=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 line shows how a TLSF specification called =FILE= can
|
|
be synthesized using =syfco= and =ltlsynt=:
|
|
|
|
#+BEGIN_SRC sh :export code
|
|
ltlsynt --tlsf FILE
|
|
#+END_SRC
|
|
|
|
The above =--tlsf= option will call =syfco= (which must be on your
|
|
=$PATH=) to perform the conversion and extract output signals, as if
|
|
you had used:
|
|
|
|
#+BEGIN_SRC sh :export code
|
|
LTL=$(syfco -f ltlxba -m fully FILE)
|
|
OUT=$(syfco --print-output-signals FILE)
|
|
ltlsynt --formula="$LTL" --outs="$OUT"
|
|
#+END_SRC
|
|
|
|
|
|
* Output options
|
|
|
|
By default, the controller is output in HOA format, but it can be
|
|
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.
|
|
|
|
#+NAME: exampleaig
|
|
#+BEGIN_SRC sh :exports both
|
|
ltlsynt -f 'F(i1 & Xi2) <-> F(o1)' --aiger
|
|
#+END_SRC
|
|
|
|
#+RESULTS: exampleaig
|
|
#+begin_example
|
|
REALIZABLE
|
|
aag 5 2 1 1 2
|
|
2
|
|
4
|
|
6 11
|
|
8
|
|
8 4 6
|
|
10 3 9
|
|
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 -f 'F(i1 & Xi2) <-> F(o1)' --hide-status --aiger --dot
|
|
#+END_SRC
|
|
|
|
#+RESULTS: exampleaigdot
|
|
|
|
#+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 they emit their value from
|
|
the =*_out= rectangles at the bottom. Their input value, to be
|
|
emitted at the next step, is received via the =*_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=.
|
|
|
|
* Internal details
|
|
|
|
The tool reduces the synthesis problem to a parity game, and solves the parity
|
|
game using Zielonka's recursive algorithm. The process can be pictured as follows.
|
|
|
|
[[file:ltlsynt.svg]]
|
|
|
|
LTL decomposition consist in splitting the specification into multiple
|
|
smaller constraints on disjoint subsets of the output values (as
|
|
described by [[https://arxiv.org/abs/2103.08459][Finkbeiner, Geier, and Passing]]), solve those constraints
|
|
separately, and then combine them while encoding the AIGER circuit.
|
|
This is enabled by default, but can be disabled by passing option
|
|
=--decompose=no=.
|
|
|
|
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 =ltlsynt= is in =--realizability= mode, the process stops here
|
|
|
|
In synthesis mode, the strategy is first simplified. How this is done
|
|
can be fine-tuned with option =--simplify=:
|
|
#+BEGIN_SRC sh :exports results
|
|
ltlsynt --help | sed -n '/--simplify=/,/^$/p' | sed '$d'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat
|
|
: simplification to apply to the controler (no)
|
|
: nothing, (bisim) bisimulation-based reduction,
|
|
: (bwoa) bissimulation-based reduction with output
|
|
: assignment, (sat) SAT-based minimization,
|
|
: (bisim-sat) SAT after bisim, (bwoa-sat) SAT after
|
|
: bwoa. Defaults to 'bwoa'.
|
|
|
|
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
|
|
|
|
** Printing games
|
|
|
|
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 flags deactivate the resolution of the
|
|
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 -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]]
|
|
|
|
** Saving statistics in CSV
|
|
:PROPERTIES:
|
|
:CUSTOM_ID: csv
|
|
:END:
|
|
|
|
For benchmarking purpose, the =--csv= option can be used to record
|
|
intermediate statistics about the resolution.
|
|
|
|
For instance the following command builds controllers (when they
|
|
exist) for the 23 demonstration specifications from [[http://www.ist.tugraz.at/staff/jobstmann/lily/][Lily 1.0.2]] while
|
|
saving some statistics in =bench.csv=. (If you compare our results
|
|
with theirs, keep in mind that Lily uses Moore's semantics, while
|
|
=ltlsynt= uses Mealy's semantics.) We use =-q= to hide the
|
|
constructed controllers, as we are only interested in the statistics.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports code :epilogue true
|
|
genltl --lily-patterns | ltlsynt --algo=acd --aiger -q --csv=bench.csv
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
|
|
After execution, =bench.csv= contains a table like the following:
|
|
|
|
#+BEGIN_SRC sh :results output raw :exports results
|
|
sed 's/"//g
|
|
s/|/\\vert{}/g
|
|
s/--/@@html:--@@/g
|
|
1a\
|
|
|-|
|
|
s/^/| /
|
|
s/$/ |/
|
|
s/,/|/g
|
|
' bench.csv
|
|
#+END_SRC
|
|
|
|
#+ATTR_HTML: :class csv-table
|
|
#+RESULTS:
|
|
| source | subspecs | algo | split | total_time | sum_trans_time | sum_split_time | sum_todpa_time | sum_solve_time | sum_strat2aut_time | aig_time | realizable | max_trans_states | max_trans_edges | max_trans_colors | max_trans_ap | max_game_states | max_game_colors | max_strat_states | max_strat_edges | sum_strat_states | sum_strat_edges | max_simpl_strat_states | max_simpl_strat_edges | sum_simpl_strat_states | sum_simpl_strat_edges | aig_latches | aig_gates |
|
|
|--------+----------+------+-------+-------------+----------------+----------------+----------------+----------------+--------------------+-------------+------------+------------------+-----------------+------------------+--------------+-----------------+-----------------+------------------+-----------------+------------------+-----------------+------------------------+-----------------------+------------------------+-----------------------+-------------+-----------|
|
|
| -:1 | 2 | acd | auto | 0.000408974 | 0.000183978 | 1.9226e-05 | 1.8736e-05 | 7.654e-06 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 3 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
|
|
| -:2 | 2 | acd | auto | 0.000297303 | 0.000176515 | 1.3345e-05 | 1.7834e-05 | 5.431e-06 | 8.075e-06 | 0 | 0 | 5 | 8 | 0 | 1 | 10 | 0 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 0 | 0 |
|
|
| -:3 | 1 | acd | auto | 0.000791278 | 0.000549861 | 4.4484e-05 | 1.7753e-05 | 1.6862e-05 | 8.436e-06 | 5.246e-05 | 1 | 12 | 46 | 1 | 3 | 26 | 1 | 5 | 5 | 5 | 5 | 2 | 2 | 2 | 2 | 1 | 0 |
|
|
| -:4 | 1 | acd | auto | 0.00078738 | 0.000526687 | 6.6005e-05 | 2.0329e-05 | 1.7083e-05 | 1.028e-05 | 3.678e-05 | 1 | 15 | 62 | 1 | 3 | 33 | 1 | 6 | 6 | 6 | 6 | 3 | 3 | 3 | 3 | 2 | 8 |
|
|
| -:5 | 1 | acd | auto | 0.000835672 | 0.000494376 | 6.9522e-05 | 2.3264e-05 | 1.8816e-05 | 2.2202e-05 | 8.9289e-05 | 1 | 20 | 88 | 1 | 3 | 47 | 1 | 8 | 9 | 8 | 9 | 6 | 7 | 6 | 7 | 3 | 46 |
|
|
| -:6 | 1 | acd | auto | 0.000872972 | 0.000479157 | 7.4541e-05 | 2.64e-05 | 2.1601e-05 | 2.5038e-05 | 8.8497e-05 | 1 | 24 | 111 | 1 | 3 | 55 | 1 | 11 | 12 | 11 | 12 | 7 | 9 | 7 | 9 | 3 | 46 |
|
|
| -:7 | 1 | acd | auto | 0.000787119 | 0.000382314 | 4.238e-05 | 1.4988e-05 | 1.3055e-05 | 8.546e-06 | 0.000155214 | 1 | 11 | 38 | 1 | 3 | 26 | 1 | 7 | 8 | 7 | 8 | 6 | 7 | 6 | 7 | 3 | 29 |
|
|
| -:8 | 1 | acd | auto | 3.2521e-05 | 1.794e-06 | 0 | 0 | 0 | 0 | 1.052e-05 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 |
|
|
| -:9 | 1 | acd | auto | 0.000505467 | 0.000354952 | 2.106e-05 | 2.7602e-05 | 1.3225e-05 | 6.282e-06 | 1.8395e-05 | 1 | 6 | 19 | 2 | 2 | 16 | 2 | 2 | 3 | 2 | 3 | 2 | 3 | 2 | 3 | 1 | 1 |
|
|
| -:10 | 1 | acd | auto | 3.2231e-05 | 1.092e-06 | 0 | 0 | 0 | 0 | 1.0921e-05 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 |
|
|
| -:11 | 1 | acd | auto | 4.1779e-05 | 1.5269e-05 | 3.847e-06 | 3.436e-06 | 3.737e-06 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 3 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
|
|
| -:12 | 1 | acd | auto | 3.4015e-05 | 1.352e-06 | 0 | 0 | 0 | 0 | 1.2925e-05 | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | 1 | 1 | 1 | 0 | 0 |
|
|
| -:13 | 1 | acd | auto | 0.000229304 | 0.000135867 | 9.848e-06 | 7.855e-06 | 4.819e-06 | 4.749e-06 | 1.2514e-05 | 1 | 2 | 3 | 1 | 2 | 5 | 1 | 2 | 2 | 2 | 2 | 1 | 2 | 1 | 2 | 0 | 0 |
|
|
| -:14 | 1 | acd | auto | 0.000310568 | 0.000199397 | 1.0069e-05 | 1.2905e-05 | 5.571e-06 | 3.888e-06 | 1.7733e-05 | 1 | 1 | 3 | 2 | 2 | 4 | 1 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 2 | 1 | 0 |
|
|
| -:15 | 1 | acd | auto | 0.00075019 | 0.000435724 | 6.0634e-05 | 2.9616e-05 | 1.6872e-05 | 1.075e-05 | 8.2957e-05 | 1 | 8 | 40 | 2 | 4 | 30 | 1 | 7 | 12 | 7 | 12 | 5 | 10 | 5 | 10 | 3 | 38 |
|
|
| -:16 | 1 | acd | auto | 0.00297522 | 0.00156048 | 0.000310197 | 8.474e-05 | 5.5796e-05 | 2.9766e-05 | 0.000558948 | 1 | 22 | 225 | 3 | 6 | 103 | 1 | 22 | 40 | 22 | 40 | 17 | 36 | 17 | 36 | 5 | 326 |
|
|
| -:17 | 1 | acd | auto | 0.000468838 | 0.000296471 | 1.3916e-05 | 1.5699e-05 | 6.362e-06 | 4.568e-06 | 2.9867e-05 | 1 | 1 | 4 | 3 | 3 | 6 | 1 | 3 | 3 | 3 | 3 | 3 | 3 | 3 | 3 | 2 | 3 |
|
|
| -:18 | 1 | acd | auto | 0.000630864 | 0.000437838 | 1.8946e-05 | 1.7714e-05 | 6.342e-06 | 5.139e-06 | 3.2902e-05 | 1 | 1 | 5 | 4 | 4 | 8 | 1 | 4 | 4 | 4 | 4 | 4 | 4 | 4 | 4 | 2 | 5 |
|
|
| -:19 | 1 | acd | auto | 0.000424403 | 0.00026955 | 2.2813e-05 | 2.641e-05 | 1.1281e-05 | 4.309e-06 | 1.5469e-05 | 1 | 4 | 15 | 2 | 3 | 11 | 2 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 1 | 0 | 0 |
|
|
| -:20 | 1 | acd | auto | 0.0109 | 0.00806685 | 0.0014951 | 0.000575409 | 0.000282314 | 1.8305e-05 | 0.000173057 | 1 | 311 | 3488 | 2 | 5 | 1002 | 2 | 10 | 10 | 10 | 10 | 6 | 8 | 6 | 8 | 3 | 30 |
|
|
| -:21 | 1 | acd | auto | 0.0674067 | 0.0618205 | 0.00108741 | 8.1494e-05 | 0.000130147 | 0.00011593 | 0.00220405 | 1 | 75 | 546 | 1 | 8 | 371 | 1 | 74 | 228 | 74 | 228 | 71 | 213 | 71 | 213 | 7 | 1299 |
|
|
| -:22 | 1 | acd | auto | 0.00230346 | 0.00124588 | 0.000171444 | 5.5064e-05 | 5.4483e-05 | 2.7612e-05 | 0.000318924 | 1 | 30 | 161 | 2 | 4 | 86 | 1 | 22 | 25 | 22 | 25 | 15 | 19 | 15 | 19 | 4 | 194 |
|
|
| -:23 | 1 | acd | auto | 0.000509164 | 0.000336807 | 1.6551e-05 | 1.5599e-05 | 1.046e-05 | 8.035e-06 | 3.3092e-05 | 1 | 7 | 16 | 1 | 2 | 17 | 1 | 5 | 6 | 5 | 6 | 3 | 4 | 3 | 4 | 2 | 10 |
|
|
|
|
The subset of columns output is adjusted according to the task
|
|
performed by =ltlsynt=. For instance with =--realizability=, the CSV
|
|
file will not include statistics about the winning strategies or the
|
|
AIG circuits. When reading a game with =--from-pgame=, columns giving
|
|
statistics about LTL translation will be omitted.
|
|
|
|
The names of the columns should be mostly self explanatory. The
|
|
decomposition of the specification into multiple sub-specifications
|
|
makes it slightly incoveniant to track statistics in a run. The
|
|
column =subspecs= indicates how many sub-specifications were found in
|
|
the original specification. Columns with names of the form =sum_*=
|
|
accumulate their statistics over all subspecifications. Columns with
|
|
names of the form =max_*= keep only the largest statistics. The following
|
|
statistics are gathered:
|
|
|
|
- =source=: location of the specification in the form FILENAME:LINE
|
|
(FILENAME is =-= when reading from standard input as in the above
|
|
example).
|
|
- =formula= (if requested with option =--csv-with-formula=): is the
|
|
actual LTL formula used for the specification, is usually makes the
|
|
CSV file very large
|
|
- =subspecs=: the number of sub-specifications resulting from the
|
|
decomposition
|
|
- =algo=: the name of the approach used to construct game, as
|
|
specified with the =--algo= option
|
|
- =split=: the name of the approach used to split the automaton into
|
|
input and output steps, as specified with the =--split= option
|
|
- =total_time=: total time measured by =ltlsynt= to solve the problem
|
|
once the problem has been loaded (parsing of the formula, conversion
|
|
from TSLF, or parsing of a parity game are all excluded)
|
|
- =sum_trans_time=: sum of the translation time used to obtain an
|
|
automaton from each subspecification.
|
|
- =sum_split_time=: sum of the times used to split the automata
|
|
- =sum_todpa_time=: sum of the times used to paritize the automata
|
|
- =sum_solve_time=: sum of the times used to solve the game for each
|
|
subspecification
|
|
- =sum_strat2aut_time=: sum of the time needed to extract the
|
|
strategies
|
|
- =aig_time=: time used to encode all strategies into one AIG circuit
|
|
- =realizable=: whether the specification is realizable
|
|
- =max_trans_states,max_trans_edges,max_trans_colors,max_trans_ap=:
|
|
Size of the largest automaton constructed for a subspecification.
|
|
The largest size is actually the largest quadruple of the form
|
|
(states,edges,colors,ap), so those maximum values are not
|
|
independent.
|
|
- =max_game_states=: maximum number of state in any game constructed
|
|
- =max_game_colors=: maximum numbers of colors in any game constructed
|
|
(might not be the same game as for =max_game_states=)
|
|
- =max_strat_states,max_strat_edges=: size of the largest strategy
|
|
found. The largest size is the largest pair (states,edges), so
|
|
those two values are not indeendent.
|
|
- =sum_strat_states,sum_strat_edges=: sum of the states/edges in
|
|
strategies for all subspecifications
|
|
- =max_simpl_strat_states,max_simpl_strat_edges=: size of the largest
|
|
simplified strategy.
|
|
- =sum_simpl_strat_states,sum_simpl_strat_edges=: sum of the
|
|
states/edges in simplified strategies for all subspecifications
|
|
- =aig_gates,aig_latches=: Size of the AIG circuit, if requested.
|
|
|
|
|
|
In this example table, some of the intermediate processing times are
|
|
listed as =0= (e.g., for input 8, 10, 12) because the specifications
|
|
can be found to be realizable trivially without building any game.
|
|
|
|
|
|
** Verifying the output
|
|
|
|
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]])
|
|
|
|
Simplification of Mealy machines is discussed in the following papers:
|
|
|
|
- *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]])
|
|
- *The Mealy-machine reduction functions of Spot*, /Florian Renkin/,
|
|
/Philipp Schlehuber-Caissier/, /Alexandre Duret-Lutz/, and /Adrien Pommellet/.
|
|
Science of Computer Programming, 230(102995), August 2023. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#renkin.23.fmsd][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/renkin.23.fmsd.pdf][pdf]])
|
|
|
|
A more recent paper covering many aspects of =ltlsynt= is the following
|
|
|
|
- *Dissecting ltlsynt*, /Florian Renkin/, /Philipp
|
|
Schlehuber-Caissier/, /Alexandre Duret-Lutz/, and Adrien Pommellet.
|
|
In Formal Methods in System Design, 2023. ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#renkin.23.scp][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/renkin.23.scp.pdf][pdf]])
|
|
|
|
# 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
|