The interpreter is unable to handle the following specification:
channels
a:nat
c
process A_bug =
begin
state
numbersToSend:set of nat := {1,2}
actions
loop = (sendNumber [] ([card numbersToSend <1]&Skip))
sendNumber = ([]i in set numbersToSend/*here is the problem*/ @ a.i->(numbersToSend := numbersToSend\{i});loop)
@ loop
end
The interpreter is unable to handle the following specification: