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

*From*: Hillel Wayne <hwa...@xxxxxxxxx>*Date*: Sun, 15 Apr 2018 15:05:35 -0700 (PDT)

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

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

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

**Follow-Ups**:**Re: Best way to test a library?***From:*Leslie Lamport

- Prev by Date:
**Re: Multi-threaded TLC Simulation Mode** - Next by Date:
**Re: Best way to test a library?** - Previous by thread:
**Re: Is tla+.jj up to date on github?** - Next by thread:
**Re: Best way to test a library?** - Index(es):