# 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.