Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Spot
Spot
Commits
727d4cc6
Commit
727d4cc6
authored
Jan 23, 2016
by
Alexandre DuretLutz
Browse files
* doc/org/concepts.org: Fix a few typos.
parent
c4e9083f
Changes
1
Hide whitespace changes
Inline
Sidebyside
doc/org/concepts.org
View file @
727d4cc6
...
@@ 881,8 +881,8 @@ finite languages as a prefix of a PSL formula.
...
@@ 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 semiextended expression, and =f= is a PSL (or LTL) formula.
In the above table =e= is a semiextended expression, and =f= is a PSL (or LTL) formula.
...
@@ 890,16 +890,16 @@ Semiextended regular expressions can be formed using Boolean
...
@@ 890,16 +890,16 @@ Semiextended 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 viceversa 
 =e1 & e2=
 =e2= should match a prefix of what =e1= matches, or viceversa 
 =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
...
@@ 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 conceptltl2tgba.png :cmdline Tpng :var txt=ltl2tgba1 :exports results
#+BEGIN_SRC dot :file conceptltl2tgba.png :cmdline Tpng :var txt=ltl2tgba1 :exports results
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment