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.
----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.