Thanks Stephan
Finally able to define the fairness properties I wanted - and have learnt a lot in the process. I can see that the fine control over fairness that TLA+ provides is going to take some time to assimilate.
Just one small question remains.
In the process algebra world we define processes, and these include both their safety and liveness properties. Then small process ar combined to build larger processes. The safety and liveness properties of the larger process are result of the properties of the components from which it is build.
Am I correct in saying:
in PlusCal processes can be define and then placed in submodules. But when the submodules get imported into a main module the liveness (fairness) property does not get imported along with it. So in PlusCal you first build a module from component process (sub modules) having done this then the liveness properties can be defined. ?
It may be that there is little practical need for this kind of modularisation. Nonetheless it has come as a surprise to me as this is central to how process algebras are used.
may thanks david