Skip to content

Instantly share code, notes, and snippets.

@PatrickLerner
Created November 22, 2013 12:02
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save PatrickLerner/7598865 to your computer and use it in GitHub Desktop.
Save PatrickLerner/7598865 to your computer and use it in GitHub Desktop.
0: proc - (:root:) creates proc 0 (barber)
0: proc - (:root:) creates proc 2 (customer)
1: proc 1 (customer) SleepingBarberProblem.pml:47 (state 14) [haircut[me] = 0]
2: proc 2 (customer) SleepingBarberProblem.pml:47 (state 14) [haircut[me] = 0]
3: proc 1 (customer) SleepingBarberProblem.pml:49 (state 11) [(sleeping)]
4: proc 1 (customer) SleepingBarberProblem.pml:51 (state 5) [sleeping = 0]
5: proc 1 (customer) SleepingBarberProblem.pml:55 (state 4) [chair = me]
6: proc 0 (barber) SleepingBarberProblem.pml:19 (state 1) [((sleeping==0))]
7: proc 1 (customer) SleepingBarberProblem.pml:66 (state 12) [.(goto)]
8: proc 2 (customer) SleepingBarberProblem.pml:49 (state 11) [(!(sleeping))]
9: proc 0 (barber) SleepingBarberProblem.pml:21 (state 2) [customer = chair]
10: proc 0 (barber) SleepingBarberProblem.pml:23 (state 3) [haircut[customer] = 1]
11: proc 1 (customer) SleepingBarberProblem.pml:66 (state 13) [(haircut[me])]
12: proc 1 (customer) SleepingBarberProblem.pml:68 (state 15) [.(goto)]
13: proc 1 (customer) SleepingBarberProblem.pml:47 (state 14) [haircut[me] = 0]
14: proc 1 (customer) SleepingBarberProblem.pml:49 (state 11) [(!(sleeping))]
15: proc 0 (barber) SleepingBarberProblem.pml:41 (state 14) [.(goto)]
16: proc 0 (barber) SleepingBarberProblem.pml:25 (state 13) [((front==end))]
17: proc 2 (customer) SleepingBarberProblem.pml:60 (state 10) [queue[end] = me]
18: proc 2 (customer) SleepingBarberProblem.pml:62 (state 8) [end = ((end+1)%3)]
19: proc 2 (customer) SleepingBarberProblem.pml:63 (state 9) [sleeping = 0]
20: proc 2 (customer) SleepingBarberProblem.pml:66 (state 12) [.(goto)]
21: proc 1 (customer) SleepingBarberProblem.pml:60 (state 10) [queue[end] = me]
22: proc 1 (customer) SleepingBarberProblem.pml:62 (state 8) [end = ((end+1)%3)]
23: proc 1 (customer) SleepingBarberProblem.pml:63 (state 9) [sleeping = 0]
24: proc 0 (barber) SleepingBarberProblem.pml:37 (state 10) [chair = 255]
25: proc 0 (barber) SleepingBarberProblem.pml:38 (state 11) [sleeping = 1]
26: proc 0 (barber) SleepingBarberProblem.pml:39 (state 12) [goto sleep]
27: proc 1 (customer) SleepingBarberProblem.pml:66 (state 12) [.(goto)]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment