Tina version 3.7.5 – 03/29/23 – LAAS/CNRS

mode -R

INPUT NET —————————————————––

parsed net feu

6 places, 6 transitions, 12 arcs

net feu
tr t0 r -> v
tr t1 v -> o
tr t2 o -> r
tr t3 r2 -> v2
tr t4 v2 -> o2
tr t5 o2 -> r2
pl v (1)
pl v2 (1)

0.000s

REACHABILITY ANALYSIS —————————————––

bounded

9 marking(s), 18 transition(s)

MARKINGS:

0 : v v2
1 : o v2
2 : o2 v
3 : r v2
4 : o o2
5 : r2 v
6 : o2 r
7 : o r2
8 : r r2

REACHABILITY GRAPH:

0 -> t1/1, t4/2
1 -> t2/3, t4/4
2 -> t1/4, t5/5
3 -> t0/0, t4/6
4 -> t2/6, t5/7
5 -> t1/7, t3/0
6 -> t0/2, t5/8
7 -> t2/8, t3/1
8 -> t0/5, t3/3

0.000s

LIVENESS ANALYSIS ———————————————–

live
reversible

0 dead marking(s), 9 live marking(s)
0 dead transition(s), 6 live transition(s)

STRONG CONNECTED COMPONENTS:

0 : 8 7 6 5 4 3 2 1 0

SCC GRAPH:

0 -> t0/0, t3/0, t2/0, t5/0, t1/0, t4/0

0.000s

ANALYSIS COMPLETED –––––––––––––––––––––––