We implemented the online algorithms for parametric timed pattern matching in C++ and we compiled them using GCC 7.3.0.
We used PPL as polyhedra library [BHZ08].
The version of IMITATOR used to run the experiments is IMITATOR v2.10.4.
We conducted the experiments on an Amazon EC2 c4.large instance (2.9 GHz Intel Xeon E5-2666 v3, 2 vCPUs, and 3.75 GiB RAM) that runs Ubuntu 18.04 LTS (64 bit).
The raw result consists of many outputs of GNU time. We parsed and generated summarized TSV files using the scripts in here.
Benchmark Gear inspired by the scenario of monitoring the gear change of an automatic transmission system. We conducted simulation of the model of an automatic transmission system [HAF14]. We used Breach to generate an input to this model; it generates a gear change signal that is fed to the model. A gear is chosen from {g_1,g_2,g_3,g_4}. The generated gear change is recorded in a timed word.
The of benchmark Accel is also constructed from the Simulink model of the automated transmission system [HAF14]. For this benchmark, the (discretized) value of three state variables are recorded in W: engine RPM (discretized to "high" and "low" with a certain threshold), velocity (discretized to "high" and "low" with a certain threshold), and 4 gear positions. We used Breach to generate a input sequence of gear change.
As a third experiment, we considered a (toy) benchmark that acts as a worst case situation for parametric timed pattern matching, coming from [AHW18].
For all case studies, the following command was used for PTPM:
> ./imitator [case_study.imi] -mode EFunsafe -no-inclusion-test-in-EF -incl -verbose experiments -output-result