added TREs

MasWag · Sep 9, 2019 · 348fc2e · 348fc2e
1 parent d3322c6
commit 348fc2e
Show file tree

Hide file tree

Showing 5 changed files with 89 additions and 51 deletions.
diff --git a/doc/TA.md b/doc/TA.md
@@ -1,7 +1,7 @@
 Timed Automata
 ==============
 
-In this document, we show how to use MONAA to monitor a timed automata specification. We assume that you know the basics of timed automata and what MONAA does. If you have never used MONAA, we recommend to read [Getting Started](./getting_started.md).
+In this document, we show how to use MONAA to monitor a timed automata specification. We assume that you know the basics of timed automata (e.g., [AD94]) and what MONAA does. If you have never used MONAA, we recommend to read [Getting Started](./getting_started.md).
 
 We use the following timed word as the input. It is also in
 [`example/getting_started/timed_word.txt`](../example/getting_started/timed_word.txt).
@@ -137,3 +137,8 @@ The result of the timed pattern matching is as follows.
   1.000000        < t' - t <=   1.400000
 =============================
 ```
+
+References
+-------------
+
+- [AD94] A theory of timed automata. Rajeev Alur and David L. Dill, Theoretical Computer Science, Volume 126, Issue 2, 1994, Pages 183-235
diff --git a/doc/TRE.md b/doc/TRE.md
@@ -0,0 +1,72 @@
+Timed Regular Expressions
+=========================
+
+In this document, we show how to use MONAA to monitor a specification written in timed regular expressions. We assume that you know the basics of timed regular expressions (e.g., [ACM02]) and what MONAA does. If you have never used MONAA, we recommend to read [Getting Started](./getting_started.md), which contains some examples of the TREs.
+
+Timed Regular Expressions
+-------------------------
+
+In MONAA, the given timed regular expression is translated into a timed automaton and the timed pattern matching problem is conducted for the translated timed automaton. The timed regular expression supported in MONAA is defined as follows. Here, we use the blank character (' ') to represent the each elements, but MONAA interprets ' ' as an event and you have to omit these blank character when you actually use MONAA. You can also read the code of the [parser](../monaa/tre_parser.yy) and the [lexer](../monaa/tre_lexer.l).
+
+```
+expr : c (An event)
+     | ( expr ) (Grouping)
+     | expr + (Kleene Plus)
+     | expr * (Kleene Star)
+     | expr expr (Concatenation)
+     | expr | expr (Disjunction)
+     | expr & expr (Conjunction)
+     | expr % (s,t) (Time Restriction)
+```
+
+For the basic examples, please read [Getting Started](./getting_started.md). We only show advanced specifications here.
+
+Conjunction
+-----------
+
+You can use conjunction to represent some complicated timing constraints.
+Here, we use the following timed word in `example/getting_started/timed_word2.txt`.
+```
+A 0.5
+B 0.8
+C 1.5
+A 2.0
+B 2.9
+C 4.2
+```
+
+![The example timed word 2](./fig/getting_started/timed_word2.svg)
+
+The following expression matches a consecutive occurrences of the events A, B, and C such that the duration between the A and B is less than 1 and the duration between the B and C is more than 1.
+
+```
+../build/monaa -e '(((AB)%(0,1)C)&(A(BC)%(1,20)))$' < ../examples/getting_started/timed_word2.txt
+```
+
+```
+  1.500000       <= t <   2.000000
+  4.200000        < t' <=        inf
+  2.200000        < t' - t <=        inf
+=============================
+```
+
+Terminate character
+-------------------
+
+The following expression matches a consecutive occurrences of the events A, B, and C such that the blank interval after C is longer than 1.
+
+```
+../build/monaa -e 'ABC($)%(1,20)' < ../examples/getting_started/timed_word2.txt
+```
+
+```
+  1.500000       <= t <   2.000000
+  5.200000        < t' <  24.200000
+  3.200000        < t' - t <  22.700000
+=============================
+```
+
+References
+-------------
+
+- [ACM02] Timed regular expressions. Eugene Asarin, Paul Caspi, and Oded Maler, Journal of the ACM, Volume 49 Issue 2, March 2002, Pages 172-206
diff --git a/doc/getting_started.md b/doc/getting_started.md
@@ -1,11 +1,10 @@
 Getting Started
 ===============
 
-Let's see an example usage of MONAA. We use timed regular expressions in
-this document.
+Let's see an example usage of MONAA. We use timed regular expressions (TREs) [ACM02] in this document.
+See also [this document](./TRE.md) for the detail of the TREs supported by MONAA.
 
-Consider the following as the input timed word. It is also in
-`example/getting_started/timed_word.txt`.
+Consider the following as the input timed word. It is also in `example/getting_started/timed_word.txt`.
 
 ``` {.example}
 A 0.5
