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

[Stephan Merz <stepha...@xxxxxxxxx>]

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.