The following model cannot execute since it dies on a wrong state type:
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 able to find the state but thinks that it is of type set of nat and thus dies internally.
The following model cannot execute since it dies on a wrong state type:
the interpreter is able to find the state but thinks that it is of type
set of natand thus dies internally.