Compiling send/receive expressions can fail because of confused variable names
As mentioned here, compiling send (and also under specific circumstances receive) expressions can sometimes fail.
Send expressions first compile both the channel expression and the value to send, and in fact they may be compiled an arbitrary amount of time before the actual send expression is compiled due to switch-case
prepared compilation.
This may then cause one sub-expression to use a local variable name (like $0
), and the next sub-expression to open up a new frame, where the local variable now exists as a bound actual variable with a different name. The resulting CCS term is invalid.
An example program is this, which creates the following CCS code:
MainAgent[a] := channel_create?$0.(when (true) (MainAgent_1[a, $0, 1]) + when (!true) (MainAgent_1[a, $0, 1]))
MainAgent_1[a, $c, t0] := when ($0>=0) (*see the use of $0) *) (put($0)!(t0).(MainAgent_2[a, $c, t0])) + when ($0<0) (receive($0)!(t0).(MainAgent_2[a, $c, t0]))
MainAgent_2[a, $c, t0] := MainAgent_3[a, $c]
MainAgent_3[a, $c] := 0
(MainAgent[1] | Channel_cons[-1]) \ {*, println, exception}
This program also suffers from the same problem. Note however that the bug is not immediately obvious because of pseuco-ccs-interpreter#2