Interpreter: 'DEADLOCK' message when there is no deadlock in the process

[lucasalbertins]

The example below describes a process POD with two actions A and B that synchronise on channel ent. The alphabets of synchronisation restrict both actions to synchronise specifically on the event ent!([mk_token("D")])!([mk_token("T")]). However, every time I run the Interpreter it displays the message DEADLOCK, but there is no deadlock in this example.

types 
    ID = seq of token
channels
    ent: ID*ID

process POD = begin 
actions
    A = ent?o!([mk_token("T")]) -> A
    B = (ent!([mk_token("D")])!([mk_token("T")]) -> B)
    @ 
    (B [{|ent.([mk_token("D")]).x | x in set {([mk_token("T")])} |} || {|ent.x.([mk_token("T")])| x in set {([mk_token("D")])} |}] A)

end  

[joey-coleman]

(semi-)simplified example:

channels
  ent: nat * nat

chansets
  csA = --{| ent.x.(1) | x in set {2} |}
        {| ent.(2).(1) |}
  csB = --{| ent.(2).x | x in set {1} |}
        {| ent.(2).(1) |}

process POD = begin 
  actions
    A = ent?o!1 -> A
    B = ent!2!1 -> B
@ 
  (ent?o!1 -> A [ csA || csB ] ent!2!1 -> B)
-- this would be fine:
--  (ent?o!1 -> A [| csA |] ent!2!1 -> B)
end