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

Re: [tlaplus] Specifying a data structure and testing the specification

A quick update after I read section 14.5. I was able to use "TLC as a TLA+ Calculator" to write a "unit test" for my specification. Pretty cool! Thanks so much Stephen. Of course, if there is a better (or more idiomatic) way of doing this, please do let me know.


On Sunday, October 2, 2022 at 4:19:40 PM UTC-4 Aman Shaikh wrote:
Hi Stephen

I'll check section 14.5 of the book.

Thanks for the explanation of the first predicate of the Graphs module. In plain English, this seems to mean "G is exactly what we expect it to be".


On Sun, Oct 2, 2022 at 8:44 AM Stephan Merz <stepha...@xxxxxxxxx> wrote:

> On 2 Oct 2022, at 01:21, Aman Shaikh <amansh...@xxxxxxxxx> wrote:
> 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?

yes, model checking is a great way of validating a specification. Chapter 14.5 of Specifying Systems has some great tips on this subject.

> 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

The latter is less precise. For one, the former says that the record has exactly these two fields. Also, since TLA+ is untyped and handles "silly" expressions by underspecification, we don't know what, say, DOMAIN 42 is, so there is no way of knowing if "node" \in DOMAIN 42 is true or false – although TLC will raise an exception if you try.

But it all depends on how you choose to set up your spec and what you want to express. For example, assume that module Graph had a constant parameter Node and contained the definition

Edge == Node \X Node

then it would be sensible to write

G \in [node : Node, edge : SUBSET Edge].


You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/GrUnNYtOlEo/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BD98E7E7-33F5-4205-A128-2EFABDAC1F04%40gmail.com.

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/ab21b664-6ab3-4a5a-87fb-adbce1f84bc6n%40googlegroups.com.