IMITATOR

IMITATOR: Experiments Data for FORTE 2017

Case Studies Related to Learning-based compositional parameter synthesis for event-recording automata

This page is dedicated to the case studies related to the manuscript Learning-based compositional parameter synthesis for event-recording automata by Étienne André and Shang-Wei Lin, published in the proceedings of FORTE’17 [ALin17].

Software

The software environment is made of IMITATOR (developed by Étienne André), CV (the compositional verifier developed by Shang-Wei Lin), and a python script interfacing both tools.

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR 2.9-alpha1 (branch master, build 2212, GitHub hash 75e2110).

Download

Compositional Verifier

The following link allows to download both CV and IMITATOR 2.9-alpha1 together with the interfacing Python script:

These binaries are standalone binaries for Linux systems 64 bits, and require no dependency, except Python of course. To generate graphics, the dot utility (from the graphviz) package is necessary.

The source code for both IMITATOR and the interfacing script are available on GitHub.

efsmt_coverts

We tried to compare our approach to the tool mentioned in [ABBCR16]. It can be downloaded there.

Note that, at the time of writing (February 2017), the efsmt_coverts installation instructions were not completely accurate, and we had to contact Lăcrămioara Aştefănoaei, who very kindly helped us to install the tool. Please feel free to do the same if necessary.

Case studies: comparisons between algorithms

We present in the following table a list of case studies computed using various algorithms using IMITATOR.

The model for each specification can be obtained by clicking on the specification name (for each specification, only the "Spec" PTA differs); the rectangular parameter domain can be obtained by clicking on the D0; logs including results can be obtained by clicking on the response time of each algorithm; the actual result by IMITATOR (in the IMITATOR normalized form) can be obtained by clicking on the "result", whenever the algorithm terminated; a graphical 2D representation of the synthesized constraint can be obtained by clicking on the [g] (when available).

Benchmark EFSynth PRPC CompSynth [ABBCR16]
Name Ref |A| |X| |P| Spec D0 t (s) Result # iter t (s) Result # abs. # counter-ex learning t (s) total (s) Result models interactions log
FMS-1 [LALSD14] 6 18 2 1 D0 0.299 result [g] 2 0.654 result [g] 1 1 0.074 0.136 result [g] models FMS1.im FMS1.log
2 0.010 result [g] 1 0.372 result [g] 0 1 0.038 0.046 result [g]
3 0.282 result [g] 1 0.309 result [g] 1 0 0.090 0.242 result [g]
FMS-2 [LALSD14] 11 37 2 1 D0 T.O. T.O. 1 1 84.2 88.9 result [g] models FMS2.im FMS2.log
2 T.O. T.O. 1 0 81.4 85.2 result [g]
3 0.051 result [g] T.O. 0 2 1.10 2.44 result [g]
4 0.062 result [g] T.O. 0 1 1.42 1.53 result [g]
5 T.O. T.O. 1 0 31.4 40.8 result [g]
6 D0 T.O. T.O. 1 0 37.2 42.4 result [g]
AIP [LALSD14] 11 46 2 1 D0 0.551 result [g] T.O. 0 1 0.086 0.114 result [g] (to upload) (to upload) (to upload)
2 2.11 result [g] T.O. 0 1 1.22 1.25 result [g]
3 3.91 result [g] T.O. 0 1 8.50 8.54 result [g]
4 0.235 result [g] T.O. 1 1 8.39 8.42 result [g]
5 T.O. T.O. 1 0 0.394 0.871 result [g]
6 T.O. T.O. 1 0 5.32 9.58 result [g]
7 T.O. T.O. 1 0 1.76 3.19 result [g]
8 T.O. T.O. 1 0 1.13 4.35 result [g]
9 T.O. T.O. 1 1 0.762 1.84 result [g]
10 0.022 result [g] T.O. 0 1 0.072 0.094 result [g]
Fischer-3 5 12 2 Fischer-3 D0 2.76 result [g] 4 14.0 result [g] T.O. models Fischer3.im Fischer3.log
Fischer-4 6 16 2 Fischer-4 D0 T.O. T.O. T.O. models Fischer4.im Fischer4.log

Case studies: scalability

We present in the following table an evaluation of the scalability of CompSynth w.r.t. of the reference parameter domain using IMITATOR.

Benchmark CompSynth
Name Ref |A| |X| |P| Spec D0 # abs. # counter-ex find next point (s) learning t (s) total (s)
FMS-2 [LALSD14] 11 37 2 1 2,500 1 1 0.0 81.0 85.7
10,000 1 1 0.1 82.5 87.3
250,000 1 1 2.2 82.0 89.0
1,000,000 1 1 8.9 83.1 96.7
25,000,000 1 1 221.2 83.1 309.0
1,000,000,000 1 1 888.1 83.5 976.4

Case studies: partitioning

We present in the following table an evaluation of the partitioning heuristics of the models when running CompSynth.

