TW♊︎NA

A realtime model-checker for analyzing Twin-TPN

  Windows executable (.exe) Download for another OS

Download

Release 0.6 (3d18676, March 2019)

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
8 marking(s), 12 domain(s), 12 classe(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.

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

News and Informations

You can find a list of possible options for the tool using option -h. $ twina -h Usage of twina: -I compute LSCG for the intersection …

A possible application of our product construction is for model checking TPN, in much the same way some observer-based verification …

One possible application of Twina, and our initial motivation for this work, is to check the diagnosability of a TPN. We consider a …

This post describe a minimal setting for reproducing the experiments reported in our conference paper. We assume that you already …

Berthomieu et al. [PBV2011] define an extension of TPN with inhibition and permission that provides a method for building composable …

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: