Tina version 3.8.5 -- 12/01/24 -- LAAS/CNRS

mode -R

INPUT NET ------------------------------------------------------- 

parsed net icq

9 places, 7 transitions, 22 arcs

net icq
tr {Icq.lock(S1)} {S1.unlocked} {icq.no_critiacal_section}  -> {icq.critical_section_1} 
tr {Icq.lock(S2)} {S2.unlocked} {icq.critical_section_1}  -> {icq.critical_section_2} 
tr {Icq.unlock(S1,S2)} {icq.critical_section_2}  -> {S1.unlocked} {S2.unlocked} {icq.no_critiacal_section} 
tr {cpu1.lock(S1)} {S1.unlocked} {cpu1.no_critical_section}  -> {cpu1.critical_section} 
tr {cpu1.unlock(S1)} {cpu1.critical_section}  -> {S1.unlocked} {cpu1.no_critical_section} 
tr {cpu2.lock(S2)} {S2.unlocked} {cpu2.no_critical_section}  -> {cpu2.critical_section} 
tr {cpu2.unlock(S2)} {cpu2.critical_section}  -> {S2.unlocked} {cpu2.no_critical_section} 
pl {S1.unlocked} (1)
pl {S2.unlocked} (1)
pl {cpu1.no_critical_section} (1)
pl {cpu2.no_critical_section} (1)
pl {icq.no_critiacal_section} (1)

0.001s

REACHABILITY ANALYSIS ------------------------------------------- 

bounded

7 marking(s), 14 transition(s)

MARKINGS:

0 : {S1.unlocked} {S2.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {icq.no_critiacal_section}
1 : {S2.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {icq.critical_section_1}
2 : {S2.unlocked} {cpu1.critical_section} {cpu2.no_critical_section} {icq.no_critiacal_section}
3 : {S1.unlocked} {cpu1.no_critical_section} {cpu2.critical_section} {icq.no_critiacal_section}
4 : {cpu1.no_critical_section} {cpu2.no_critical_section} {icq.critical_section_2}
5 : {cpu1.no_critical_section} {cpu2.critical_section} {icq.critical_section_1}
6 : {cpu1.critical_section} {cpu2.critical_section} {icq.no_critiacal_section}

REACHABILITY GRAPH:

0 -> {Icq.lock(S1)}/1, {cpu1.lock(S1)}/2, {cpu2.lock(S2)}/3
1 -> {Icq.lock(S2)}/4, {cpu2.lock(S2)}/5
2 -> {cpu1.unlock(S1)}/0, {cpu2.lock(S2)}/6
3 -> {Icq.lock(S1)}/5, {cpu1.lock(S1)}/6, {cpu2.unlock(S2)}/0
4 -> {Icq.unlock(S1,S2)}/0
5 -> {cpu2.unlock(S2)}/1
6 -> {cpu1.unlock(S1)}/3, {cpu2.unlock(S2)}/2

0.000s

LIVENESS ANALYSIS ----------------------------------------------- 

live
reversible

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

STRONG CONNECTED COMPONENTS:

0 : 6 5 4 3 2 1 0

SCC GRAPH:

0 -> {cpu1.unlock(S1)}/0, {cpu2.unlock(S2)}/0, {Icq.unlock(S1,S2)}/0, {Icq.lock(S1)}/0, {cpu1.lock(S1)}/0, {cpu2.lock(S2)}/0, {Icq.lock(S2)}/0

0.000s

ANALYSIS COMPLETED ----------------------------------------------