Why isn't the UPPAAL-compiler throwing an error when I declare a channel within a template section? If I got it right, no other Template can access these Channels, thus Channel declaration only appears to make sense in the overall Declaration section. Or am I overlooking something?
Thanks!
PS I'd like to model "internal" Template communication via synchronous channels and hoped that declaring a channel within a Template might be a solution. The upper question just appears to be easier to pose and answer :)
You can have urgent broadcast chan ASAP
locally and force urgent transitions without synchronizing with anything.
As for the "internal" communication you can share specific channels by passing a channel reference as a parameter and use only channel declarations from the system declaration section.