diff --git a/README.md b/README.md index 5c0e34c..88143c6 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ Quantitative Timed Pattern Matching [![License: GPL v3](https://img.shields.io/badge/License-GPLv3-blue.svg)](./LICENSE) [![Doxygen](https://img.shields.io/badge/docs-Doxygen-deepgreen.svg)](https://maswag.github.io/qtpm/doxygen/index.html) -This is our experimental implementation of *Quantitative Timed Pattern Matching*. +This is an experimental implementation of *Quantitative Timed Pattern Matching*. See [FORMATS2019.md](./experiments/README.md) for the experiments in our FORMATS 2019 paper. Demo on Google Colab is [HERE](https://colab.research.google.com/drive/1y1LU0pKQb5rMcuwwA9VwEb5Ec8I2qvlf)!! @@ -24,7 +24,7 @@ Usage **-V**, **--version** Print the version
**-i** *file*, **--input** *file* Read a signal from *file*.
**-f** *file*, **--automaton** *file* Read a timed automaton from *file*.
-**-a**, **--abs** absolute time mode.
+**-a**, **--abs** absolute time mode. In this mode, the "time" entry shows the (absolute) timestamp of the end of each piece.
**--maxmin** Use max-min semiring robust semantics (default).
**--minplus** Use min-plus semiring robust semantics.
**--maxplus** Use max-plus semiring robust semantics.
@@ -54,10 +54,33 @@ Input Format ### Signal -A signal is a sequence of the following line. +A signal is a sequence of the following lines. time v(x1) v(x2) v(x3) ... v(xn) +Here, the column "time" has different meaning between relative time mode (default) and absolute time mode (enabled by `-a`). +Consider an example of a signal where during the first 1.0 time unit, the value is 0.0, and during the next 1.0 time unit, the value is 2.0. +In the relative time mode, such a signal is encoded as follows, where the "time" entry shows the duration of each piece. + +``` +1.0 0.0 +1.0 2.0 +``` + +In the absolute time mode, such a signal is encoded as follows, where the "time" entry shows the (absolute) timestamp of the end of each piece. + +``` +1.0 0.0 +2.0 2.0 +``` + +Note on the accepting states +---------------------------- + +To simplify the algorithm, we assume that each matching ends at the same time as a transition to an accepting state is invoked. This assumption does not harm the generality: one can construct a TSWA for such a matching algorithm by making all the states during matching non-accepting, making a fresh accepting state, and making transitions to it so that the transitions to the accepting state are invoked when the matching ends. The following is a typical example of such a TSWA: + +![TSWA taken from the paper](./doc/paper.svg) + How to make compile_commands.json --------------------------------- diff --git a/doc/paper.svg b/doc/paper.svg new file mode 100644 index 0000000..b4c8d37 --- /dev/null +++ b/doc/paper.svg @@ -0,0 +1,56 @@ + + + + + + +G + + + +0 + +{x0 < 15} + + + +1 + +{x0 > 5} + + + +0->1 + + +x0 < 5 / x0 := 0 + + + +2 + + + + + + +1->2 + + +x0 < 10 + + + +dummy0 + + + +dummy0->0 + + + + +