# How to Use Twina

You can find a list of possible options for the tool using option `-h`

.

```
$ twina -h
Usage of twina.exe:
-I compute LSCG for the intersection of twin-nets
-P use product-nets instead of twin-nets when used with options -I or -twin
-S compute the Strong State Class Graph (SSCG) for one net, preserves LTL
-W compute the Linear State Class Graph (LSCG) for one net, preserves LTL (DEFAULT)
-aut transition system output (.aut format)
-diag test diagnosability for one fault and returns a counter-example if not (see option --fault=label)
-fault=string label used in the twin machine construction (default "_")
-iptpn output a net with IPTPN arcs then quit (set -p)
-kaut transition system with state properties encoded (.aut format)
-lt prints labeled transition properties
-net prints the net being evaluated
-parse just parses and check input
-twin compute LSCG for the twin machine (see option --fault=label)
-v textual output (full)
files:
infiles: input file is stdin when using -
outfile: output is always on stdout
errorfile: error are always printed on stderr
```

By default `twina`

uses option `-W`

, that computes the (Linear) State Class
Graph, or LSCG for short, for the system given as input. The LSCG is a
deterministic automata that defines exactly the possible traces of a system
(when the TPN is bounded); hence the reason why the LSCG preserves linear time
properties (LTL).

## Basic Usage and Display Options

By default, Twina gives you some statistics on the size of the generated graph, while option
`-v`

gives you a full textual output of the LSCG, complete with
information on timing constraints (in the form of *Difference Bound Matrices*).
With option `-lt`

you may also display the labels associated with the
transitions that are fired. (In this case *silent actions* have label `i`

.)

It is possible to generate an *automaton* view of the LSCG in the
AUT
format (option `-aut`

),
the LTS description format of the Aldebaran tool of the CADP toolset. This
format can be used with NetDraw. There is also option `-kaut`

to export a
specification in AUT format in which state properties (markings) are encoded as
simple loops; see option `-sp 2`

of tina. This option is useful if you need to
test the equivalence between different State Class Graphs or to export the
result in the KTZ format, a compressed format for transition system used in the
Tina toolbox.

## Intersection (option `-I`

)

Twina can generate a LSCG for the (synchronous) product of two TPN, that is a
state class graph containing only the executions that are *common* to both nets.
Intuitively, a trace is common to two nets `A`

and `B`

if we can find a pair
of executions, $(\sigma_A, \sigma_B)$, one in each net, such that any labelled
transition in $\sigma_A$ can be uniquely matched to a transition with the same
label in $\sigma_B$, at the same date and in the same order (and vice versa).

