Reusing PlusCal processes in multiple models/modules

[Shuhao Wu]

Hello,

I have a multi-process algorithm implemented in PlusCal with processes
A, B, C and D. Together they have some Temporal formula Spec they follow
as well as some Invariant that it must satisfy.

I want to now slightly change the definition of one of these processes,
C, to perform something slightly different (let's call this ModifiedC).
As an example, the original C can be something like:

fair process (C = "C")
variables data;
{
proc_c: data := 1;
}

and I would like to have ModifiedC to be:

fair process (ModifiedC = "ModifiedC")
variables data;
{
proc_c: either {
data := 1;
} or {
data := 2;
}
}

I want to use ModifiedC instead of C in a new model that follows the
same TemporalFormula and a different Invariant. What is the preferred
way to do this without having to copy the entire module to a new tla
file? Am I even doing this correctly?

Thanks,
Shuhao

[Stephan Merz]

Hello Shuhao,

there is no support for modularity in PlusCal, the idea being that specifications in general and PlusCal algorithms in particular are short enough and rarely reused directly, making copy and paste acceptable.

Stephan

> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Hillel Wayne]

Could you put both invariants in one module, and then make two separate models to check one each? That might sidestep the problem for you.

[Shuhao Wu]

Hello Stephan,

Right now in my specification I have several failure scenarios where if
I made a step in a particular fashion, it will cause invariant
violations. I can do this at multiple locations and it would be nice to
be able to verify these invariant violations exists as a) a sanity check
and b) it can serve an illustration for others who read the spec to see
for themselves exactly how the violation takes place. Furthermore,
swapping out the processes I had talked about will allow me to specify a
system with several different implementations of something that
accomplish the same thing.

Without modularity, this is difficult to accomplish without copy or
pasting the TLA+ spec many many times. If the spec is to be changed, the
change must be mirrored everywhere. Are there some recommended ways of
solving this problem? Or is this simply something that should be
discouraged from TLA+'s perspective? An idea could be using C
pre-processors, but that seems like a massive hack.

Thanks,
Shuhao