Reproducing the Benchmarks of our 2020 Paper

This post is part II of a series of articles describing how to reproduce the experiments reported in our 2020 (submitted) paper about Twina. See part I.

Pattern Diagnosability on the Product Transportation System

In this post we consider the model of a product transportation system with added timing constraints displayed in Fig. 1.

As in part I, we consider the diagnosability with respect to omega , a pattern for property “at least three F1 before a F2”. Hence the observable labels in this example are U, D, PR1, PR2, ERR1, ERR2, ELR1 and ELR2.

It is possible to check the diagnosability of the pattern using a sequence of bash commands such as:

$ cat transport.tpn
load transport_timed.net
load omega.net
intersect
dup 1
intersect U D PR1 PR2 ERR1 ERR2 ELR1 ELR2
$ twina -kaut transport.tpn | ktzio -tina -AUT - transport.ktz
$ selt -q -b transport.ktz -f "(<> {found.1.1}) => <>({found.1.2} \/ dead);"
FALSE

We have tested the diagnosability of the system for several choices of timing constraints for the transitions t6 (label U, denoting a product going Up the elevator), t7 (label D, denoting a product going Down the elevator), t10 and t14 (silent, non-observable transitions.). The result depends on the timing constraints: let X be the (static) time interval for t6, Y for t7 and Z for t10 and t14.

• $X = Y = Z = [0, \infty[$: the system is not diagnosable and has 126 548 classes. The system without any timing constraint leads to a state space with 14 270 markings
• $X = Y = [0, \infty[$ and $Z = [0, 6]$: the system is not diagnosable and has 129 096 classes
• $X = Y = [0, \infty[$ and $Z = [1, 6]$: the system is diagnosable and has 15 848 classes
• $X = Y = [1, 10]$ and $Z = [0, \infty[$: the system is diagnosable and has only 2186 classes

The time needed to generate the state space in the most complex case is about 4.5s on a laptop (see model transport_bigger ), and under 10ms for the models with less than 20 000 classes.