Best way to test a library?

[Hillel Wayne <hwa...@xxxxxxxxx>]

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