I'm looking for the 'Leader' module from the excellent paper
Real Time is Really Simple (page 33). If the module is not available online then I think I'll be able to recreate it in toolbox, but there is one more detail I don't understand. It's the symmetry view described on page 58. What is the actual formula I need to use in TLC for Σ? Also, are there any more comprehensive materials/guidelines available regarding symmetry view settings in TLC?
The techniques described in this paper look to me as very useful for RF mesh protocol design, but I think it is crucial to fully understand the symmetry views settings in order to fully leverage model checking capabilities for such specs.
Or am I maybe overestimating the possibilities offered by these techniques and should instead look at something different?
Help is greatly appreciated.