# 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 nets; meaning TPN where all observable transitions have
trivial time constraints (their time interval is $[0, \infty[$]). With this
extension, it is always possible to build a composable IPTPN from a TPN.

For example, Fig. 1 and 2 below display two TPN and Fig. 3 displays the IPTPN corresponding to their product. In this construction, we create a silent, extra-transition $tc_i$ for every non-trivial observable transition $t_i$. These transitions cannot fire (they self-inhibit themselves with an inhibitor arc —○) but “record the timing constraints” of the transition they are associated with. Then a permission arc ( —●) is used to transfer these constraints on the (product of) labeled transitions.

Option `-iptpn`

is used to generate a TPN (in .net or .tpn syntax) that can be
analyzed using Tina. This option can be used to generate an IPTPN from: (1) the
product of two nets (together with option `-I`

); (2) the “twin-plant”
construction (`-twin`

); or (3) just from a single net alone. In the resulting
net, the silent (timed) transition corresponding to $tc_i$ is named `{ti.t}`

.

```
$ twina -iptpn -fault=a C1.net
#
# net C1
# 2 places, 2 transitions + 1 tc transitions
#
pl p0 (1)
pl p1 (1)
tr t0 : a [0,w[ p0 ->
tr t1 : b p1 ->
tr {t1.t} [0,1] p1 ->
pr {t1.t} -o {t1.t}
pr {t1.t} -* t1
```

To use the resulting net with Tina you only need to set an environment variable
called IPTPN (to a non-zero value). Then you may directly pipe the result to
Tina, like in the following example. (our example below use `sift`

, an
optimized tool for state-space generation.)

```
$ export IPTPN=1
$ twina -iptpn -I C1.net C2.net | sift -
3 marking(s), 3 domain(s), 3 classe(s), 2 transition(s)
0.000s
```

## Examples used in this post

The basic examples of nets used in our paper C1.net and C2.net .