When animated, the following specification, only offers one choice for communication. As written, it will offer onlya.1. If (B [] A) is changed to (A [] B) the only choice will be a.2.
channels
a : int
process Test =
begin
actions
A = a!1 -> Skip
B = a!2 -> Skip
C = a?x -> Skip
@ (B [] A) [|{a}|] C
end
When animated, the following specification, only offers one choice for communication. As written, it will offer only
a.1
. If(B [] A)
is changed to(A [] B)
the only choice will bea.2
.