Skip to content

GitLab

Commit 7a4b8040 authored by Jaime Arias's avatar Jaime Arias
Browse files

artifact submission

parents
Expand all Hide whitespace changes
Inline Side-by-side
LICENSE 0 → 100644
View file @ 7a4b8040
This diff is collapsed.
README.md 0 → 100644
View file @ 7a4b8040
# Artifact: Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata
## 1. Folder Structure
```
.
├── artifact
│   ├── assets
│   │   ├── imitator # Binary of the tool
│   │   ├── IMITATOR-user-manual.pdf # Manual of the tool
│   │   └── testcases # Folder with the models and properties of the experiments
│   ├── imitator # Folder with the code source of the tool
│   ├── packages # Folder with the packages needed to compile the tool
│   └── scripts
│   ├── brp_experiments.sh # Script to run the experiments of the BRP case study
│   ├── generate_iterative.sh # Script to run the experiments of the table 2
│   └── generate_strategies.sh # Script to run the experiments of the table 1
├── LICENSE # GPL-3 license
└── README.md # File with the instructions of this artifact
```
## 2. The tool
The executable of the tool is provided:
```
artifact/assets/imitator
```
The execution of the tool without options/automata file provides a summary of
the usage of the tool. The full detailed manual is in:
```
artifact/assets/IMITATOR-user-manual.pdf
```
__Although it is not necessary__, users can compile the tool themselves in
the provided environment using:
```
sudo dpkg -i artifact/packages/*.deb # installs the dependencies
cd artifact/imitator
./build.sh # compiles the tool
cp bin/imitator ../assets # updates the imitator binary used in the experiments
```
## 3. Running the experiments
Three scripts are provided in the folder `scripts`. They were used for the
experiments in the paper. The first two scripts can be run on all, or on a
subset of the models (_i.e._ critical-region, critical-region4, F3, F4,
FDDI4, FischerAHV93, flipflop, fmtv1A1-v2, lynch lynch5, Pipeline-KP12-2-3,
RCP, Sched2.100.0, Sched2.50.0, spsmall, tgcTogether2) in order to obtain the
results in a shorter time.
- `generate_strategies.sh` generates __Table 1__ contents in `csv` format
which can be viewed in a spreadsheet tool (__the delimiter used is `;` which is
standard__). The script requires an output file specified with the `-o` option,
_e.g._:
```
cd artifact/scripts
./generate_strategies.sh -o table1.csv
```
The script also provides means to specify a timeout with the `-t` option
(other than the 120 seconds by default), use the _predefined_ subset of the
models (option `-S`), use the green colour (option `-g`) or give a list of
models separated by space (option `-i`). The help option explains them in
detail:
```
cd artifact/scripts
./generate_strategies.sh -h
```
The execution time of the script with and without the option `-S` is
approximately:
```
Benchmark #1: ./generate_strategies.sh -o table1.csv
Time (mean ± σ): 7653.829 s ± 11.522 s [User: 7603.133 s, System: 20.121 s]
Range (min … max): 7645.682 s … 7661.976 s 2 runs
Benchmark #2: ./generate_strategies.sh -o table1-short.csv -S
Time (mean ± σ): 1628.522 s ± 14.405 s [User: 1623.864 s, System: 4.148 s]
Range (min … max): 1618.336 s … 1638.708 s 2 runs
Summary
'./generate_strategies.sh -o table1-short.csv -S' ran
4.70 ± 0.04 times faster than './generate_strategies.sh -o table1.csv'
```
- `generate_iterative.sh` generates __Table 2__ in a similar way, _e.g._:
```
cd artifact/scripts
./generate_iterative.sh -o table2.csv
```
The script also provides means to specify a timeout with the `-t` option
(other than the 120 seconds by default), use the _predefined_ subset of the
models (option `-S`), use the exploration with layers (option `-l`) or give
a list of models separated by space (option `-i`). The help option explains
them in detail:
```
cd artifact/scripts
./generate_iterative.sh -h
```
The execution time of the script with and without the option `-S` is
approximately:
```
Benchmark #1: ./generate_iterative.sh -o table2.csv
Time (mean ± σ): 9132.625 s ± 86.479 s [User: 9055.203 s, System: 20.805 s]
Range (min … max): 9071.475 s … 9193.775 s 2 runs
Benchmark #2: ./generate_iterative.sh -o table2-short.csv -S
Time (mean ± σ): 1580.291 s ± 0.233 s [User: 1576.721 s, System: 3.913 s]
Range (min … max): 1580.126 s … 1580.455 s 2 runs
Summary
'./generate_iterative.sh -o table2-short.csv -S' ran
5.78 ± 0.05 times faster than './generate_iterative.sh -o table2.csv'
```
- `brp_experiments.sh` executes all experiments on the _Bounded Retransmission
Protocol_ in the same order as they appear in the paper. This script has
only the option `-a` which includes the execution of the experiment of section
6.1 with the `MAX=20`. The output is not processed by the script, hence the
user sees the partial results obtained on-the-fly by `imitator`.
```
cd artifact/scripts
./brp_experiments.sh
```
To enhance readability:
* Each series of experiments in a section has a title with a green background
* The commands executed are displayed with a yellow background before execution
* The final results of `imitator` are easily located as the constraint is
displayed with a black background
The help option explains in detail the options of the script:
```
cd artifact/scripts
./brp_experiments.sh -h
```
The execution time of the script with and without the option `-a` is
approximately:
```
Benchmark #1: ./brp_experiments.sh
Time (mean ± σ): 35.311 s ± 0.574 s [User: 34.989 s, System: 0.304 s]
Range (min … max): 34.904 s … 35.717 s 2 runs
Benchmark #2: ./brp_experiments.sh -a
Time (mean ± σ): 234.426 s ± 3.212 s [User: 233.971 s, System: 0.440 s]
Range (min … max): 232.155 s … 236.698 s 2 runs
Summary
'./brp_experiments.sh' ran
6.64 ± 0.14 times faster than './brp_experiments.sh -a'
```
## 4. External availability of the artifact
This artifact can be found in the following repositories
- __Zenodo DOI:__ https://doi.org/10.5281/zenodo.4115919
- __Gitlab:__ https://depot.lipn.univ-paris13.fr/imitator/papers/tacas21
Moreover, it can be executed using the following technologies:
- __Web Application:__ https://imitator.lipn.univ-paris13.fr/artifact
- __Docker Image:__ https://hub.docker.com/r/imitator/tacas21
artifact/assets/testcases/BRP/accepting.imiprop 0 → 100644
View file @ 7a4b8040
property := #synth CycleThrough(accepting)
artifact/assets/testcases/BRP/accepting_one.imiprop 0 → 100644
View file @ 7a4b8040
property := #witness CycleThrough(accepting)
artifact/assets/testcases/BRP/brp_Channels.imi 0 → 100755
View file @ 7a4b8040
(************************************************************
* IMITATOR MODEL
*
* BRP (Bounded Retransmission Protocol)
*
* Description : Bounded Retransmission Protocol [version slightly modified]
* Source : "The Bounded Retransmission Protocol Must Be on Time!"
* Author : Pedro R. D'Argenio , Joost-Pieter Katoen , Theo C. Ruys , G. Jan Tretmans
* Modeling : Laurent Fribourg
* Modified by : Laure Petrucci and Jaco van de Pol
*
* Created : ? (< 09/2007)
* Last modified : 2020/09/22
*
* IMITATOR version: 3.0
************************************************************)
(* MAX is now a parameter. We check that the channels cannot be both full (in_transit) *)
var x,z,u,v
: clock;
i, (* subscript of the chunk currently beeing processed (1<=i<=N) *)
rc, (* nb of attempt undertaken by S to retransmit d_i (0<=rc<=MAX) *)
b1,bN, rb1,rbN, (* these Boolean variables are used for communication between S-K-L-R *)
ab, rab, exp_ab (* to be sent/received/expected alternating bit *)
: discrete;
MAX = 2, (* maximal number of retransmissions *)
N = 2, (* number of chunks of a file *)
SYNC, (* delay added after a failure in order to assure
that S does not start transmitting a new file before
the receiver has properly reacted to the failure *)
TS, (* time-out of the sender for initiating a retransmission
when S has not received an ack from S *)
TR, (* time-out of the receiver for indicating failure
when R has not received the last chunk of a file *)
TD (* maximum delay in channel K (and L) *)
: parameter;
(****************************************************)
(****************************************************
****************************************************
AUTOMATA
****************************************************
****************************************************)
(****************************************************)
automaton sender
(****************************************************)
synclabs: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
loc idleS: invariant x>=0
when True sync S_in do {b1:=1,x:=0} goto next_frame;
urgent loc next_frame: invariant True
when i=N sync sndD do {bN:=1} goto wait_ack;
when i<N sync sndD do {bN:=0} goto wait_ack;
loc wait_ack: invariant x<=TS
when x=TS & rc=MAX & i=N sync S_DK do {x:=0,rc:=0,i:=1} goto error;
when x=TS & rc=MAX & i<N sync S_NOK do {x:=0,rc:=0,i:=1} goto error;
when x<TS sync rcvA do {ab:=1-ab,x:=0,rc:=0} goto success;
when x=TS & rc<MAX sync sndD do {rc:=rc+1,x:=0} goto wait_ack;
urgent loc success: invariant True
when i<N do {i:=i+1,b1:=0} goto next_frame;
when i=N sync S_OK do {i:=1} goto idleS;
loc error: invariant x <= SYNC
when x=SYNC do {ab:=0} goto idleS;
end (* sender *)
(****************************************************)
automaton receiver
(****************************************************)
synclabs: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
loc new_file: invariant True
when True sync rcvD do {z:=0} goto fst_safe;
urgent loc fst_safe: invariant True
when rb1=1 do {exp_ab:=rab} goto frame_received;
urgent loc frame_received: invariant True
when rab=exp_ab & rb1=1 & rbN=0 sync R_FST
do {rb1:=0,rab:=0} goto frame_reported;
when rab=exp_ab & rb1=0 & rbN=0 sync R_INC
do {rb1:=0,rab:=0} goto frame_reported;
when rab=exp_ab & rbN=1 sync R_OK
do {rb1:=0,rab:=0} goto frame_reported;
when rab=1-exp_ab sync sndA do {rb1:=0,rab:=0} goto idleR;
urgent loc frame_reported: invariant True
when True sync sndA do {exp_ab:=1-exp_ab,z:=0} goto idleR;
loc idleR: invariant z<=TR
when z<TR sync rcvD do {} goto frame_received;
when z=TR & rbN=0 sync R_NOK do {rbN:=0,exp_ab:=0} goto new_file;
when z=TR & rbN=1 do {rbN:=0,exp_ab:=0} goto new_file;
end (* receiver *)
(****************************************************)
automaton channelK
(****************************************************)
synclabs: sndD, rcvD, lostK;
loc startK: invariant u>=0
when True sync sndD do {u:=0} goto in_transitK;
loc in_transitK: invariant u<=TD
when True sync lostK goto startK;
when True do {rb1:=b1, rbN:=bN, rab:=ab} sync rcvD goto startK;
end (* channelK *)
(****************************************************)
automaton channelL
(****************************************************)
synclabs: sndA, rcvA, lostL;
loc startL: invariant v>=0
when True sync sndA do {v:=0} goto in_transitL;
loc in_transitL: invariant v<=TD
when True sync rcvA goto startL;
when True sync lostL goto startL;
end (* channelL *)
(************************************************************)
(* Initial state *)
(************************************************************)
init := loc[sender]=idleS
& loc[receiver]=new_file
& loc[channelK]=startK
& loc[channelL]=startL
& x=0 & z=0 & u=0 & v=0
& rc=0 & i=1 & ab=0
& b1=0 & bN=0 & rb1=0 & rbN=0
& rab=0 & exp_ab=0
& TD > 0
& TS > 0
& TR > 0
& SYNC > 0
;
artifact/assets/testcases/BRP/brp_Channels.imiprop 0 → 100644
View file @ 7a4b8040
(************************************************************)
(* Property specification *)
(************************************************************)
property := #synth AGnot(loc[channelK] = in_transitK & loc[channelL] = in_transitL)
artifact/assets/testcases/BRP/brp_GF_S_in_RC.imi 0 → 100644
View file @ 7a4b8040
(* monitor: GF S_in *)
(************************************************************
* IMITATOR MODEL
*
* BRP (Bounded Retransmission Protocol)
*
* Description : Bounded Retransmission Protocol [version slightly modified]
* Source : "The Bounded Retransmission Protocol Must Be on Time!"
* Author : Pedro R. D'Argenio , Joost-Pieter Katoen , Theo C. Ruys , G. Jan Tretmans
* Modeling : Laurent Fribourg
* Modified by : Laure Petrucci and Jaco van de Pol
*
* Created : ? (< 09/2007)
* Last modified : 2020/09/22
*
* IMITATOR version: 3.0
************************************************************)
var x,z,u,v
: clock;
i, (* subscript of the chunk currently beeing processed (1<=i<=N) *)
rc, (* nb of attempt undertaken by S to retransmit d_i (0<=rc<=MAX) *)
b1,bN, rb1,rbN, (* these Boolean variables are used for communication between S-K-L-R *)
ab, rab, exp_ab (* to be sent/received/expected alternating bit *)
: discrete;
MAX = 2, (* maximal number of retransmissions *)
N = 2, (* number of chunks of a file *)
SYNC, (* delay added after a failure in order to assure
that S does not start transmitting a new file before
the receiver has properly reacted to the failure *)
TS, (* time-out of the sender for initiating a retransmission
when S has not received an ack from S *)
TR, (* time-out of the receiver for indicating failure
when R has not received the last chunk of a file *)
TD (* maximum delay in channel K (and L) *)
: parameter;
(****************************************************)
(****************************************************
****************************************************
AUTOMATA
****************************************************
****************************************************)
(************************************************************)
automaton monitor
(************************************************************)
synclabs: S_in, sndD;
loc s0: invariant True
when True sync sndD goto s0;
when True sync S_in goto s0;
when True sync sndD goto s1;
accepting loc s1: invariant True
when True sync sndD goto s1;
end (* monitor *)
(****************************************************)
automaton sender
(****************************************************)
synclabs: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
loc idleS: invariant x>=0
when True sync S_in do {b1:=1,x:=0} goto next_frame;
urgent loc next_frame: invariant True
when i=N sync sndD do {bN:=1} goto wait_ack;
when i<N sync sndD do {bN:=0} goto wait_ack;
loc wait_ack: invariant x<=TS
when x=TS & rc=MAX & i=N sync S_DK do {x:=0,rc:=0,i:=1} goto error;
when x=TS & rc=MAX & i<N sync S_NOK do {x:=0,rc:=0,i:=1} goto error;
when x<TS sync rcvA do {ab:=1-ab,x:=0,rc:=0} goto success;
when x=TS & rc<MAX sync sndD do {rc:=rc+1,x:=0} goto wait_ack;
urgent loc success: invariant True
when i<N do {i:=i+1,b1:=0} goto next_frame;
when i=N sync S_OK do {i:=1} goto idleS;
loc error: invariant x <= SYNC
when x=SYNC do {ab:=0} goto idleS;
end (* sender *)
(****************************************************)
automaton receiver
(****************************************************)
synclabs: rcvD, sndA, R_NOK, R_OK, R_FST, R_INC;
loc new_file: invariant True
when True sync rcvD do {z:=0} goto fst_safe;
urgent loc fst_safe: invariant True
when rb1=1 do {exp_ab:=rab} goto frame_received;
urgent loc frame_received: invariant True
when rab=exp_ab & rb1=1 & rbN=0 sync R_FST
do {rb1:=0,rab:=0} goto frame_reported;
when rab=exp_ab & rb1=0 & rbN=0 sync R_INC
do {rb1:=0,rab:=0} goto frame_reported;
when rab=exp_ab & rbN=1 sync R_OK
do {rb1:=0,rab:=0} goto frame_reported;
when rab=1-exp_ab sync sndA do {rb1:=0,rab:=0} goto idleR;
urgent loc frame_reported: invariant True
when True sync sndA do {exp_ab:=1-exp_ab,z:=0} goto idleR;
loc idleR: invariant z<=TR
when z<TR sync rcvD do {} goto frame_received;
when z=TR & rbN=0 sync R_NOK do {rbN:=0,exp_ab:=0} goto new_file;
when z=TR & rbN=1 do {rbN:=0,exp_ab:=0} goto new_file;
end (* receiver *)
(****************************************************)
automaton channelK
(****************************************************)
synclabs: sndD, rcvD, lostK;
loc startK: invariant u>=0
when True sync sndD do {u:=0} goto in_transitK;
loc in_transitK: invariant u<=TD
when True sync lostK goto startK;
when True do {rb1:=b1, rbN:=bN, rab:=ab} sync rcvD goto startK;
end (* channelK *)
(****************************************************)
automaton channelL
(****************************************************)
synclabs: sndA, rcvA, lostL;
loc startL: invariant v>=0
when True sync sndA do {v:=0} goto in_transitL;
loc in_transitL: invariant v<=TD
when True sync rcvA goto startL;
when True sync lostL goto startL;
end (* channelL *)
(************************************************************)
(* Initial state *)
(************************************************************)
init := loc[sender]=idleS
& loc[receiver]=new_file
& loc[channelK]=startK
& loc[channelL]=startL
& loc[monitor]=s0
& x=0 & z=0 & u=0 & v=0
& rc=0 & i=1 & ab=0
& b1=0 & bN=0 & rb1=0 & rbN=0
& rab=0 & exp_ab=0
& SYNC >= TR
& TS > 2*TD
& TD > 0
& TR > 4*TS + 3*TD
;
artifact/assets/testcases/BRP/brp_GF_S_in_RC2.imi 0 → 100644
View file @ 7a4b8040
(* monitor: GF S_in *)
(************************************************************
* IMITATOR MODEL
*
* BRP (Bounded Retransmission Protocol)
*
* Description : Bounded Retransmission Protocol [version slightly modified]
* Source : "The Bounded Retransmission Protocol Must Be on Time!"
* Author : Pedro R. D'Argenio , Joost-Pieter Katoen , Theo C. Ruys , G. Jan Tretmans
* Modeling : Laurent Fribourg
* Modified by : Laure Petrucci and Jaco van de Pol
*
* Created : ? (< 09/2007)
* Last modified : 2020/09/22
*
* IMITATOR version: 3.0
************************************************************)
var x,z,u,v
: clock;
i, (* subscript of the chunk currently beeing processed (1<=i<=N) *)
rc, (* nb of attempt undertaken by S to retransmit d_i (0<=rc<=MAX) *)
b1,bN, rb1,rbN, (* these Boolean variables are used for communication between S-K-L-R *)
ab, rab, exp_ab (* to be sent/received/expected alternating bit *)
: discrete;
MAX = 2, (* maximal number of retransmissions *)
N = 2, (* number of chunks of a file *)
SYNC, (* delay added after a failure in order to assure
that S does not start transmitting a new file before
the receiver has properly reacted to the failure *)
TS, (* time-out of the sender for initiating a retransmission
when S has not received an ack from S *)
TR, (* time-out of the receiver for indicating failure
when R has not received the last chunk of a file *)
TD (* maximum delay in channel K (and L) *)
: parameter;
(****************************************************)
(****************************************************
****************************************************
AUTOMATA
****************************************************
****************************************************)
(************************************************************)
automaton monitor
(************************************************************)
synclabs: S_in, sndD;
loc s0: invariant True
when True sync sndD goto s0;
when True sync S_in goto s0;
when True sync sndD goto s1;
accepting loc s1: invariant True
when True sync sndD goto s1;
end (* monitor *)
(****************************************************)
automaton sender
(****************************************************)
synclabs: S_in, rcvA, sndD, S_DK, S_NOK, S_OK;
loc idleS: invariant x>=0
when True sync S_in do {b1:=1,x:=0} goto next_frame;
urgent loc next_frame: invariant True
when i=N sync sndD do {bN:=1} goto wait_ack;
when i<N sync sndD do {bN:=0} goto wait_ack;
loc wait_ack: invariant x<=TS
when x=TS & rc=MAX & i=N sync S_DK do {x:=0,rc:=0,i:=1} goto error;
when x=TS & rc=MAX & i<N sync S_NOK do {x:=0,rc:=0,i:=1} goto error;
when x<TS sync rcvA do {ab:=1-ab,x:=0,rc:=0} goto success;
when x=TS & rc<MAX sync sndD do {rc:=rc+1,x:=0} goto wait_ack;
urgent loc success: invariant True
when i<N do {i:=i+1,b1:=0} goto next_frame;
when i=N sync S_OK do {i:=1} goto idleS;
loc error: invariant x <= SYNC
when x=SYNC do {ab:=0} goto idleS;
end (* sender *)