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
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
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
manual pages). The result
should be similar to what is obtained with Tina’s option
$ 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.
A State Class Construction for Computing the Intersection of Time Petri Nets Languages
A New Product Construction for the Diagnosability of Patterns in Time Petri Net
The easiest way to contact us is through the TINA mailing list. Subscribe or update your list subscription(s) at:
Send submissions to email@example.com
For bug reports or additional information specifically about Twina, please contact: