process Trans [LDreq, LDcon, LDind, LDres, TDreq] (n, id: Nat, v: Version)
              : noexit :=
   hide TX0 in
      (
      TransReq [LDreq, LDcon, TDreq, TX0] (n, id)
      |[TX0]|
      TransRes [LDind, LDres, TX0] (id, v)
      )
endproc

(*---------------------------------------------------------------------------*)

process TransReq [LDreq, LDcon, TDreq, TX0] (n, id: Nat) : noexit :=
   TDreq !id ?dest: Nat ?h: HEADER ?d: DATA [dest le n];
   (
   TX0;
   exit (dest, h, d)
   []
   exit (dest, h, d)
   ) >> accept dest: Nat, h: HEADER, d: DATA in
   (
   LDreq !id !dest !h !d;
      (
      [dest eq n] ->
         LDcon !id !broadsent;
         TransReq [LDreq, LDcon, TDreq, TX0] (n, id)
      []
      [dest ne n] ->
         (
         choice a: ACK []
            LDcon !id !ackrec (a);
            TransReq [LDreq, LDcon, TDreq, TX0] (n, id)
         )
      []
         LDcon !id !ackmiss;
         TransReq [LDreq, LDcon, TDreq, TX0] (n, id)
      )
   )
endproc

(*---------------------------------------------------------------------------*)

process TransRes [LDind, LDres, TX0] (id: Nat, v: Version) : noexit :=
   LDind !id ?l: LIN_DIND;
   (
   [is_broadrec (l)] ->
      (
      [v = ko] ->
         (* original (incorrect) specification *)
         LDres !id !a1 !no_op;
         TransRes [LDind, LDres, TX0] (id, v)
      []
      [v = ok] ->
         (* correct specification *)
         TransRes [LDind, LDres, TX0] (id, v)
      )
   []
   [not (is_broadrec (l))] ->
      (
      choice a: ACK []
         (
         (* concatenated response = lock transaction *)
         TX0;
         LDres !id !a !hold;
         TransRes [LDind, LDres, TX0] (id, v)
         []
         (* split response *)
         LDres !id !a !release;
         TransRes [LDind, LDres, TX0] (id, v)
         )
      )
   )
endproc