[tlaplus] Specifying a data structure and testing the specification

[Aman Shaikh <amanshaikh75@xxxxxxxxx>]

Hi everyone

I'm writing a specification for a data structure (defined as a "record type") and some operations on it. Something along the lines of the Graphs specification in the "Specifying Systems" book.

One question I have is: how do I "test" the specification? I guess I can write an MC*.tla and MC*.cfg file and use TLC for this purpose, but what's the Idiomatic way of doing these things?

I also have a specific question about the Graphs specification. It's about the first predicate in the operator 'IsDirectedGraph' which goes like this:

/\ G = [node |-> G.node, edge |-> G.edge]

If one wants to check that G is a record with 'node' and 'edge' why not write this as:

/\ "node" \in DOMAIN G

/\ "edge" \in DOMAIN G

thx

aman

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/40d7af77-0fb9-4930-a908-ed150992fcacn%40googlegroups.com.