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 2 (pcbit_receive) line 70 "task5_modified.pml" (state 2) [(1)] 26: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 24) [turn = (_pid-2)] 28: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 25) [(((flag[(3-_pid)]==0)||(turn==(3-_pid))))] 30: proc 3 (pcbit_receive) line 100 "task5_modified.pml" (state 27) [(1)] 32: proc 3 (pcbit_receive) line 47 "task5_modified.pml" (state 31) [flag[(_pid-2)] = 0] 34: proc 3 (pcbit_receive) line 106 "task5_modified.pml" (state 33) [goto start] 36: proc 3 (pcbit_receive) line 67 "task5_modified.pml" (state 1) [(1)] 38: proc 3 (pcbit_receive) line 40 "task5_modified.pml" (state 23) [flag[(_pid-2)] = 1] 40: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 24) [turn = (_pid-2)] 42: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 25) [(((flag[(3-_pid)]==0)||(turn==(3-_pid))))] 44: proc 3 (pcbit_receive) line 100 "task5_modified.pml" (state 27) [(1)] 46: proc 3 (pcbit_receive) line 47 "task5_modified.pml" (state 31) [flag[(_pid-2)] = 0] 48: proc 3 (pcbit_receive) line 106 "task5_modified.pml" (state 33) [goto start] 50: proc 3 (pcbit_receive) line 67 "task5_modified.pml" (state 1) [(1)] 52: proc 2 (pcbit_receive) line 73 "task5_modified.pml" (state 3) [channel!_pid,FROM_P,GIMME] 53: proc 1 (memory_manager) line 54 "task5_modified.pml" (state 1) [channel?who,FROM_P,GIMME] 55: proc 3 (pcbit_receive) line 40 "task5_modified.pml" (state 23) [flag[(_pid-2)] = 1] 57: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 24) [turn = (_pid-2)] 59: proc 3 (pcbit_receive) line 41 "task5_modified.pml" (state 25) [(((flag[(3-_pid)]==0)||(turn==(3-_pid))))] 61: proc 3 (pcbit_receive) line 100 "task5_modified.pml" (state 27) [(1)] 63: proc 3 (pcbit_receive) line 47 "task5_modified.pml" (state 31) [flag[(_pid-2)] = 0] 65: proc 3 (pcbit_receive) line 106 "task5_modified.pml" (state 33) [goto start] 67: proc 3 (pcbit_receive) line 70 "task5_modified.pml" (state 2) [(1)] 69: proc 1 (memory_manager) line 54 "task5_modified.pml" (state 2) [channel!who,FROM_M,DONE] 70: proc 2 (pcbit_receive) line 74 "task5_modified.pml" (state 4) [channel?_pid,FROM_M,result] 72: proc 3 (pcbit_receive) line 73 "task5_modified.pml" (state 3) [channel!_pid,FROM_P,GIMME] 73: proc 1 (memory_manager) line 54 "task5_modified.pml" (state 1) [channel?who,FROM_P,GIMME] 75: proc 2 (pcbit_receive) line 78 "task5_modified.pml" (state 7) [else] 77: proc 2 (pcbit_receive) line 82 "task5_modified.pml" (state 11) [(1)] 79: proc 2 (pcbit_receive) line 40 "task5_modified.pml" (state 23) [flag[(_pid-2)] = 1] 81: proc 2 (pcbit_receive) line 41 "task5_modified.pml" (state 24) [turn = (_pid-2)] 83: proc 2 (pcbit_receive) line 41 "task5_modified.pml" (state 25) [(((flag[(3-_pid)]==0)||(turn==(3-_pid))))] 85: proc 2 (pcbit_receive) line 100 "task5_modified.pml" (state 27) [(1)] 87: proc 2 (pcbit_receive) line 47 "task5_modified.pml" (state 31) [flag[(_pid-2)] = 0] 89: proc 2 (pcbit_receive) line 106 "task5_modified.pml" (state 33) [goto start] <<<<>>>> 91: proc 2 (pcbit_receive) line 67 "task5_modified.pml" (state 1) [(1)] 93: proc 2 (pcbit_receive) line 40 "task5_modified.pml" (state 23) [flag[(_pid-2)] = 1] 95: proc 2 (pcbit_receive) line 41 "task5_modified.pml" (state 24) [turn = (_pid-2)] 97: proc 2 (pcbit_receive) line 41 "task5_modified.pml" (state 25) [(((flag[(3-_pid)]==0)||(turn==(3-_pid))))] 99: proc 2 (pcbit_receive) line 100 "task5_modified.pml" (state 27) [(1)] 101: proc 2 (pcbit_receive) line 47 "task5_modified.pml" (state 31) [flag[(_pid-2)] = 0] 103: proc 2 (pcbit_receive) line 106 "task5_modified.pml" (state 33) [goto start] spin: trail ends after 103 steps #processes: 4 turn = 0 flag[0] = 0 flag[1] = 0 103: proc 3 (pcbit_receive) line 74 "task5_modified.pml" (state 4) 103: proc 2 (pcbit_receive) line 66 "task5_modified.pml" (state 21) 103: proc 1 (memory_manager) line 54 "task5_modified.pml" (state 2) 103: proc 0 (:init:) line 117 "task5_modified.pml" (state 5) 4 processes created