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