Hi,
> On 2 Oct 2022, at 01:21, Aman Shaikh <amanshaikh75@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].
Stephan
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BD98E7E7-33F5-4205-A128-2EFABDAC1F04%40gmail.com.