The version of IMITATOR used to run the experiments is IMITATOR v2.10.4.
We present in the following table a list of case studies to which parametric timed pattern matching was applied.
| Model | PTPM | PTPMopt | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| |X| | |P| | Raw word | Model | Length | Time frame | Parsing | States | Matches | Time | Result | States | Time | Result |
| 3 | 5 | blowup-200.imi | 200 | 101 | 0.01 | 20602 | 5050 | 15.31 | blowup-200.res | 515 | 0.24 | blowup-200-minp1.res | |
| blowup-400.imi | 400 | 202 | 0.02 | 81202 | 20100 | 82.19 | blowup-400.res | 1015 | 0.49 | blowup-400-minp1.res | |||
| blowup-600.imi | 600 | 301 | 0.03 | 322402 | 45150 | 158.5 | blowup-600.res | 1508 | 0.59 | blowup-600-minp1.res | |||
| blowup-800.imi | 800 | 405 | 0.04 | 242202 | 80200 | 342.9 | blowup-800.res | 2008 | 0.83 | blowup-800-minp1.res | |||
| blowup-1000.imi | 1000 | 503 | 0.1 | 377752 | 125250 | 625.4 | blowup-1000.res | 2508 | 1.08 | blowup-1000-minp1.res | |||
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 S-TaLiRo 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 S-TaLiRo to generate a input sequence of gear change.
As a third experiment, we considered an original (toy) benchmark that acts as a worst case situation for parametric timed pattern matching [AHW18].
Our random timed words were generated automatically using a Python script gen_timed_word.py.
The IMITATOR timed words were generated automatically from the .tsv files using a Python script convert_benchmark.py.
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
For all case studies, the following command was used for PTPMopt:
> ./imitator [case_study.imi] -mode [EFmin|EFmax] -no-inclusion-test-in-EF -incl -verbose experiments -output-result -output-prefix [case_study-minP1|maxp1|minp10.imi]