Skip to content

MasWag/SyMon

Repository files navigation

SyMon --- SYmbolic MONitor

Boost.Test License: GPL v3

This is the source code repository for SyMon --- A tool for symbolic monitoring

Demo on Google Colab is HERE!!

Usage

Synopsis

symon [OPTIONS] -pf [AUTOMATON_FILE] -s [SIGNATURE_FILE] (-i [TIMEDWORD_FILE])

Options

-h, --help Print a help message.
-i file, --input file Read a timed word from file.
-f file, --automaton file Read a timed automaton from file.
-s file, -signature pattern Read a signature from file.
-b, -boolean non-parametric and Boolean mode (default).
-d, -dataparametric data-parametric mode.
-p, -parametric fully parametric mode.

Example

./build/symon -f ./example/copy/copy.dot -s ./example/copy/copy.sig < ./example/copy/copy.txt
./build/symon -df ./example/copy/copy_data_parametric.dot -s ./example/copy/copy.sig < ./example/copy/copy.txt
./build/symon -pf ./example/copy/copy_parametric.dot -s ./example/copy/copy.sig < ./example/copy/copy.txt
./build/symon -pf ./example/copy/copy_tpm.dot -s ./example/copy/copy.sig < ./example/copy/copy.txt

The examples used in our CAV 2019 paper is here.

Installation

SyMon is tested on macOS 10.14.4

Requirements

  • C++ compiler supporting C++17 and the corresponding libraries.
  • Boost (>= 1.67.0)
  • CMake
  • Parma Polyhedra Library

Instructions

mkdir build 
cd build && cmake -DCMAKE_BUILD_TYPE=Release .. && make

Limitation in Boolean mode

  • The updates of a variable is only xN := xY
    • We do not allow assignment of literal or expression.
  • The constraint of number expression is only <expression> <op> <constaint>
    • This is not the essential problem. Just for simplicity of the implementation.
  • In a constraint s0 <op> s1 of strings, we assume that we know the value of either s0 or s1 (i.e., one of them must be constant).
  • In a constraint n0 or n0 <op> n1 of numbers, we assume that we know the value of both n0 and n1 (i.e., both of them must be constant).
    • It is possible to have an unknown variable only if it is not used in the constraint.

Specifications

  • The unobservable action is available only in the fully parametric mode (with -p).
  • The unobservable action is assigned to id 127. This will be modified in a future version.

The file format of the signature

The format of the signature file is as follows.

<key0>	<StringSize>	<NumberSize>
<key1>	<StringSize>	<NumberSize>
...

For example, the following signature shows that:

  • the predicate 0 is open, which takes one string argument; and
  • the predicate 1 is put, which takes one string argument and one number argument.
open	1	0
put	1	1

How to make compile_commands.json

mkdir build
cd build && cmake -DCMAKE_EXPORT_COMPILE_COMMANDS=ON ..

References

About

A tool for SYmbolic MONitoring

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages