Composing modules written in PlusCal

[Tristan Slominski <tristan....@xxxxxxxxx>]

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