CCSInput#computeTypes does not check the channel properly
CCSInput#computeTypes
should call channel.computeTypes
to check whether the channel is well-formed. It however does not do that in the right order, leading to this CCS expression c(a)?a.0
passing the typecheck but of course failing in the later evaluation.
More specifically, a
is already added to the environment when c(a)
is checked even though it should be the other way around.
Edited by Johannes Hostert