Computing initial states...
Finished computing initial states: 1 distinct state generated.
Error: Invariant NoDeadlock is violated.
Error: The behavior up to this point is:
State 1:
/\ buffer = <<>>
/\ waitSet = {}
State 2:
/\ buffer = <>
/\ waitSet = {}
State 3:
/\ buffer = <>
/\ waitSet = {}
State 4:
/\ buffer = <>
/\ waitSet = {p1}
State 5:
/\ buffer = <>
/\ waitSet = {p1, p2}
State 6:
/\ buffer = <>
/\ waitSet = {p1, p2, p3}
State 7:
/\ buffer = <>
/\ waitSet = {p2, p3}
State 8:
/\ buffer = <<>>
/\ waitSet = {p3}
State 9:
/\ buffer = <<>>
/\ waitSet = {p3, c1}
State 10:
/\ buffer = <<>>
/\ waitSet = {p3, c1, c2}
State 11:
/\ buffer = <>
/\ waitSet = {c1, c2}
State 12:
/\ buffer = <>
/\ waitSet = {c2}
State 13:
/\ buffer = <>
/\ waitSet = {p1, c2}
State 14:
/\ buffer = <>
/\ waitSet = {p1, p2, c2}
State 15:
/\ buffer = <>
/\ waitSet = {p1, p2, p3, c2}
State 16:
/\ buffer = <>
/\ waitSet = {p2, p3, c2}
State 17:
/\ buffer = <<>>
/\ waitSet = {p2, p3}
State 18:
/\ buffer = <<>>
/\ waitSet = {p2, p3, c1}
State 19:
/\ buffer = <<>>
/\ waitSet = {p2, p3, c1, c2}
State 20:
/\ buffer = <>
/\ waitSet = {p3, c1, c2}
State 21:
/\ buffer = <>
/\ waitSet = {c1, c2}
State 22:
/\ buffer = <>
/\ waitSet = {p1, c1, c2}
State 23:
/\ buffer = <>
/\ waitSet = {p1, p2, c1, c2}
State 24:
/\ buffer = <>
/\ waitSet = {p1, p2, p3, c1, c2}
385 states generated, 86 distinct states found, 2 states left on queue.
The depth of the complete state graph search is 24.