---- 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
\* ...
====