TW​♊︎​NA

A realtime model-checker for analyzing Twin-TPN

Windows executable (.exe) Download for another OS

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.

Download

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.

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

Howto

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 (.
Silvano
Last updated on Apr 1, 2020

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.
Silvano
Last updated on Apr 1, 2020

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$).
Silvano
Apr 5, 2020

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.

Diagnosability of TPN
Checking Properties with Language Intersection
Reproducing the Benchmarks for our 2019 Paper
Inhibition and Permission TPN (IPTPN)

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.

Diagnosability of Patterns and Single-Faults
Reproducing the Benchmarks of our 2020 Paper

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

For bug reports or additional information specifically about Twina, please contact: