Using TLA VARIABLES in PlusCal algorithm

[James C]

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

[Carl Thuringer]

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; *)

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

--

Cheers,

Carl Thuringer

[Hillel Wayne]

You can move the INSTANCE to a define block:

variables
  A = 1;
  VarB = 2;

define
  Foo == INSTANCE Core WITH VarA <- A
end define;

I defined VarB implicitly due to what might be a bug in the PlusCal translator, where it does not recognize INSTANCE Core WITH VarA <- A, VarB <- B as valid. I think it's the comma being a problem.

[James C]

Hi Carl and Hillel,

Indeed implicit substitution combined with the use of define works wonderfully.  Thanks for the help!

---- Module Tester ----
EXTENDS Whatever
CONSTANTS Things

(*--algorithm maketest

variables

  A = {}, B = {}; \* A and B implicitly substitute same-named variables from Core module.

define

  TestCore == INSTANCE Core   \* Instantiate Core within PlusCal context.

end define;

\* A and B can now be used in rest of PlusCal algorithm.

\* Other operators from Core can be used with TestCore!OperatorName .

end algorithm; *)
\* BEGIN

TRANSLATION
\* ...
====