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

mode -R

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

parsed net exo2

5 places, 4 transitions, 12 arcs

net exo2
tr t0 lit -> dort lock
tr t1 dort lock -> lit
tr t2 ecrit -> dort2 lock3
tr t3 dort2 lock3 -> ecrit
pl dort (4)
pl dort2 (2)
pl lock (3)

0.000s

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

bounded

5 marking(s), 8 transition(s)

MARKINGS:

0 : dort4 dort22 lock3
1 : dort3 dort22 lit lock2
2 : dort4 dort2 ecrit
3 : dort2 dort22 lit2 lock
4 : dort dort22 lit3

REACHABILITY GRAPH:

0 -> t1/1, t3/2
1 -> t0/0, t1/3
2 -> t2/0
3 -> t0/1, t1/4
4 -> t0/3

0.000s

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

live
reversible

0 dead marking(s), 5 live marking(s)
0 dead transition(s), 4 live transition(s)

STRONG CONNECTED COMPONENTS:

0 : 4 3 2 1 0

SCC GRAPH:

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

0.000s

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