Benchmark Partitioning CompSynth
Name Ref |A| |X| |P| Spec D0 A B # abs. # counter-ex learning t (s) total (s) Result
FMS-1 [LALSD14] 6 18 2 1 D0 C M R1 R2 A 1 1 1.071 1.137 result
C M R1 R2 A 1 1 0.077 0.148 result
C M R2 R1 A 1 1 5.152 5.406 result
C M A R1 R2 1 1 5.663 5.980 result
C M R1 R2 A 1 1 0.123 0.290 result
C M R1 A R2 1 1 0.119 0.360 result
C M R2 A R1 1 1 6.150 6.690 result
2 C M R1 R2 A 0 1 0.133 0.149 result
C M R1 R2 A 0 2 0.077 0.123 result
C M R2 R1 A 0 1 0.040 0.056 result
C M A R1 R2 0 1 0.824 0.842 result
C M R1 R2 A 0 1 0.034 0.044 result
C M R1 A R2 0 2 0.096 0.144 result
C M R2 A R1 0 2 0.042 0.051 result
3 D0 C M R1 R2 A 1 0 0.211 0.270 result
C M R1 R2 A 1 0 0.082 0.186 result
C M R2 R1 A 1 0 1.094 1.208 result
C M A R1 R2 1 0 0.729 0.881 result
C M R1 R2 A 1 0 0.119 0.279 result
C M R1 A R2 1 0 0.314 0.634 result
C M R2 A R1 1 0 0.104 0.257 result

Description of the Case Studies

FMS-1 and FMS-2

This model is a parametric version of the flexible manufacturing system described in [LALSD14]. This flexible manufacturing system [QCM05] produces blocks with a cylindrical painted pin from raw blocks and raw pegs. It consists of 14 devices: three conveyors, two mills, a lathe, a painting device, six robots, and an assembly machine. The devices are connected through nine buffers, and the capacity of each buffer is one.

We modeled the FMS system in a constructive way such that FMS-1 is the simplest one and FMS-2 is a more detailed version. Properties require that each buffer should not overflow or underflow and that output of each buffer should be within three time units after its input.

AIP

AIP is a parametric version of a manufacturing system producing two products from two different materials [LALSD14]; this version was itself derived from [LLD06].

The AIP manufacturing system produces two products from two different materials. It consists of ten components: an I/O station, three transport units, two assembly stations, three external loops, and a central loop. Properties require that the routes of the two materials should be opposite and output of each loop should be within three time units after its input.

Fischer

This is a PERA model of Fischer’s mutual exclusion protocol, with 3 and 4 processes, respectively.

The (unique) specification requests than no more than one process is present in the critical section at one time.

Algorithms used

For all case studies, the following commands were used:

> bin/imitator29alpha1 case_study.imi case_study.v0 -mode EF -merge -incl -output-result -time-limit 600
> bin/imitator29alpha1 case_study.imi case_study.v0 -mode PRPC -merge -incl -output-result -time-limit 600
> bin/imitator29alpha1 case_study.imi case_study.v0 -mode coverlearning -merge -incl -output-result -time-limit 600

To generate the synthesized constraint in a graphical form, please add:

-output-cart

Syntax restriction

When using IMIATOR + CV, the full syntax of IMITATOR is not supported. In addition, some "tags" must be used in IMITATOR models to be recognized by CV.

References

[ABBCR16]
Lăcrămioara Aştefănoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess: Compositional Parameter Synthesis. FM 2016: 60-68
[AFKS12]
Étienne André, Laurent Fribourg, Ulrich Kühne and Romain Soulat. IMITATOR 2.5: A Tool for Analyzing Robustness in Scheduling Problems. In Dimitra Giannakopoulou and Dominique Méry (eds.), FM’12, LNCS 7436, Springer, pages 33–36, August 2012. (English) [PDF | PDF (author version) | BibTeX]
[ALin17]
Étienne André and Lin Shang-Wei (林尚威). Learning-based compositional parameter synthesis for event-recording automata. In Ahmed Bouajjani and Alexandra Silva (eds.), FORTE’17, Springer LNCS, June 2017. To appear.
[LALSD14]
Lin Shang-Wei (林尚威), Étienne André, Liu Yang (刘杨), Sun Jun and Dong Jin Song. Learning Assumptions for Compositional Verification of Timed Systems. Transactions on Software Engineering 40(2), pages 137–153, February 2014. [PDF | PDF (author version) | BibTeX]
[LLD06]
Ryan J. Leduc, Mark Lawford, Pengcheng Dai: Hierarchical interface-based supervisory control of a flexible manufacturing system. IEEE Trans. Contr. Sys. Techn. 14(4): 654-668 (2006)
[QCM05]
Max H. Queiroz, José E. R. Cury, W. Murray Wonham: Multitasking Supervisory Control of Discrete-Event Systems. Discrete Event Dynamic Systems 15(4): 375-395 (2005)

Contact

Étienne André