Skip to content

Commit

Permalink
updated README
Browse files Browse the repository at this point in the history
  • Loading branch information
MasWag committed Aug 7, 2023
1 parent 2448b03 commit 520e4b2
Show file tree
Hide file tree
Showing 2 changed files with 82 additions and 3 deletions.
29 changes: 26 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)!!
Expand All @@ -24,7 +24,7 @@ Usage
**-V**, **--version** Print the version <br />
**-i** *file*, **--input** *file* Read a signal from *file*. <br />
**-f** *file*, **--automaton** *file* Read a timed automaton from *file*. <br />
**-a**, **--abs** absolute time mode. <br />
**-a**, **--abs** absolute time mode. In this mode, the "time" entry shows the (absolute) timestamp of the end of each piece.<br />
**--maxmin** Use max-min semiring robust semantics (default). <br />
**--minplus** Use min-plus semiring robust semantics. <br />
**--maxplus** Use max-plus semiring robust semantics. <br />
Expand Down Expand Up @@ -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
---------------------------------

Expand Down
56 changes: 56 additions & 0 deletions doc/paper.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.

0 comments on commit 520e4b2

Please sign in to comment.