[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Using TLA VARIABLES in PlusCal algorithm
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 ----
VARIABLES A, B
INSTANCE Core WITH VarA <- A, VarB <- B
\* Reference to A or B in here result in a PCal Translator Error:
\* "Assignment to undeclared variable <variablename>"
end algorithm; *)
\* BEGIN TRANSLATION
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.