Skip to content

Latest commit

 

History

History
144 lines (99 loc) · 5.59 KB

README.md

File metadata and controls

144 lines (99 loc) · 5.59 KB
Raw

Experiments Data for FORMATS 2019

This is a document on the experiment data for the FORMATS 2019 paper [Waga19].

Experimental setting

We compiled using GCC 4.9.3. See also README.md. 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 DOT files representing the TSAs are in this directory.

Description of the Benchmarks

All the benchmarks are inspired by the properties in [KJD+16] for automotive specifications. The input signals are generated from tprasadtp/cruise-control-simulink.

Overshoot

The TSA is for the settling when the reference value of the velocity is changed from vref < 35 to vref > 35. The duration of the matching signals is less than 150 time units. 0d

Ringing

The TSA is for the frequent rise and fall of the signal in 80 time units. The constraints rise and fall are rise = v(t) − v(t − 10) > 10 and fall = v(t) − v(t − 10) < −10.

Overshoot (Unbounded)

The TSA is almost the same as that in Overshoot, but the time-bound (c < 150) is removed.

Files

Input TSAs

The following files are the TSAs (i.e., the specifications) used in the experiments.

  • overshoot.dot: TSA for Overshoot benchmark
  • ringing.dot: TSA for Ringing benchmark
  • overshoot_unbounded.dot: TSA for Overshoot (Unbounded) benchmark

Input Logs

The input logs can be downloaded from HERE. The content of the downloaded file is as follows. This log is generated by a cruise control model. The input data set consists of two parts: different length and different density.

.
├── 10.0
│   ├── BrCCPulse-120000.tsv
│   ├── BrCCPulse-180000.tsv
│   ├── BrCCPulse-240000.tsv
│   ├── BrCCPulse-300000.tsv
│   ├── BrCCPulse-360000.tsv
│   ├── BrCCPulse-420000.tsv
│   ├── BrCCPulse-480000.tsv
│   ├── BrCCPulse-540000.tsv
│   ├── BrCCPulse-60000.tsv
│   └── BrCCPulse-600000.tsv
└── density
    ├── BrCCPulseDensity-10000.tsv
    ├── BrCCPulseDensity-12000.tsv
    ├── BrCCPulseDensity-15000.tsv
    ├── BrCCPulseDensity-20000.tsv
    ├── BrCCPulseDensity-30000.tsv
    ├── BrCCPulseDensity-6.666667e+03.tsv
    ├── BrCCPulseDensity-6000.tsv
    ├── BrCCPulseDensity-60000.tsv
    ├── BrCCPulseDensity-7500.tsv
    └── BrCCPulseDensity-8.571429e+03.tsv

Data format

The input logs are TSV (tab-separated values) files as follows.

time	v(t)	v_ref(t)	|v(t) - v_ref(t)|

For example, the following log shows that:

  1. From 0--10 time units, the velocity was 40.69039115 and the reference value as 50. Therefore their difference is 9.309608849.
  2. From 10--20 time units, the velocity was 51.26813036 and the reference value as 50. Therefore their difference is 1.26813036.
  3. From 20--30 time units, the velocity was 54.04550954 and the reference value as 50. Therefore their difference is 4.045509539.
  4. ...
0	20	20	0
10	40.69039115	50	9.309608849
20	51.26813036	50	1.26813036
30	54.04550954	50	4.045509539
40	54.05581387	50	4.055813869

For ringing, we append differences to make another entry.

time	v(t)	v_ref(t)	|v(t) - v_ref(t)|	v(t) - v(t - interval)

Different Length (files under 10.0)

For the files under 10.0, the sampling frequency is fixed (0.1Hz) and the number of the entries is changed (6001--60001). The number on each file stands for the duration of the log not the number of entries. For example, BrCCPulse-60000.tsv contains 6001 entries because we sample one entry every 10.0 time units.

Different Density (files under density)

For the files under density, the number of the entries in each log is fixed (6001), and the sampling frequency is changed (1.0Hz--10.0Hz). The number on each file stands for the duration of the log not the sampling frequency nor the number of entries. For example, the sampling frequency of BrCCPulse-60000.tsv is 10.0Hz because the duration is 60000 time units and it contains 6001 samples, which means 10.0Hz.

Calling qtpm

For all case studies, the following command was used:

./build/qtpm -i [signal.tsv] -f [pattern.dot] --abs

In the paper, we used the result of the following command to measure the execution time and the memory usage.

/usr/bin/time -v -o [log] ../build/qtpm -i [signal.tsv] -f [pattern.dot] --abs > /dev/null 2>&1

Scripts

run_gtime.sh/run_gtime_density.sh

  • The script to run an experiment
  • This script works both in Linux and Mac

make_tsv.sh

  • The script to make tsv of the summary of the experiment results.
  • The input data is not specified in the script. Therefore, it can be used for both of the data sets.
  • This script works both in Linux and Mac

References

[Waga19]
Masaki Waga, Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata. In Proc. FORMATS 2019, LNCS 11750, pp. 3-22.
[KJD+16]
James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, Alexandre Donze, To- moya Yamaguchi, Hisahiro Ito, Tomoyuki Kaga, Shunsuke Kobuna, and Sanjit Seshia. St-lib: a library for specifying and classifying model behav- iors. Technical report, SAE Technical Paper, 2016.