When the two nets have the same set of labels (same alphabet) the set of common traces corresponds to language intersection. This methods can be used even when the two TPN have transitions sharing the same label and that have a non-trivial timing constraints (i.e. different from $[0, +\infty[$); that is even if we cannot compose the two nets together.

You can generate the LSCG for the intersection of two TPN using option `-I`

.
For example, if we consider the running example of
[Formats19] (see files
C1.net and
C2.net ).

```
$ twina -v -lt -I C1.net C2.net
# states 3
# transitions 2
class 0
marking: {p0.1} {p1.1} {p0.2}
domain:
0 <= {t0.1} < w
0 <= {t1.1} <= 1
0 <= {t0.2} < w
successors: {t0.1}|{t0.2}:"a"/1
class 1
marking: {p1.1} {p1.2}
domain:
0 <= {t1.1} <= 1
1 <= {t1.2} < w
successors: {t1.1}|{t1.2}:"b"/2
class 2
marking:
domain:
successors:
```

In the resulting SCG, places and transitions from the first net are suffixed
with `.1`

, and are suffixed with `.2`

for the second net. We can see from
the result that, initially, only transitions labelled with `a`

can be fired
(i.e. `t0`

from `C1`

at the same time than `t0`

from `C2`

). This
corresponds to the “product” transition `{t0.1}|{t0.2}`

in the product TPN.
Looking at the timing constraints, we can also deduce that these transitions
should fire before 1 unit of time.

## Twin-Plant Method for TPN (options `-twin`

and `-diag`

)

It is possible to distinguish a particular label, say `f`

, using option
`--fault=f`

. This *fault label* can be interpreted as the label of actions
corresponding to a silent failure in the system.

The *twin-plant* of a net, `A`

, is defined as the product of `A`

with a copy
of itself where every transitions labelled with the fault `f`

have been
removed. For instance, this is the result of analyzing the twin-plant for model
jdedstimed that is part of our
examples.

```
$ twina -twin -fault=f jdedstimed.net
544 classe(s), 121 marking(s), 489 domain(s), 1144 transition(s)
0.004s
```

This construction is interesting since the twin plant can be used to check if
there are failed executions in `A`

(meaning executions that have triggered a
fault) that can be mistaken with non-faulty one. In this case one can say that
the net is *not diagnosable*.

It is possible to detect that a system is not diagnosable without generating all
the reachable classes of a net. Indeed, it is enough to stop when we find an
inifinite trace (a loop) that contains label `f`

in the LSCG of the twin
machine. To this end, we have implemented a dedicated on-the-fly diagnosability
check in Twina (see option `-diag`

).

In our example, we find that the system is not diagnosable after generating only
110 classes. It is also possible to print (a textual representation of) the
counter-example using option `-v`

.

```
$ twina -diag --fault=f jdedstimed.net
# net is not diagnosable
# length: 40
#
# states (explored): 110
# markings: 57
# dbms: 97
0.000s
$ twina -diag --fault=f -v -lt jdedstimed.net
# net is not diagnosable
# length: 40
class 0
marking: {p0.1} {p1.1} {p0.2} {p1.2}
domain:
2 <= {t0.1} <= 8
4 <= {t1.1} <= 6
2 <= {t0.2} <= 8
4 <= {t1.2} <= 6
----[{t0.1}:"i"]--------->
class 1
marking: {p2.1} {p1.1} {p0.2} {p1.2}
domain:
0 <= {t1.1} <= 4
0 <= {t0.2} <= 6
0 <= {t1.2} <= 4
{t1.1} - {t1.2} <= 2
{t0.2} - {t1.1} <= 4
{t0.2} - {t1.2} <= 4
{t1.2} - {t1.1} <= 2
----[{t1.1}:"i"]--------->
[...]
```

We still have some limitations at the moment. For instance, Twina may return a “non-optimal” counter-example (not among the shortest ones). We may also return a counter-example where the fault needs to be fired an unbounded number of times. We plan to provide new options in order to overcome these limitations.

## Inhibition-Permission TPN (options `-iptpn`

)

There is already an extension of TPN, available in Tina, that can be used to
“compute the product of two nets” even when they are *not syntactically
composable*. In this extension, called IPTPN, we can use two new kinds of arcs
between transitions: one that can inhibit a transition (akin to a priority); and
the dual relation, where a transition can “permit” another one to fire. This
extension has been detailed in
[DEDS2011].

Unlike our approach, IPTPN are strictly more expressive than TPN and they
require to use a more precise State Class Graph construction called SSCG (for
Strong SCG). It is possible to check nets with IPTPN arcs in Tina by declaring a
shell variable called `IPTPN`

in your environment.

To compare the two aproaches, we provide the possibility to generate an IPTPN net from a twin-plant or the intersections of two TPN. This net (in tpn format) can be directly passed to Tina on the standard input. This option supports input nets that have priorities between transitions.

```
$ export IPTPN=1
$ twina --fault=f -twin -iptpn jdedstimed.net | sift -
121 marking(s), 398 domain(s), 706 classe(s), 1432 transition(s)
0.016s
```

In this case, the *strong* SCG (SSCG) has 706 classes, compared to only 544
classes in the LSCG computed by Twina. Indeed, it is often the case that the
strong SCG has far more classes than the related linear one.