[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs

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 

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.