Starting :init: with pid 0 spin: couldn't find claim (ignored) Starting memory_manager with pid 2 2: proc 0 (:init:) line 113 "task5_modified.pml" (state 1) [(run memory_manager())] Starting pcbit_receive with pid 3 3: proc 0 (:init:) line 114 "task5_modified.pml" (state 2) [(run pcbit_receive())] Starting pcbit_receive with pid 4 4: proc 0 (:init:) line 115 "task5_modified.pml" (state 3) [(run pcbit_receive())] 6: proc 3 (pcbit_receive) line 67 "task5_modified.pml" (state 1) [(1)] 8: proc 3 (pcbit_receive) line 40 "task5_modified.pml" (state 23) [flag[(_pid-2)] = 1] 10: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 24) [turn = (_pid-2)] <<<<>>>> 12: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 25) [(((flag[(3-_pid)]==0)||(turn==(3-_pid))))] 14: proc 3 (pcbit_receive) line 100 "task5_modified.pml" (state 27) [(1)] 16: proc 3 (pcbit_receive) line 47 "task5_modified.pml" (state 31) [flag[(_pid-2)] = 0] 18: proc 3 (pcbit_receive) line 106 "task5_modified.pml" (state 33) [goto start] 20: proc 3 (pcbit_receive) line 67 "task5_modified.pml" (state 1) [(1)] 22: proc 3 (pcbit_receive) line 40 "task5_modified.pml" (state 23) [flag[(_pid-2)] = 1] 24: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 24) [turn = (_pid-2)] spin: trail ends after 24 steps #processes: 4 turn = 1 flag[0] = 0 flag[1] = 1 24: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 25) 24: proc 2 (pcbit_receive) line 66 "task5_modified.pml" (state 21) 24: proc 1 (memory_manager) line 53 "task5_modified.pml" (state 9) 24: proc 0 (:init:) line 117 "task5_modified.pml" (state 5) 4 processes created