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

* doc/org/concepts.org: Fix a few typos.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2016-01-23 22:11:18 +01:00
parent c4e9083f4e
commit 727d4cc678
1 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

26
doc/org/concepts.org
View file

@ -881,8 +881,8 @@ finite languages as a prefix of a PSL formula.
| PSL formula | meaning | | PSL formula | meaning |
|--------------+-------------------------------------------------------------------------| |--------------+-------------------------------------------------------------------------|
| ={e}<>->f | =f= should hold on the last instant of some one prefix that matches =e= | | ={e}<>->f= | =f= should hold on the last instant of some one prefix that matches =e= |
| ={e}[]->f | =f= should hold on the last instant of all prefixes that match =e= | | ={e}[]->f= | =f= should hold on the last instant of all prefixes that match =e= |
In the above table =e= is a semi-extended expression, and =f= is a PSL (or LTL) formula. In the above table =e= is a semi-extended expression, and =f= is a PSL (or LTL) formula.
@ -890,16 +890,16 @@ Semi-extended regular expressions can be formed using Boolean
expressions over [[#ap][atomic propositions]] and the following expressions over [[#ap][atomic propositions]] and the following
operators: operators:
| SERE | meaning | | SERE | meaning |
|--------------------+-----------------------------------------------------------------------------------| |----------------------+-----------------------------------------------------------------------------------|
| =e1;e2= | =e1= followed by =e2= (concatenation) | | =e1;e2= | =e1= followed by =e2= (concatenation) |
| =e1:e2= | =e1= fused with =e2=: =e2= has to start matching on the last letter matching =e1= | | =e1:e2= | =e1= fused with =e2=: =e2= has to start matching on the last letter matching =e1= |
| =e1 \vert\vert e2= | =e1= or =e2= have to match (union) | | =e1= \vert\vert =e2= | =e1= or =e2= have to match (union) |
| =e1 && e2= | =e1= and =e2= have to match (intersection) | | =e1 && e2= | =e1= and =e2= have to match (intersection) |
| =e1 & e2= | =e2= should match a prefix of what =e1= matches, or vice-versa | | =e1 & e2= | =e2= should match a prefix of what =e1= matches, or vice-versa |
| =e[*]= | =e= should be matched a finite number of times (Kleene star) | | =e[*]= | =e= should be matched a finite number of times (Kleene star) |
| =e[*2..3]= | same as =(e;e)\vert\vert(e;e;e)= | | =e[*2..3]= | same as =(e;e)= \vert\vert =(e;e;e)= |
| =e[+]= | =e= should be matched a finite number of times, and at least once | | =e[+]= | =e= should be matched a finite number of times, and at least once |
For example the formula ={(1;1)[*]}[]->a= can be interpreted as follows: For example the formula ={(1;1)[*]}[]->a= can be interpreted as follows:
@ -929,7 +929,7 @@ automaton can then be simplified using several algorithms depending on what opti
Here is for instance a translation of ={(1;1)[*]}[]->a= discussed [[#psl][above]]. Here is for instance a translation of ={(1;1)[*]}[]->a= discussed [[#psl][above]].
#+NAME: ltl2tgba1 #+NAME: ltl2tgba1
#+BEGIN_SRC sh :results verbatim :exports both #+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba '{(1;1)[*]}[]->a' -d ltl2tgba '{(1;1)[*]}[]->a' -d
#+END_SRC #+END_SRC
#+BEGIN_SRC dot :file concept-ltl2tgba.png :cmdline -Tpng :var txt=ltl2tgba1 :exports results #+BEGIN_SRC dot :file concept-ltl2tgba.png :cmdline -Tpng :var txt=ltl2tgba1 :exports results