# TW​♊︎​NA

A realtime model-checker for analyzing Twin-TPN

# The Twin TPN Analyzer

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.

## Release 0.9 (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

## Installation

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

## Usage

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.

### Use Cases and Benchmarks

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.

### Product TPN and PTPN Scripts

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$).

# Language Intersection and TPN

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.

# Product TPN and Diagnosability

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.

# Contact

The easiest way to contact us is through the TINA mailing list. Subscribe or update your list subscription(s) at:

Send submissions to tina-users@laas.fr