Re: [tlaplus] Using TLA VARIABLES in PlusCal algorithm

It seems to me that the pcal translator runs in a separate context entirely from the rest of the specification.

The `variables` statement inside of the algorithm will introduce a VARIABLES declaration in the translation.

I find it extremely helpful to study example pluscal algorithms by opening the smallest possible algorithm first, then gradually adding things as they become necessary. This has helped me learn what parts of the translation are produced by what parts of the pluscal, and where I can step outside of the algorithm, and where I must stay inside, when it comes to operators and variables.

(*-- algorithm base

begin skip;

end algorithm; *)

On Mon, Apr 6, 2020 at 11:24 AM James C <coulter.bits@xxxxxxxxx> wrote:

I have a "tester" module that imports another "spec" module. The imported "core" module has variables that I need to substitute. Then I also need to use these variables in a PlusCal algorithm in the "tester" spec, but I cannot figure out how do so. I've searched documentation, but found nothing relevant.

---- Module Tester ---- EXTENDS Whatever CONSTANTS Things VARIABLES A, B INSTANCE Core WITH VarA <- A, VarB <- B (*--algorithm maketest \* Reference to A or B in here result in a PCal Translator Error: \* "Assignment to undeclared variable <variablename>" end algorithm; *) \* BEGIN TRANSLATION ====

Thanks,
James

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2523b313-25da-417d-90b8-6dbac319798d%40googlegroups.com.