* doc/org/ltlmix.org: Fix several typos.
This commit is contained in:
Alexandre Duret-Lutz
parent
3e90265ce7
commit
b549e8e8c1
1 changed files with 54 additions and 51 deletions
|
|
@ -1,5 +1,5 @@
|
|||
# -*- coding: utf-8 -*-
|
||||
#+TITLE: =ltlgrind=
|
||||
#+TITLE: =ltlmix=
|
||||
#+DESCRIPTION: Spot command-line tool for combining LTL formulas randomly
|
||||
#+INCLUDE: setup.org
|
||||
#+HTML_LINK_UP: tools.html
|
||||
|
|
@ -14,7 +14,7 @@ some handwritten, meaningful formulas, and combine those formulas to
|
|||
build larger sets that are possibly more challenging.
|
||||
|
||||
Here is a very simple example that builds five formulas that are
|
||||
Boolean combination of formulas from taken in the set
|
||||
Boolean combination of formulas taken from the set
|
||||
$\{\mathsf{GF}a,\mathsf{FG}b,\mathsf{X}c\}$:
|
||||
|
||||
#+BEGIN_SRC sh :exports both
|
||||
|
|
@ -34,15 +34,15 @@ ltlmix -f GFa -f FGb -f Xc -n 5
|
|||
|
||||
For each formula that it generates, =ltlmix= constructs a random
|
||||
syntax-tree of a certain size (5 by default) in which internal nodes
|
||||
represent operators selected randomly from a list of operator, and
|
||||
leaves are subformulas selected randomly from the set of input
|
||||
formulas. As an example, the syntax tree of =!φ₁ xor !φ₂= has size 5,
|
||||
and its leaves =φ₁= and =φ₂= will be taken randomly from the set of
|
||||
input formulas.
|
||||
represent operators selected randomly from a list of operators.
|
||||
Leaves of that tree are subformulas selected randomly from the set of
|
||||
input formulas. As an example, the syntax tree of =!φ₁ xor !φ₂= has
|
||||
size 5, and its leaves =φ₁= and =φ₂= will be taken randomly from the
|
||||
set of input formulas.
|
||||
|
||||
The algorithm is actually the same as for =randltl=, except
|
||||
that =randltl= use random atomic propositions as leaves when =ltlmix=
|
||||
uses random formulas.
|
||||
The algorithm is actually the same as for =randltl=, except that
|
||||
=randltl= uses random atomic propositions as leaves when =ltlmix= uses
|
||||
random formulas.
|
||||
|
||||
The same input formula can be picked several times to be used on
|
||||
multiple leaves of the tree. Note that because Spot implements some
|
||||
|
|
@ -104,10 +104,10 @@ and 1
|
|||
or 1
|
||||
#+end_example
|
||||
|
||||
In the above list, =false= and =true= represent the Boolean constants
|
||||
(which are usually undesirable when building random Boolean formulas),
|
||||
and =sub= represent a random formula drawn from the list of input
|
||||
formulas.
|
||||
In the above list, =false= and =true= represent the Boolean constants:
|
||||
those are usually undesirable when building random Boolean formulas,
|
||||
especially with Spot's trivial rewritings. =sub= represents a random
|
||||
formula drawn from the list of input formulas.
|
||||
|
||||
The above command shows that each operator has a weight, called
|
||||
/priority/. When the priority is 0, the operator is never used. When
|
||||
|
|
@ -146,7 +146,7 @@ Ge <-> (!Fc <-> !Xa)
|
|||
** Boolean or LTL syntax tree
|
||||
|
||||
By default, the syntax tree generated on top of the randomly selected
|
||||
input formula uses only Boolean operators.
|
||||
input formulas uses only Boolean operators.
|
||||
|
||||
Using option =-L= will use LTL operators instead.
|
||||
|
||||
|
|
@ -195,21 +195,24 @@ and 1
|
|||
or 1
|
||||
#+end_example
|
||||
|
||||
Note that in the LTL case, =false= and =true= can be generated by default.
|
||||
Note that in the LTL case, =false= and =true= can be generated by
|
||||
default: when building leave, =alse= and =true= have the same
|
||||
probability to be selected as any input formula.
|
||||
example). He
|
||||
|
||||
* Randomizing atomic propositions with =-A= or =-P=
|
||||
|
||||
Options =-A= or =-P= can be used to change the atomic propositions
|
||||
used in the input formulas. This works as follows: if =-A N= was
|
||||
given, every time an input formula φ is selected, its atomic
|
||||
used in the input formulas. This works as follows: if option =-A N=
|
||||
was given, every time an input formula φ is selected, its atomic
|
||||
propositions are replaced by atomic propositions randomly selected in
|
||||
a set of size $N$. If φ uses $i$ atomic propositions and $i\ge N$,
|
||||
then those $i$ atomic proposition will be remapped to $i$ distinct
|
||||
atomic propositions chosen randomly in that set. if $i>N$, some of
|
||||
atomic propositions chosen randomly in that set. If $i>N$, some of
|
||||
the new atomic propositions may replace several of the original atomic
|
||||
propositions.
|
||||
|
||||
Option =-P N= is similar to =-A N= except that the selected atomic
|
||||
Option =-P N= is similar to =-A N=, except that the selected atomic
|
||||
propositions can possibly be negated.
|
||||
|
||||
|
||||
|
|
@ -218,17 +221,18 @@ These options solve two problems:
|
|||
- They lessen the issue that a formula selected several times can lead
|
||||
to syntax tree such as =φ | φ | φ= that reduces to =φ=. Now, each
|
||||
occurrence of =φ= as a chance to use different atomic propositions.
|
||||
(The larger =N= is, the more likely it is that these copies of φ
|
||||
will be different).
|
||||
The larger =N= is, the more likely it is that these copies of φ
|
||||
will be different.
|
||||
|
||||
- They allow combining formulas that had completely different sets of
|
||||
atomic propositions, in such a way that they are now interdependent
|
||||
(the smaller N is the more likely it is that subformulas will share
|
||||
atomic propositions).
|
||||
atomic propositions, in such a way that they are now interdependent.
|
||||
The smaller N is the more likely it is that subformulas will share
|
||||
atomic propositions.
|
||||
|
||||
|
||||
Here is an example with a single formula, =GFa=, whose atomic proposition
|
||||
will be randomly replaced by one of $\{p_0,p_1,p_2,p_3,p_4\}$.
|
||||
Here is that same example with a single formula, =GFa=, whose atomic
|
||||
proposition will be randomly replaced by one of
|
||||
$\{p_0,p_1,p_2,p_3,p_4\}$.
|
||||
|
||||
#+BEGIN_SRC sh :exports both
|
||||
ltlmix -fGFa -A5 --tree-size=8 -n10
|
||||
|
|
@ -274,8 +278,8 @@ GF!p1 xor (!GF!p2 | (GF!p1 <-> GFp0))
|
|||
** Mixing the DAC patterns
|
||||
|
||||
The command [[file:genltl.org][=genltl --dac-pattern=]] will print a list of 55 LTL
|
||||
formulas representing various specification patterns listed by Dwyer
|
||||
et al. (FMSP'98). Using =--stat=%x= to count the atomic propositions
|
||||
formulas representing various specification patterns listed by [[https://doi.org/10.1145/302405.30267][Dwyer
|
||||
et al. (FMSP'98)]]. Using =--stat=%x= to count the atomic propositions
|
||||
in each formula, and some standard unix tools, we can compute that
|
||||
they use at most 6 atomic propositions.
|
||||
|
||||
|
|
@ -324,9 +328,9 @@ so is uses atomic propositions $\{p_0,p_1,...\}$ starting at 0 and without gap.
|
|||
|
||||
** Random conjunctions
|
||||
|
||||
Some benchmarks (e.g., [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][for LTL satisfiability]]) are built by
|
||||
conjunction of $L$ random formulas picked from a set of basic
|
||||
formulas. Each picked formula has its atomic proposition mapped to
|
||||
Some benchmarks (e.g., [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][for LTL satisfiability]]) are built as
|
||||
conjunctions of $L$ random formulas picked from a set of basic
|
||||
formulas. Each picked formula has its atomic propositions mapped to
|
||||
random literals built from a subset of $m$ atomic variables.
|
||||
|
||||
Given a value for $m$, option =-P m= will achieve the second part of
|
||||
|
|
@ -335,7 +339,7 @@ need to ask for a tree of size $2L-1$ in which only the =and= operator
|
|||
is allowed.
|
||||
|
||||
Here is an example with $L=10$ (hence =--tree-size=19=) and $m=50$.
|
||||
The example use a small set of three basic formulas
|
||||
The example uses a small set of three basic formulas
|
||||
$\{\mathsf{G}a,\mathsf{F}a,\mathsf{X}a\}$ for illustration, but in
|
||||
practice you should replace these =-f= options by =-F FILENAME=
|
||||
pointing to a file containing all the input formulas to select from.
|
||||
|
|
@ -359,9 +363,9 @@ Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12
|
|||
Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31
|
||||
#+end_example
|
||||
|
||||
In fact building random conjunctions is common enough to have its own
|
||||
flag. Using =-C N= will see the tree size to $2N-1$ and disable all
|
||||
operators but =and=. The above command can therefore be reduced to
|
||||
Random conjunctions is common enough to have its own flag. Using =-C
|
||||
N= will see the tree size to $2N-1$ and disable all operators but
|
||||
=and=. The above command can therefore be reduced to
|
||||
|
||||
#+BEGIN_SRC sh :exports both
|
||||
ltlmix -fGa -fFa -fXa -n10 -P50 -C10
|
||||
|
|
@ -381,7 +385,6 @@ Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12
|
|||
Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31
|
||||
#+end_example
|
||||
|
||||
|
||||
Selecting 10 random conjuncts out of 3×50×2=300 possibilities has a
|
||||
13.7% chance that at least 2 conjuncts will be identical (see [[https://en.wikipedia.org/wiki/Birthday_problem][Birthday
|
||||
paradox]]), so because of Spot's trivial rewritings, some of the above
|
||||
|
|
@ -398,10 +401,10 @@ a setup similar to the above, except that when atomic proposition are
|
|||
randomized, we must make sure not to change their input or output
|
||||
nature.
|
||||
|
||||
They use small examples from the [[http://www.ist.tugraz.at/staff/jobstmann/lily/][Lily]] distribution has basic formulas
|
||||
to combine. Spot can print those using =genltl --lily=. There are 23
|
||||
of them, we will limit ourselves to four of them for illustrative
|
||||
purpose.
|
||||
They use small examples from the [[http://www.ist.tugraz.at/staff/jobstmann/lily/][Lily]] distribution as basic formulas
|
||||
to combine. Spot can print those formulas using =genltl --lily=.
|
||||
There are 23 of them, but we will limit ourselves to four of them for
|
||||
illustrative purpose.
|
||||
|
||||
#+BEGIN_SRC sh :exports both
|
||||
genltl --lily=8..11
|
||||
|
|
@ -413,12 +416,13 @@ purpose.
|
|||
: (GFi1 | Fi0) -> (GFo1 | Go0)
|
||||
: !(G(i1 -> Fo0) & G(i0 -> Fo1))
|
||||
|
||||
Notice that atomic proposition either start with =i= (for input) or
|
||||
=o= for output. This allows Spot to infer their nature. For instance,
|
||||
we could feed those directly to [[file:ltlsynt.org][=ltlsynt=]]:
|
||||
Notice how these atomic propositions either start with =i= (for input)
|
||||
or =o= for output. This allows Spot to infer their nature. For
|
||||
instance, we could feed those directly to [[file:ltlsynt.org][=ltlsynt=]] to decide if they
|
||||
are realizable:
|
||||
|
||||
#+BEGIN_SRC sh :exports both :prologue true
|
||||
genltl --lily=8..11 | ltlsynt -q
|
||||
#+BEGIN_SRC sh :exports both :epilogue true
|
||||
genltl --lily=8..11 | ltlsynt --realizability
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
|
@ -427,7 +431,6 @@ we could feed those directly to [[file:ltlsynt.org][=ltlsynt=]]:
|
|||
: REALIZABLE
|
||||
: UNREALIZABLE
|
||||
|
||||
|
||||
When randomizing the atomic propositions in these formulas before
|
||||
combining them, we want to replace each input (resp. output)
|
||||
proposition by a random input (resp. output) proposition. This is
|
||||
|
|
@ -453,8 +456,8 @@ set of 5 (resp. 4).
|
|||
: !(G(i3 -> Fo1) & G(i1 -> Fo3)) & !(G(i3 -> Fo0) & G(i0 -> Fo2)) & ((GFi0 | Fi3) -> (GFo0 | Go1))
|
||||
: ((Fi1 | GFi4) -> (Go0 | GFo2)) & !(G(i0 -> Fo2) & G(i4 -> Fo1)) & !(G(i3 -> Fo2) & G(i1 -> Fo1))
|
||||
|
||||
#+BEGIN_SRC sh :exports both :prologue true
|
||||
genltl --lily=8..11 | ltlmix -A5,4 -C3 -n6 | ltlsynt -q
|
||||
#+BEGIN_SRC sh :exports both :epilogue true
|
||||
genltl --lily=8..11 | ltlmix -A5,4 -C3 -n6 | ltlsynt --realizability
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
|
@ -468,11 +471,11 @@ set of 5 (resp. 4).
|
|||
Note that because one of the original pattern is unrealizable, any
|
||||
conjunction involving it will be unrealizable. Even if we had only
|
||||
realizable specifications to combine, the smaller the atomic
|
||||
propositions set are, the more likely the random conjuncts will be in
|
||||
proposition sets are, the more likely the random conjuncts will be in
|
||||
conflict. Therefore, increasing the number of atomic propositions to
|
||||
chose from may help to get more realizable formulas.
|
||||
|
||||
#+BEGIN_SRC sh :exports both :prologue true
|
||||
#+BEGIN_SRC sh :exports both :epilogue true
|
||||
genltl --lily=8..11 | ltlmix -A50,50 -C3 -n6 | ltlsynt -q
|
||||
#+END_SRC
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue