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

mode -R

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

parsed net icq

5 places, 4 transitions, 12 arcs

net icq
tr {Icq.lock(S1)} {S1.unlocked} {icq.no_critiacal_section}  -> {icq.critical_section_1} 
tr {Icq.unlock(S1)} {icq.critical_section_1}  -> {S1.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} 
pl {S1.unlocked} (1)
pl {cpu1.no_critical_section} (1)
pl {icq.no_critiacal_section} (1)

0.000s

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

bounded

3 marking(s), 4 transition(s)

MARKINGS:

0 : {S1.unlocked} {cpu1.no_critical_section} {icq.no_critiacal_section}
1 : {cpu1.no_critical_section} {icq.critical_section_1}
2 : {cpu1.critical_section} {icq.no_critiacal_section}

REACHABILITY GRAPH:

0 -> {Icq.lock(S1)}/1, {cpu1.lock(S1)}/2
1 -> {Icq.unlock(S1)}/0
2 -> {cpu1.unlock(S1)}/0

0.000s

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

live
reversible

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

STRONG CONNECTED COMPONENTS:

0 : 2 1 0

SCC GRAPH:

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

0.000s

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