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 non-empty 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$¹.

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 twin-plant 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 file model.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 top-level net on the stack

• intersect o1 ... on, for computing the PTPN product of the two top-level 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 label a from the top-level net in the stack

• ren a1/b1 ... ak/bk, for the relabeling of transitions. Transitions with label bi, before, are now labeled with ai after executing the command. Command ren /b can be used to remove (hide) the label b. All renaming and/or hidings are applied simultaneously

• merge n, replaces the n top-level nets in the stack with their free product (juxtaposition, preserving labels)

• sync n, replaces the n top-level 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}