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

Re: [tlaplus] Reusing PlusCal processes in multiple models/modules

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

On 2018-01-18 12:45 PM, Stephan Merz wrote:

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


On 18 Jan 2018, at 18:09, Shuhao Wu <shu...@xxxxxxxxxxxx> wrote:

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

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