- The spec is clear. I particularly like the pervasive use of LET ... IN ... to give useful names to intermediate values and keep the resulting expressions short. It's worth making a habit of clarity, as it really helps when applying TLA+ to more difficult problems.
- The spec is very well commented. I mention this because some people don't write comments in specs, and I've seen that cause confusion, bad assumptions, and errors. So omitting comments is a big mistake when trying to apply TLA+ to difficult problems. With tricky or complex specs, as with tricky or complex code, I've found it very helpful to follow Leslie's advice to write the comments first -- see
http://www.budiu.info/blog/lamport.html- Leslie also taught me that it's a good idea to explicitly state the purpose of a specification. For example, what aspect of the system's behavior (or perhaps its interaction with its environment) are you trying to clarify? Alternatively, what kind of design bugs are you trying to find? Doing this is very useful in my experience. I've also found that writing down the purpose before starting to write the spec really helps me to choose the level of detail/abstraction for that spec.
So, I will ask as a rhetorical question: beyond learning TLA+, what is the purpose of this spec? What are you trying to clarify or verify?
From reading the spec, I might guess that the purpose is to clarify some unusual assumptions that you want to make about part of "the environment" of the system, specifically the communication medium (network). I say that because you have a sub-action, ConsumeMsgAndBroadcastSync, that has coarse-grain concurrency: in a single atomic step it changes the inbox of every process in the system, which implies a strong assumption about the ability to send a group of messages without any concurrent interleaving (somewhat like a transaction). However, you also have an action of the environment, LoseMsg, that can non-deterministically discard an arbitrary message from any inbox at any time. Message loss is one of the standard assumptions about weaker communication mediums, but the other standard assumptions --duplicated messages and re-ordered messages-- are not modeled by this spec. So, together this is an interesting mix of strong and weak assumptions, and I'm curious as to the reason.
From reading the spec, I might also guess that the purpose is not to verify a safety or liveness property (which is fine if that's your intent). I say that because the only property in the spec is the type invariant and I doubt that it would ever be worth writing a spec to only verify a type invariant, as they are usually very shallow.
Perhaps you intend to later add a property, such as some variant of 'eventual consistency' (really a family of properties). That could well be worth verifying. However, I doubt that the spec would satisfy such a property without some changes, as the environment can lose messages but the system (at this level of abstraction) doesn't have a mechanism to re-transmit lost messages. (Also, the spec doesn't have a liveness assumption, so allows behaviors in which processes simply never consume any more messages from their inbox.)
If the above guesses are wrong, and the sole purpose of the spec was to learn TLA+ then you've certainly succeeded at learning the language, apparently quite quickly. However, I'm a little worried that you or your colleagues might feel that you've performed a ritual with no practical value. If that's the case, I'd encourage you to suspend judgement on the value until you've applied TLA+, with purpose, to a difficult problem.
I hope this helps,
Chris