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

mode -R

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

parsed net exo3

9 places, 5 transitions, 19 arcs

net exo3
tr t0 p0 p6 -> p1
tr t1 p1 p5 -> p2 p7
tr t2 p2 p7 -> p3 p5
tr t3 p3 p5 p7 -> p4
tr t4 p4 -> p5 p6 p8
pl p0 : {entrée piscine} (999)
pl p5 : M (3)
pl p6 : N (3)
pl p8 : {quitte piscine}

0.001s

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

bounded

39 marking(s), 58 transition(s)

MARKINGS:

0 : p0999 p53 p63
1 : p0998 p1 p53 p62
2 : p0997 p12 p53 p6
3 : p0998 p2 p52 p62 p7
4 : p0996 p13 p53
5 : p0997 p1 p2 p52 p6 p7
6 : p0998 p3 p53 p62
7 : p0996 p12 p2 p52 p7
8 : p0997 p22 p5 p6 p72
9 : p0997 p1 p3 p53 p6
10 : p0996 p1 p22 p5 p72
11 : p0996 p12 p3 p53
12 : p0997 p2 p3 p52 p6 p7
13 : p0996 p23 p73
14 : p0996 p1 p2 p3 p52 p7
15 : p0997 p32 p53 p6
16 : p0997 p2 p4 p5 p6
17 : p0996 p22 p3 p5 p72
18 : p0996 p1 p32 p53
19 : p0996 p1 p2 p4 p5
20 : p0997 p2 p52 p62 p8
21 : p0996 p2 p32 p52 p7
22 : p0996 p22 p4 p7
23 : p0996 p1 p2 p52 p6 p8
24 : p0996 p33 p53
25 : p0996 p2 p3 p4 p5
26 : p0996 p22 p5 p6 p7 p8
27 : p0995 p12 p2 p52 p8
28 : p0996 p2 p3 p52 p6 p8
29 : p0995 p1 p22 p5 p7 p8
30 : p0995 p1 p2 p3 p52 p8
31 : p0995 p23 p72 p8
32 : p0995 p22 p3 p5 p7 p8
33 : p0995 p2 p32 p52 p8
34 : p0995 p22 p4 p8
35 : p0995 p22 p5 p6 p82
36 : p0994 p1 p22 p5 p82
37 : p0994 p23 p7 p82
38 : p0994 p22 p3 p5 p8*2

REACHABILITY GRAPH:

0 -> t0/1
1 -> t0/2, t1/3
2 -> t0/4, t1/5
3 -> t0/5, t2/6
4 -> t1/7
5 -> t0/7, t1/8, t2/9
6 -> t0/9
7 -> t1/10, t2/11
8 -> t0/10, t2/12
9 -> t0/11, t1/12
10 -> t1/13, t2/14
11 -> t1/14
12 -> t0/14, t2/15, t3/16
13 -> t2/17
14 -> t1/17, t2/18, t3/19
15 -> t0/18
16 -> t0/19, t4/20
17 -> t2/21, t3/22
18 -> t1/21
19 -> t1/22, t4/23
20 -> t0/23
21 -> t2/24, t3/25
22 -> t2/25, t4/26
23 -> t0/27, t1/26
24 ->
25 -> t4/28
26 -> t0/29, t2/28
27 -> t1/29
28 -> t0/30
29 -> t1/31, t2/30
30 -> t1/32
31 -> t2/32
32 -> t2/33, t3/34
33 ->
34 -> t4/35
35 -> t0/36
36 -> t1/37
37 -> t2/38
38 ->

0.000s

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

not live
not reversible

3 dead marking(s), 3 live marking(s)
0 dead transition(s), 0 live transition(s)

dead marking(s): 38 33 24

STRONG CONNECTED COMPONENTS:

0 : 24
1 : 33
2 : 38
3 : 37
4 : 36
5 : 35
6 : 34
7 : 32
8 : 30
9 : 28
10 : 25
11 : 21
12 : 31
13 : 29
14 : 26
15 : 22
16 : 17
17 : 13
18 : 18
19 : 27
20 : 23
21 : 19
22 : 14
23 : 10
24 : 11
25 : 7
26 : 4
27 : 15
28 : 20
29 : 16
30 : 12
31 : 8
32 : 9
33 : 5
34 : 2
35 : 6
36 : 3
37 : 1
38 : 0

SCC GRAPH:

0 ->
1 ->
2 ->
3 -> t2/2
4 -> t1/3
5 -> t0/4
6 -> t4/5
7 -> t2/1, t3/6
8 -> t1/7
9 -> t0/8
10 -> t4/9
11 -> t2/0, t3/10
12 -> t2/7
13 -> t1/12, t2/8
14 -> t0/13, t2/9
15 -> t2/10, t4/14
16 -> t2/11, t3/15
17 -> t2/16
18 -> t1/11
19 -> t1/13
20 -> t0/19, t1/14
21 -> t1/15, t4/20
22 -> t1/16, t2/18, t3/21
23 -> t1/17, t2/22
24 -> t1/22
25 -> t1/23, t2/24
26 -> t1/25
27 -> t0/18
28 -> t0/20
29 -> t0/21, t4/28
30 -> t0/22, t2/27, t3/29
31 -> t0/23, t2/30
32 -> t0/24, t1/30
33 -> t0/25, t1/31, t2/32
34 -> t0/26, t1/33
35 -> t0/32
36 -> t0/33, t2/35
37 -> t0/34, t1/36
38 -> t0/37

0.000s

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