Put anything used only to test a module M in a separate module that EXTENDS M.
Leslie
On Sunday, April 15, 2018 at 3:05:35 PM UTC-7, Hillel Wayne wrote:
I'm writing a Graphs library and want to include a sanity-checking operator. It consists of a list of validations that I defined everything correctly. If one of those validations fail, it raises an assertion error with a counterexample, and otherwise does nothing. Here's an example of what it will look like:
LOCAL SanityCheck ==
LET
graphs == Graphs({1, 2, 3})
AcyclicUndirected ==
{g \in graphs: (\E p \in Pairs(g.node): g.edge[p]) /\ Acyclic(g) /\ Undirected(g)}
IN
CASE AcyclicUndirected /= {} -> Assert(FALSE,
"All nontrivial undirected graphs should be cyclic, counterexample: "
\o ToString(CHOOSE g \in AcyclicUndirected: TRUE))
[] OTHER -> TRUE
(I wrap it in a CASE statement to avoid TLC evaluating CHOOSE if the condition passes... which would then raise an error!)
This works, with one problem: I can't evaluate SanityCheck in the Toolbox, as "Evaluate Constant _expression_" can't run local operators. I could fix this by removing the LOCAL, but then extending the library would make SanityCheck an operator in my spec. Is there a way to get both evaluation and encapsulation here? Thanks!
Hillel