# Diagnosability of Patterns and Single-Faults

This post is **part I** of a series of articles describing how to reproduce the
experiments reported in our 2020 (submitted) paper about Twina. We assume that
you already installed Twina and a recent release of Tina. You can also install a
Docker image containing all the necessary tools, scripts and model files:

```
docker pull vertics/twina
```

## Diagnosability of Single-Faults

We have three different methods for deciding the diagnosability of a single
fault. Each method use a different option provided by Twina. We give, in each
case, an example of how to apply these methods taking as model a simple instance
of the *WODES diagnosis benchmark* of Giua with added timing constraints
(*
wodes *) and the fault label $F1$.
This system is not diagnosable.

- the first method relies on option
`-twin`

, that computes the state class graph for the “twin-product” of a net given a fault label $f$. In this case we need to check the LTL formula`(<> f) => (<> dead);`

- the second method relies on the use of the
PTPN scripting
language to build the twin plant model. We give more explanation
on this construction below. In this case we need to check the LTL formula
`(<> f.1) => <>(f.2 \/ dead);`

- the last method relies on option
`-diag`

, for testing diagnosability of single faults using a dedicated on-the-fly algorithm (meaning that we avoid computing the whole state space of the system when not necessary). When the system is not diagnosable, it is possible to print a counter-example using the verbose output mode, option`-v`

For method (1) and (2), we need to compute the state class graph in a format
than can be used as an input with `selt`

, our LTL model-checker. (We only need
information regarding the labels of transitions.) To this end we use a
combination of options `-aut`

and `-lt`

and the `ktzio`

tool from the Tina
toolbox. Options `-q`

and `-b`

of `selt`

are used to print only the truth
value of the formula.

### Method 1

```
$ twina -twin --fault=F1 -lt -aut wodes.net | ktzio -AUT - wodes.ktz
$ selt -q -b wodes.ktz -f "(<> F1) => (<> dead);"
FALSE
```

We generate a SCG with 55 402 classes, corresponding to a ktz file of size 284K. The overall computation time is about 3s.

### Method 2

```
$ cat wodes.tpn
load wodes.net
ren F1.1/F1
load wodes.net
ren F1.2/F1
intersect TTe TTs TT1_3 TT2_3
$ twina -aut -lt wodes.tpn | ktzio -AUT - wodes.ktz
$ selt -q -b wodes.ktz -f "(<> {F1.1}) => <>({F1.2} \/ dead);"
FALSE
```

We generate a SCG with 205 140 classes, corresponding to a ktz file of size 1.2M. The overall computation time is about 12s. We can further simplify this method by removing the transitions with label F1.2 in the result (and use the same approach than in method 1).

### Method 3

```
$ twina -diag --fault=F1 -twin wodes.net
# net is not diagnosable
# length: 54
#
# states (explored): 293
# markings: 97
# dbms: 289
0.003s
```

This method is generally better when the system is not diagnosable. In our example, it returns a result after exploring only 293 classes (instead of 55 402). We also do not need to serialize the SCG before loading it in the model-checker. On the opposite, this approach enumerates the Strongly Connected Components of the system. Hence it may be less beneficial when the system is diagnosable.

## Pattern Diagnosability

Our method can be naturally extended to check for the diagnosability of
*patterns of unobservable events*. In our case, a pattern $M$ is a special
instance of TPN. We denote $F$ the set of labels occurring in $M$ and we
distinguish a place in $M$, say *found*, that is a witness for detection.

Instead of defining a pattern as a regular language, or as a set of timed
sequences, we use instead the timed language of $M$. Hence we restrict ourselves
to *time regular languages*, meaning sets of executions that can be realized
with a TPN. This is enough to model every regular set of (untimed) traces.

We also want to make sure that a pattern does not interfere with the system it interacts with. For example, it should not prevent some executions of the system. To this end, we impose three well-formedness conditions on patterns:

- patterns are total; they should always allow transitions on the labels in $F$, at any time (they never block or delay a transition)
- patterns are deterministic (the same observations should lead to the same states)
- labels in $F$ are unobservable

We use an example based on the model of a *product transportation system* with
added timing constraints (*
transport_timed *) and the
pattern (*
omega *) display in Fig. 2.

By analogy with our previous definition of diagnosability, we say that pattern $M$ is diagnosable if it is not possible to find a (critical) pair of executions such that $M$ is found in one but never in the other. We can again reduce this question to a model-checking problem on a twin-plant; this time on the product of the system with the pattern.

```
$ 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);"
TRUE
```

Unlike the previous methods, we need to generate a SCG that contains information
about the markings of each state; hence the use of option `-kaut`

with Twina.
We also need to adapt the LTL formula to check whether we found the pattern in
the first or second component of the product.

The pattern is diagnosable in the (timed) instance of the transport model that
we use (*
transport_timed *). At the
opposite, the pattern is not diagnosable if we use the untimed version
(*
transport.net *).

## Examples used in this post

- wodes.net
- wodes.tpn, a TPN script for the wodes benchmark
- transport_timed.net, a timed instance of transport.net
- omega, a pattern for the property “at least three F1 without F2”