# TW♊︎NA

A realtime model-checker for analyzing Twin-TPN

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

### Checking Properties with Language Intersection

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

### Diagnosability of TPN

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

### Reproducing our Benchmarks

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

### Inhibition and Permission TPN (IPTPN)

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