[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 15 Apr 2018 15:14:17 -0700 (PDT)*References*: <50f37aa2-b032-430b-82d2-61ddac8c8833@googlegroups.com>

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

**References**:**Best way to test a library?***From:*Hillel Wayne

- Prev by Date:
**Best way to test a library?** - Next by Date:
**How to define Hexa decimal sets/Vectors in TLA+** - Previous by thread:
**Best way to test a library?** - Next by thread:
**How to define Hexa decimal sets/Vectors in TLA+** - Index(es):