Tina version 3.8.5 -- 12/01/24 -- LAAS/CNRS mode -R INPUT NET ------------------------------------------------------- parsed net icq 16 places, 16 transitions, 44 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.lock(S3)} {S3.unlocked} {icq.critical_section_2} -> {icq.critical_section_3} tr {Icq.unlock(S1,S2,S3)} {icq.critical_section_3} -> {S1.locked} {S2.locked} {S3.locked} {icq.no_critiacal_section} tr {S1.lock()} {S1.unlocked} -> {S1.locked} tr {S1.unlock()} {S1.locked} -> {S1.unlocked} tr {S2.lock()} {S2.unlocked} -> {S2.locked} tr {S2.unlock()} {S2.locked} -> {S2.unlocked} tr {S3.lock()} {S3.unlocked} -> {S3.locked} tr {S3.unlock()} {S3.locked} -> {S3.unlocked} tr {cpu1.lock(S1)} {S1.unlocked} {cpu1.no_critical_section} -> {cpu1.critical_section} tr {cpu1.unlock(S1)} {cpu1.critical_section} -> {S1.locked} {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.locked} {cpu2.no_critical_section} tr {cpu3.lock(S3)} {S3.unlocked} {cpu3.no_critical_section} -> {cpu3.critical_section} tr {cpu3.unlock(S3)} {cpu3.critical_section} -> {S3.locked} {cpu3.no_critical_section} pl {S1.unlocked} (1) pl {S2.unlocked} (1) pl {S3.unlocked} (1) pl {cpu1.no_critical_section} (1) pl {cpu2.no_critical_section} (1) pl {cpu3.no_critical_section} (1) pl {icq.no_critiacal_section} (1) 0.001s REACHABILITY ANALYSIS ------------------------------------------- bounded 40 marking(s), 150 transition(s) MARKINGS: 0 : {S1.unlocked} {S2.unlocked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 1 : {S2.unlocked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.critical_section_1} 2 : {S1.locked} {S2.unlocked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 3 : {S1.unlocked} {S2.locked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 4 : {S1.unlocked} {S2.unlocked} {S3.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 5 : {S2.unlocked} {S3.unlocked} {cpu1.critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 6 : {S1.unlocked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 7 : {S1.unlocked} {S2.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 8 : {S3.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.critical_section_2} 9 : {S2.locked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.critical_section_1} 10 : {S2.unlocked} {S3.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.critical_section_1} 11 : {S3.unlocked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.critical_section_1} 12 : {S2.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.critical_section_1} 13 : {S1.locked} {S2.locked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 14 : {S1.locked} {S2.unlocked} {S3.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 15 : {S1.locked} {S3.unlocked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 16 : {S1.locked} {S2.unlocked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 17 : {S1.unlocked} {S2.locked} {S3.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 18 : {S2.locked} {S3.unlocked} {cpu1.critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 19 : {S1.unlocked} {S2.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 20 : {S2.unlocked} {S3.locked} {cpu1.critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 21 : {S1.unlocked} {S3.locked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 22 : {S3.unlocked} {cpu1.critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 23 : {S2.unlocked} {cpu1.critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 24 : {S1.unlocked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 25 : {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.critical_section_3} 26 : {S3.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.critical_section_2} 27 : {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.critical_section_2} 28 : {S2.locked} {S3.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.critical_section_1} 29 : {S2.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.critical_section_1} 30 : {S3.locked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.critical_section_1} 31 : {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.critical_section} {icq.critical_section_1} 32 : {S1.locked} {S2.locked} {S3.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 33 : {S1.locked} {S2.locked} {cpu1.no_critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 34 : {S1.locked} {S3.locked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 35 : {S1.locked} {cpu1.no_critical_section} {cpu2.critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 36 : {S2.locked} {S3.locked} {cpu1.critical_section} {cpu2.no_critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 37 : {S2.locked} {cpu1.critical_section} {cpu2.no_critical_section} {cpu3.critical_section} {icq.no_critiacal_section} 38 : {S3.locked} {cpu1.critical_section} {cpu2.critical_section} {cpu3.no_critical_section} {icq.no_critiacal_section} 39 : {cpu1.critical_section} {cpu2.critical_section} {cpu3.critical_section} {icq.no_critiacal_section} REACHABILITY GRAPH: 0 -> {Icq.lock(S1)}/1, {S1.lock()}/2, {S2.lock()}/3, {S3.lock()}/4, {cpu1.lock(S1)}/5, {cpu2.lock(S2)}/6, {cpu3.lock(S3)}/7 1 -> {Icq.lock(S2)}/8, {S2.lock()}/9, {S3.lock()}/10, {cpu2.lock(S2)}/11, {cpu3.lock(S3)}/12 2 -> {S1.unlock()}/0, {S2.lock()}/13, {S3.lock()}/14, {cpu2.lock(S2)}/15, {cpu3.lock(S3)}/16 3 -> {Icq.lock(S1)}/9, {S1.lock()}/13, {S2.unlock()}/0, {S3.lock()}/17, {cpu1.lock(S1)}/18, {cpu3.lock(S3)}/19 4 -> {Icq.lock(S1)}/10, {S1.lock()}/14, {S2.lock()}/17, {S3.unlock()}/0, {cpu1.lock(S1)}/20, {cpu2.lock(S2)}/21 5 -> {S2.lock()}/18, {S3.lock()}/20, {cpu1.unlock(S1)}/2, {cpu2.lock(S2)}/22, {cpu3.lock(S3)}/23 6 -> {Icq.lock(S1)}/11, {S1.lock()}/15, {S3.lock()}/21, {cpu1.lock(S1)}/22, {cpu2.unlock(S2)}/3, {cpu3.lock(S3)}/24 7 -> {Icq.lock(S1)}/12, {S1.lock()}/16, {S2.lock()}/19, {cpu1.lock(S1)}/23, {cpu2.lock(S2)}/24, {cpu3.unlock(S3)}/4 8 -> {Icq.lock(S3)}/25, {S3.lock()}/26, {cpu3.lock(S3)}/27 9 -> {S2.unlock()}/1, {S3.lock()}/28, {cpu3.lock(S3)}/29 10 -> {Icq.lock(S2)}/26, {S2.lock()}/28, {S3.unlock()}/1, {cpu2.lock(S2)}/30 11 -> {S3.lock()}/30, {cpu2.unlock(S2)}/9, {cpu3.lock(S3)}/31 12 -> {Icq.lock(S2)}/27, {S2.lock()}/29, {cpu2.lock(S2)}/31, {cpu3.unlock(S3)}/10 13 -> {S1.unlock()}/3, {S2.unlock()}/2, {S3.lock()}/32, {cpu3.lock(S3)}/33 14 -> {S1.unlock()}/4, {S2.lock()}/32, {S3.unlock()}/2, {cpu2.lock(S2)}/34 15 -> {S1.unlock()}/6, {S3.lock()}/34, {cpu2.unlock(S2)}/13, {cpu3.lock(S3)}/35 16 -> {S1.unlock()}/7, {S2.lock()}/33, {cpu2.lock(S2)}/35, {cpu3.unlock(S3)}/14 17 -> {Icq.lock(S1)}/28, {S1.lock()}/32, {S2.unlock()}/4, {S3.unlock()}/3, {cpu1.lock(S1)}/36 18 -> {S2.unlock()}/5, {S3.lock()}/36, {cpu1.unlock(S1)}/13, {cpu3.lock(S3)}/37 19 -> {Icq.lock(S1)}/29, {S1.lock()}/33, {S2.unlock()}/7, {cpu1.lock(S1)}/37, {cpu3.unlock(S3)}/17 20 -> {S2.lock()}/36, {S3.unlock()}/5, {cpu1.unlock(S1)}/14, {cpu2.lock(S2)}/38 21 -> {Icq.lock(S1)}/30, {S1.lock()}/34, {S3.unlock()}/6, {cpu1.lock(S1)}/38, {cpu2.unlock(S2)}/17 22 -> {S3.lock()}/38, {cpu1.unlock(S1)}/15, {cpu2.unlock(S2)}/18, {cpu3.lock(S3)}/39 23 -> {S2.lock()}/37, {cpu1.unlock(S1)}/16, {cpu2.lock(S2)}/39, {cpu3.unlock(S3)}/20 24 -> {Icq.lock(S1)}/31, {S1.lock()}/35, {cpu1.lock(S1)}/39, {cpu2.unlock(S2)}/19, {cpu3.unlock(S3)}/21 25 -> {Icq.unlock(S1,S2,S3)}/32 26 -> {S3.unlock()}/8 27 -> {cpu3.unlock(S3)}/26 28 -> {S2.unlock()}/10, {S3.unlock()}/9 29 -> {S2.unlock()}/12, {cpu3.unlock(S3)}/28 30 -> {S3.unlock()}/11, {cpu2.unlock(S2)}/28 31 -> {cpu2.unlock(S2)}/29, {cpu3.unlock(S3)}/30 32 -> {S1.unlock()}/17, {S2.unlock()}/14, {S3.unlock()}/13 33 -> {S1.unlock()}/19, {S2.unlock()}/16, {cpu3.unlock(S3)}/32 34 -> {S1.unlock()}/21, {S3.unlock()}/15, {cpu2.unlock(S2)}/32 35 -> {S1.unlock()}/24, {cpu2.unlock(S2)}/33, {cpu3.unlock(S3)}/34 36 -> {S2.unlock()}/20, {S3.unlock()}/18, {cpu1.unlock(S1)}/32 37 -> {S2.unlock()}/23, {cpu1.unlock(S1)}/33, {cpu3.unlock(S3)}/36 38 -> {S3.unlock()}/22, {cpu1.unlock(S1)}/34, {cpu2.unlock(S2)}/36 39 -> {cpu1.unlock(S1)}/35, {cpu2.unlock(S2)}/37, {cpu3.unlock(S3)}/38 0.000s LIVENESS ANALYSIS ----------------------------------------------- live reversible 0 dead marking(s), 40 live marking(s) 0 dead transition(s), 16 live transition(s) STRONG CONNECTED COMPONENTS: 0 : 39 38 37 36 35 34 33 32 31 30 29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 9 8 7 6 5 4 3 2 1 0 SCC GRAPH: 0 -> {cpu1.unlock(S1)}/0, {cpu2.unlock(S2)}/0, {cpu3.unlock(S3)}/0, {S3.unlock()}/0, {S2.unlock()}/0, {S1.unlock()}/0, {Icq.unlock(S1,S2,S3)}/0, {Icq.lock(S1)}/0, {S1.lock()}/0, {cpu1.lock(S1)}/0, {S2.lock()}/0, {cpu2.lock(S2)}/0, {S3.lock()}/0, {cpu3.lock(S3)}/0, {Icq.lock(S2)}/0, {Icq.lock(S3)}/0 0.000s ANALYSIS COMPLETED ----------------------------------------------