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

Source code
Standalone binary for Linux (Ubuntu-like, Debian-like 64 bits)

Compositional Verifier

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

IMITATOR + CV

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.

The syntax recognized is exactly that of parametric event-recording automata, without the extensions usually supported by IMITATOR (no stopwatches, no discrete variables, no invariants, no urgent locations…) However, shared clocks, shared parameters, synchronization… are all supported.
For each event "a", a clock named "clock_a" must be explicitly reset (this clock MUST be named "clock_a", i.e., the name of the event preceded with "clock_")
As the Python script works with string replacing, there are some restrictions on variable names:
- no parameter name should overlap another parameter name, nor any string in the entire model: that is, if p1 is defined, then p11 should not be defined; the name "a" or "p" for a parameter should also be avoided, as all "a" or "p" will be replaced by something in the full model (including in predefined strings such as "automaton" or "end")
- all initial locations should have different names and, again, should not overlap other names. Other locations are subject to no restriction.
Some "tags" (in the form of comments) are required for the interface to recognize the components:
- Component A should start with tag "(* --- BEGIN COMPONENT A --- *)" and end with tag "(* --- END COMPONENT A --- *)"
- Component B should start with tag "(* --- BEGIN COMPONENT B --- *)" and end with tag "(* --- END COMPONENT B --- *)"
- The specification should start with tag "(* --- BEGIN SPECIFICATION --- *)" and end with tag "(* --- END SPECIFICATION --- *)"
- For all accepting locations, a tag "(*-*- ACCEPTING -*-*)" must be added after the name of the location. For example, "loc my_location(*-*- ACCEPTING -*-*): while True wait {}" All locations are accepting in all automata, except in the specification, where the only accepting location is the location to be reached (e.g., the error location for a safety property).

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 10321, pages 17–32, June 2017. (English) [PDF (author version) | BibTeX | Slides]🌐
[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é