Re: [tlaplus] Composing modules written in PlusCal

[Ioannis Filippidis <jfili...@xxxxxxxxx>]

Hi Tristan,

I am unfamiliar with PlusCal. From some past experience trying to combine imperative
and declarative statements for specifying systems using modular specifications,
it seems to me more practical to work directly with declarative statements, in TLA+.

If both the modules and the assumptions made during their composition (for example,
an assumption about interleaving) are in TLA+, it may be easier to reason about
how they relate to each other. An additional resource to Chapter 10 that could be
useful is the paper "Conjoining specifications" by Abadi and Lamport [1].

If the modules change the same variables, then it will probably help to refer
to Section 10.4 of the TLA+ book. A question worth considering is why do you want
to decompose the specification? Are the modules going to be reused independently
of each other? Or is the purpose to organize the specification similarly to
how the components will be implemented?

If the modules are to be reused independently, then you will probably need
to write assumptions that each one makes about the other components, and
check that it satisfies some desired properties, provided that the assumptions hold.

You will also need to check that the other components satisfy the assumptions
that the component made about them, and avoid circular dependencies among them.
This type of reasoning can quickly become more difficult than writing
a single specification for the entire system.

[1] http://lamport.azurewebsites.net/pubs/pubs.html#abadi-conjoining

Best regards,
ioannis


On 2/10/17 2:36 PM, Tristan Slominski wrote:
> Hello,
>
> My use case revolves around building systems that have high level actions like CreateTenant, StoreObject, DestroyTenant. I've been attempting to model interleaving of DestroyTenant and StoreObject to ensure that no extra objects are around after the tenant is destroyed.
>
> To do this, I have a TLA+ module that is a model for the Store. Then I create a PlusCal module for DestroyTenant and a PlusCal module for StoreObject. But it seems very difficult to compose the generated code from the two PlusCal modules together into one Spec with one Next function (especially since both can change the shared Store, or not, so UNCHANGED becomes difficult to specify).
>
> Originally, if I do all of this in one single module using multiple PlusCal fair processes (one for DestroyTenant and one for StoreObject), things are straightforward and it is easy to validate the model. The problem arises when I want to refactor the single module into multiple modules, for example a Destroy module containing the fair process that implements what happens when tenant is destroyed (includes deleting stuff from Store), and another module for StoreObject, which contains a fair process that implements what happens when tenant asks for an object to be stored (including putting stuff into Store).
>
> Is there a pattern for composing multiple modules where each is generated from its own PlusCal code? I've read this thread (https://groups.google.com/forum/#!searchin/tlaplus/module%7Csort:relevance/tlaplus/P5hIPrDgcfk/QjjRKho4BwAJ) and Chapter 10 of "Specifying Systems" book, but they both seem to assume working with TLA+ directly. Am I "doing it wrong"? Should I specify everything in TLA+ in order to achieve modularity?
>
> Cheers,
>
> Tristan
>