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 nonempty subsets of transitions in $T$ (hence $R \subseteq P(T)$, the powerset of $T$). The idea is that all the transitions in an element $r$ of $R$ should be fired at the exact same time.
We support a textual format for PTPN that extends the syntax of Tina’s net file.
In this context, a PTPN file for the net $(N, R)$ is a .net file for net $N$,
in Tina’s syntax, in which
there is one line of the form pxl t1 ... tk
for each firing set $r = {t_1,
\dots t_k}$ in $R$^{1}.
We give a minimal example of PTPN file below.
pl p1 (1)
tr t1 : b [3,5] p2 > p1
tr t2 : a [2,3] p1 > p0
tr t3 : b [1,2] p0 > p1
tr t4 : a [0,w[ p0 > p2
tr t5 : a ]3,6[ p2 > p2
pxl t1 t3
pxl t2 t4 t5
There are some restrictions:
 all the transitions that occur in the same firing set should have the same label (or they should all be without label); this is the label used when firing the firing set
 all pairs of firing sets should be non comparable; one set cannot be included in another one
 transitions in the same firing set should be independent (have distinct set of input places); hence they can always be fired simultaneously
It is possible to generate a PTPN file with Twina using option net
. For
instance, we can generate the twinplant model for the TPN in file
faulted.net
with
respect to fault $f$ using a command such as:
$ twina net parse fault=f twin faulted.net
#
# net twin_simplefault_f
# 6 places, 7 transitions
#
pl {p2.1}
pl {p1.1} (1)
pl {p0.1}
pl {p2.2}
pl {p1.2} (1)
pl {p0.2}
tr {t1.1} : b [3,5] {p2.1} > {p1.1}
tr {t2.1} : a [2,3] {p1.1} > {p0.1}
tr {t3.1} : b [1,2] {p0.1} > {p1.1}
tr {t4.1} : f [0,w[ {p0.1} > {p2.1}
tr {t1.2} : b [3,5] {p2.2} > {p1.2}
tr {t2.2} : a [2,3] {p1.2} > {p0.2}
tr {t3.2} : b [1,2] {p0.2} > {p1.2}
pxl {t1.1} {t1.2}
pxl {t1.1} {t3.2}
pxl {t2.1} {t2.2}
pxl {t3.1} {t1.2}
pxl {t3.1} {t3.2}
PTPN Scripts
We also provide a simple scripting language for composing PTPN files, similar to the TPN format of Tina. A script manages a stack of nets and is built as a sequence of commands, one command per line, using operators like:

load model.net
, to push a fresh copy of a net defined in filemodel.net
on the stack (paths are not accepted) 
new
, push a new, empty net at the top of the stack. All the declarations used in a net file are also accepted (tr
for creating a new transition,pl
for places, etc.) 
dup n
, for pushing n copies of the toplevel net on the stack 
intersect o1 ... on
, for computing the PTPN product of the two toplevel nets in the stack relative to set ${o_1, …, o_n}$. We compute the product over all the common labels when the set is empty 
remove a
, to remove all transitions with labela
from the toplevel net in the stack 
ren a1/b1 ... ak/bk
, for the relabeling of transitions. Transitions with labelbi
, before, are now labeled withai
after executing the command. Commandren /b
can be used to remove (hide) the labelb
. All renaming and/or hidings are applied simultaneously 
merge n
, replaces the n toplevel nets in the stack with their free product (juxtaposition, preserving labels) 
sync n
, replaces the n toplevel nets in the stack with their synchronous composition , where we “fuse” copies of transitions with the same labels
With PTPN scripts, we can implement the equivalent of the command twina
fault=f twin faulted.net
by evaluating the following sequence of
commands, see file
faulted.tpn . In our case, the last command
in this script is a shorthand for intersect a b
.
load faulted.net
dup 1
remove f
intersect
A script file can be used directly with Twina.
$ twina fault=f twin faulted.net
3 classe(s), 3 marking(s), 3 domain(s), 3 transition(s)
0.000s
$ twina faulted.tpn
3 classe(s), 3 marking(s), 3 domain(s), 3 transition(s)
0.001s
$ twina net parse faulted.tpn
#
# net {(simplefault.1 + simplefault.2)}
# 6 places, 7 transitions
#
pl {p2.1}
pl {p1.1} (1)
pl {p0.1}
pl {p2.2}
pl {p1.2} (1)
pl {p0.2}
tr {t1.1} : b [3,5] {p2.1} > {p1.1}
tr {t2.1} : a [2,3] {p1.1} > {p0.1}
tr {t3.1} : b [1,2] {p0.1} > {p1.1}
tr {t1.2} : b [3,5] {p2.2} > {p1.2}
tr {t2.2} : a [2,3] {p1.2} > {p0.2}
tr {t3.2} : b [1,2] {p0.2} > {p1.2}
tr {t4.2} : f [0,w[ {p0.2} > {p2.2}
pxl {t1.1} {t1.2}
pxl {t1.1} {t3.2}
pxl {t2.1} {t2.2}
pxl {t3.1} {t1.2}
pxl {t3.1} {t3.2}

PTPN files are not syntactically correct .net files and therefore cannot be used with tools in the Tina toolbox. ↩︎