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

Hi David,

I am not familiar enough with how systems are specified in process algebra to make an informed comparison. Also, I have never really attempted to spread PlusCal processes over different modules, and I don't think that PlusCal was designed with this kind of modularity in mind. When you do that, the PlusCal translator will produce a TLA+ specification corresponding to each of the parts, and you could in principle take their conjunction to be the specification of the overall system. In fact, the slogan "composition is conjunction" is quite prominent in the TLA(+) literature, and this resembles the process algebra view where you have explicit composition operators for building an overall system model out of individual process specifications.

In practice, we want to use TLC to verify our specification, and it expects specifications to be written in the standard form

Init /\ [][Next]_vars /\ L

Therefore, you will want to assemble the overall initial condition and the overall next-state relation as the conjunction, respectively disjunction, of the individual formulas. Similarly, you will assemble the overall fairness conditions to build the one for the complete specification. In that sense, neither the safety nor the liveness part of the specification "get imported" as a whole from the individual modules, but you do get the individual pieces for assembling the specification.

Does this make sense?

Stephan

On 28 Feb 2019, at 01:51, david streader <davidistreader@xxxxxxxxx> wrote:

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.

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