This is the source code repository for Param MONAA --- A Tool for Parametric Timed Patten Matching with Automata-Based Acceleration.
The demo on Google Colab is HERE!!
pmonaa [OPTIONS] -f FILE
-h, --help Print a help message.
-q, --quiet Quiet mode. Causes any results to be suppressed.
-s mode, --skip mode Specify which skipping is used. It should be one of parametric
(default), non-parametric
, and none
.
-a, --ascii Ascii mode. (default)
-b, --binary Binary mode.
-V, --version Print the version
-i file, --input file Read a timed word from file.
-r, --rational Use rational number of GMP (default).
-F, --float Use floating point number.
-f file, --automaton file Read a timed automaton from file.
./build/pmonaa -s parametric -f ./examples/pta.dot < ./examples/timed_word.txt
Param MONAA is tested on Arch Linux and Mac OSX 10.14.1
- C++ compiler supporting C++14 and the corresponding libraries.
- Boost (>= 1.59)
- Eigen
- CMake
- Bison
- Flex
- PPL
mkdir build
mkdir build/tre build/constraint
cd build && cmake -DCMAKE_BUILD_TYPE=Release .. && make && make install
You can use DOT language to represent a parametric timed automaton. For the timing constraints and other information, you can use the following custom attributes.
attribute | value | description | |
---|---|---|---|
vertex | init | 0 or 1 | init=1 if the state is initial |
vertex | match | 0 or 1 | match=1 if the state is accepting |
edge | label | [a-z], [A-Z] | the value represents the event on the transition |
edge | reset | a list of integers | the set of variables reset after the transition |
edge | guard | a list of inequality constraints | the guard of the transition |
- Offline Timed Pattern Matching under Uncertainty. Étienne André, Ichiro Hasuo, and Masaki Waga. ICECCS 2018: 10-20 [arXiv version]
- Online Parametric Timed Pattern Matching with Automata-Based Skipping. Masaki Waga and Étienne André, NFM 2019: 371-389 [arXiv version]