alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* doc/org/ltlmix.org: Typos.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2024-09-19 08:50:41 +02:00
parent 7b0e15a7fb
commit 40a45eff22
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
doc/org/ltlmix.org
View file

@ -198,7 +198,7 @@ or 1
Note that in the LTL case, =false= and =true= can be generated by Note that in the LTL case, =false= and =true= can be generated by
default: when building leave, =alse= and =true= have the same default: when building leave, =alse= and =true= have the same
probability to be selected as any input formula. probability to be selected as any input formula.
example). He
* Randomizing atomic propositions with =-A= or =-P= * Randomizing atomic propositions with =-A= or =-P=
@ -207,7 +207,7 @@ used in the input formulas. This works as follows: if option =-A N=
was given, every time an input formula φ is selected, its atomic was given, every time an input formula φ is selected, its atomic
propositions are replaced by atomic propositions randomly selected in propositions are replaced by atomic propositions randomly selected in
a set of size $N$. If φ uses $i$ atomic propositions and $i\ge N$, 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 then those $i$ atomic propositions 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 the new atomic propositions may replace several of the original atomic
propositions. propositions.
@ -231,7 +231,7 @@ These options solve two problems:
Here is that same example with a single formula, =GFa=, whose atomic Here is that same example with a single formula, =GFa=, whose atomic
proposition will be randomly replaced by one of propositions will be randomly replaced by one of
$\{p_0,p_1,p_2,p_3,p_4\}$. $\{p_0,p_1,p_2,p_3,p_4\}$.
#+BEGIN_SRC sh :exports both #+BEGIN_SRC sh :exports both
@ -397,7 +397,7 @@ because we have to deal with two sets of atomic proposition: one set
for input, and one set for output. for input, and one set for output.
[[https://www.ijcai.org/proceedings/2017/0189.pdf][Zhu et al. (IJCAI'17)]] generate their benchmark for LTL synthesis using [[https://www.ijcai.org/proceedings/2017/0189.pdf][Zhu et al. (IJCAI'17)]] generate their benchmark for LTL synthesis using
a setup similar to the above, except that when atomic proposition are a setup similar to the above, except that when atomic propositions are
randomized, we must make sure not to change their input or output randomized, we must make sure not to change their input or output
nature. nature.
@ -435,7 +435,7 @@ When randomizing the atomic propositions in these formulas before
combining them, we want to replace each input (resp. output) combining them, we want to replace each input (resp. output)
proposition by a random input (resp. output) proposition. This is proposition by a random input (resp. output) proposition. This is
achieved by passing two numbers to =-A= or =-P=. In the case of [[https://www.ijcai.org/proceedings/2017/0189.pdf][Zhu achieved by passing two numbers to =-A= or =-P=. In the case of [[https://www.ijcai.org/proceedings/2017/0189.pdf][Zhu
et al.]], they do not change the polarity of the proposition during et al.]], they do not change the polarity of the propositions during
their generation, so we would use =-A= to mimic their setup. their generation, so we would use =-A= to mimic their setup.
Here are 6 random conjunctions of the above four patterns, in which Here are 6 random conjunctions of the above four patterns, in which
@ -489,6 +489,6 @@ chose from may help to get more realizable formulas.
When the original LTL synthesis specification formulas have atomic When the original LTL synthesis specification formulas have atomic
proposition that do not start with =i= or =o=, options =--ins=, propositions that do not start with =i= or =o=, options =--ins=,
=--outs=, or =--part-file= can be used to specify the nature of the =--outs=, or =--part-file= can be used to specify the nature of these
atomic propositions. These options work as [[file:ltlsynt.org::#input-options][=ltlsynt='s input options]]. atomic propositions. These options work as [[file:ltlsynt.org::#input-options][=ltlsynt='s input options]].