Uploaded materials

• virtual machine: SyMonCAV19AE.ova SyMonCAV19AE.ova(mirror)
  • sha1sum: 283ecdae424b7e64328e9c60073a3880e284e4b4
• short description: short_description.txt

The Virtual Machine

• OS: Ubuntu 16.04.3 LTS (64 bit)
• Login User: cav
• Password: ae

Our Host Platform

• OS: macOS Mojave
• RAM: 8GB
• number of cores: 2
• CPU frequency: 2.6 GHz

How to Proceed After Booting the Image

1. You can login automatically.
2. The full artifact description README.html is in the desktop. You can open the file by double-clicking.

A Workflow of the Evaluation

1. Open the terminal and change the current directory to /home/cav/evaluation_files by cd ~/evaluation_files
2. Execute SyMon giving the PTDA for Copy and a timed data word by ./run_copy.sh ./data/copy/copy-2000.tsv. One can use an arbitrary file in ./data/copy, for example ./run_copy.sh ./data/copy/copy-10000.tsv.
   • In addition to the convex polyhedra, this script also outputs some runtime data given by GNU time.
   • You can see the output convex polyhedra in /home/cav/evaluation_files/log/copy e.g., /home/cav/evaluation_files/log/copy/copy-2000.tsv.log.
3. Execute SyMon giving the PTDA for Dominant and a timed data word by ./run_dominant.sh ./data/dominant/dominant-2000.tsv. One can use an arbitrary file in ./data/dominant, for example ./run_dominant.sh ./data/dominant/dominant-10000.tsv.
   • In addition to the convex polyhedra, this script also outputs some runtime data given by GNU time.
   • You can see the output convex polyhedra in /home/cav/evaluation_files/log/dominant e.g., /home/cav/evaluation_files/log/dominant/dominant-2000.tsv.log.
4. Execute SyMon giving the PTDA for Periodic and a timed data word by ./run_periodic.sh ./data/periodic/periodic-10000.tsv. One can use an arbitrary file in ./data/periodic, for example ./run_periodic.sh ./data/periodic/periodic-20000.tsv.
   • In addition to the convex polyhedra, this script also outputs some runtime data given by GNU time.
   • You can see the output convex polyhedra in /home/cav/evaluation_files/log/periodic e.g., /home/cav/evaluation_files/log/periodic/periodic-10000.tsv.log.

Description of the Files and Directories

• /home/cav/evaluation_files/Makefile: Makefile to conduct experiments and create the resulting files
• /home/cav/evaluation_files/run_copy.sh: A script to execute SyMon giving the PTDA at /home/cav/evaluation_files/copy.dot and the signature at /home/cav/evaluation_files/copy.sig.
• /home/cav/evaluation_files/run_dominant.sh: A script to execute SyMon giving the PTDA at /home/cav/evaluation_files/dominant.dot and the signature at /home/cav/evaluation_files/dominant.sig.
• /home/cav/evaluation_files/run_periodic.sh: A script to execute SyMon giving the PTDA at /home/cav/evaluation_files/periodic.dot and the signature at /home/cav/evaluation_files/periodic.sig.
• /home/cav/evaluation_files/data/: The directory in which the input timed data words exist.
• /home/cav/evaluation_files/log/: The directory in which the produced logs by SyMon exist.

Source Code of SyMon

• Location: /home/cav/evaluation_files/symon/

The most relevant and interesting part of the source code tree

• /home/cav/evaluation_files/symon/src/parametric_monitor.hh, line 116–265 (ParametricMonitor::notify)

This is the function ParametricMonitor::notify. Given the structure consists of the 1) current event; 2) the data on the event; and 3) the timestamp, it incrementally conducts the symbolic monitor. More precisely, it follows the transitions of the PTDA, it updates the current configuration, and it outputs the observed result if it reaches an accepting location.

Unit test

We use unit test to assure the quality of the code of SyMon. The codes for the unit test are under /home/cav/evaluation_files/symon/test/. You can execute the unit test by cd /home/cav/evaluation_files/symon/build && make unit_test && ./unit_test.

Logs Created by SyMon

• Location: /home/cav/evaluation_files/log/