A realtime model-checker for analyzing Twin-TPN

Twina is a tool for analyzing the “product” of two Time Petri Nets (TPN), with
possibly inhibitor and read arcs. Its main objective is to compute a usable
representation of the intersection of two *net languages*; meaning the
intersection of the (timed) languages obtained from the executions of two TPN,
in which transitions with the same labels are fired at the same date.

Another possible use of Twina is to check the *diagnosability* of a net, using
an approach similar to the *twin-plant method*, but applicable on TPN.

The tool is based on a new extension of the State Class Graph construction, the method used in the TINA (TIme petri Net Analyzer) toolbox. Like for TINA, this tool is maintained by the Verification of Time Critical Systems (VERTICS) group, which develops new verification methods and tools for checking properties of critical systems having strong temporal and timing requirements. General information about Petri nets can be found on the Petri Nets World site.

`0629ff2`

, March 2020)64 bits versions; other targets possible on request, see here.

`twina (Linux)`

twina for PCs under Linux: ELF
64-bit LSB executable, x86-64

`twina.exe (Windows)`

twina for PCs under Windows: PE32+
executable (console) x86-64

`twina (Darwin)`

twina for Intel Macs under
MacOS 10.10 and above

`vertics/twina`

a
Docker image for twina based on Ubuntu Bionic

Simply download the right executable for your OS and put it in a place where it
can be found by your shell (this may include updating your `PATH`

variables).

Twina can construct the State Class Graph from nets described in the same
textual format than Tina (see information on the `.net`

format in the
Tina
manual pages). The result
should be similar to what is obtained with Tina’s option `-W`

.

```
$ twina ifip.net
12 classe(s), 8 marking(s), 12 domain(s), 29 transition(s)
0.000s
```

In this example ( ), taken from [Berthomieu83], we have only 8 different reachable markings but 12 different classes. You may find examples of nets on the examples page or in the distribution of Tina. Alternatively, you can edit nets using nd (NetDraw), a GUI for Petri nets, Time Petri Nets and Automata that is distributed with Tina, and save your net in text format (using the textify command in nd).

For more information on Twina, you can have a look at the how-to page.

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

This post is used to collect most of the models used in our experiments, with a reference to the original paper where they appear when possible.
Examples of TPN (from the Tina distribution) Alternating Bit Protocol abp.net IFIP example taken from [Berthomieu83]: ifip.net Level-crossing example with 3 trains: train3.net Intersection of TPN The two basic examples used in our [Formats19] paper: C1.net and C2.

Since version 0.9 of Twina, it is possible to use two new kinds of input formats for nets, in addition to the original net format of Tina (and the implicit nets obtained from the use of options -I and -twin).
Product TPN Product Time Petri Net (PTPN) are an extension of “classical” TPN in which it is possible to fire several transitions synchronously. A Product TPN is the composition $(N,R)$ of a net $N$, with transitions $T$, and a (product) relation, $R$, that is a collection of firing sets $r_1 ,…, r_n$, which are non-empty subsets of transitions in $T$ (hence $R \subseteq P(T)$, the powerset of $T$).

A State Class Construction for Computing the Intersection of Time Petri Nets Languages

The following posts describe how to reproduce the experiments reported in our [Formats19] paper.

A New Product Construction for the Diagnosability of Patterns in Time Petri Net

The following posts describe how to reproduce the experiments reported in our 2020 (submitted) paper about diagnosability of patterns and single-faults in Time Petri Net.