Skip to content

A Tool for Parametric Timed Patten Matching with Automata-Based Acceleration

License

Notifications You must be signed in to change notification settings

MasWag/ParamMONAA

Repository files navigation

Param MONAA --- A Tool for Parametric Timed Patten Matching with Automata-Based Acceleration

Boost.Test License: GPL v3

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!!

Usage

Synopsis

pmonaa [OPTIONS] -f FILE

Options

-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.

Example

./build/pmonaa -s parametric -f ./examples/pta.dot < ./examples/timed_word.txt

Installation

Param MONAA is tested on Arch Linux and Mac OSX 10.14.1

Requirements

  • C++ compiler supporting C++14 and the corresponding libraries.
  • Boost (>= 1.59)
  • Eigen
  • CMake
  • Bison
  • Flex
  • PPL

Instructions

mkdir build 
mkdir build/tre build/constraint
cd build && cmake -DCMAKE_BUILD_TYPE=Release .. && make && make install

Syntax of Parametric Timed Automata

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 init0 or 1init=1 if the state is initial
vertexmatch0 or 1match=1 if the state is accepting
edgelabel[a-z], [A-Z]the value represents the event on the transition
edgereseta list of integersthe set of variables reset after the transition
edgeguarda list of inequality constraintsthe guard of the transition

References

  • 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]

About

A Tool for Parametric Timed Patten Matching with Automata-Based Acceleration

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published