@@ -22,7 +21,7 @@ C 4.6
 Your first example
 ------------------
 
-Let\'s detect consecutive occurrences of the events A and B. For
+Let's detect consecutive occurrences of the events A and B. For
 example, we can use the TRE `(AB)$`. An example of the usage and the
 result is as follows.
 
@@ -53,7 +52,7 @@ A 2.0
 B 3.2
 ```
 
-In timed pattern matching, the \`\`occurrences\'\' does not mean the
+In timed pattern matching, the "occurrences" does not mean the
 subwords but it means the trimming on an open interval. For example, the
 first occurrence of AB is observed by the trimming on (0.3,1.0).
 Therefore, the result of MONAA is not a set of subwords but a (possibly
@@ -151,48 +150,7 @@ We note that this does not change the result because in the log, we do not have
 =============================
 ```
 
-Advanced specifications
------------------------
+References
+-------------
 
-### Conjunction
-
-You can use conjunction to represent some complicated timing constraints.
-Here, we use the following timed word in `example/getting_started/timed_word2.txt`.
-```
-A 0.5
-B 0.8
-C 1.5
-A 2.0
-B 2.9
-C 4.2
-```
-
-![The example timed word 2](./fig/getting_started/timed_word2.svg)
-
-The following expression matches a consecutive occurrences of the events A, B, and C such that the duration between the A and B is less than 1 and the duration between the B and C is more than 1.
-
-```
-../build/monaa -e '(((AB)%(0,1)C)&(A(BC)%(1,20)))$' < ../examples/getting_started/timed_word2.txt
-```
-
-```
-  1.500000       <= t <   2.000000
-  4.200000        < t' <=        inf
-  2.200000        < t' - t <=        inf
-=============================
-```
-
-### Terminate character
-
-The following expression matches a consecutive occurrences of the events A, B, and C such that the blank interval after C is longer than 1.
-
-```
-../build/monaa -e 'ABC($)%(1,20)' < ../examples/getting_started/timed_word2.txt
-```
-
-```
-  1.500000       <= t <   2.000000
-  5.200000        < t' <  24.200000
-  3.200000        < t' - t <  22.700000
-=============================
-```
+- [ACM02] Timed regular expressions. Eugene Asarin, Paul Caspi, and Oded Maler, Journal of the ACM, Volume 49 Issue 2, March 2002, Pages 172-206
diff --git a/doc/index.md b/doc/index.md
@@ -25,6 +25,8 @@ Further information
 -------------------
 
 <dl>
+<dt><a href="./TRE/">Timed regular expressions</a></dt>
+<dd>Detail of the timed regular expressions supported by MONAA.</dd>
 <dt><a href="./TA/">Timed automata</a></dt>
 <dd>Use timed automata to describe advanced timing constraints.</dd>
 <dt><a href="./related_tools/">Related Tool</a></dt>

diff --git a/mkdocs.yml b/mkdocs.yml
@@ -9,5 +9,6 @@ nav:
 #  - Home: index.md
   - Getting started: getting_started.md
   - Installation guide: install.md
+  - Timed regular expressions: TRE.md
   - Timed automata: TA.md
   - Related Tool: related_tools.md