templatessynchronouschanneluppaal

Channel Declaration in UPPAAL


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 :)


Solution

  • 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.