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

Reusing PlusCal processes in multiple models/modules



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