Re: [tlaplus] Spec Review Request

[Stephan Merz <stepha...@xxxxxxxxx>]

Hi Jamie,

I completely agree with the remarks that Chris made. The spec is written very competently, but its purpose, and in particular the properties it might enjoy, are not really obvious. One property that comes to mind is that the playlist states of the clients are always "behind" that of the server. It might be worthwhile defining this notion precisely in TLA+.

Follow a few lower-level comments:

- Perhaps you may want to beef up your TypeOK predicate a little. Since TLA+ is untyped, you are not restricted to types that you find in programming languages. For example, one could define

  ValidState(s) == s.playhead.i \in {-1} \cup (1 .. Len(s.playlist))

to express that the index of the playhead points to a valid entry in the list, unless the playhead is stopped and add the conjunct

  /\ \A n \in Node : ValidState(state[n])

to the definition of TypeOK.

- Playing with ordering assumptions is quite easy in TLA+, e.g. replace "Seq(Message)" by "SUBSET Message" in TypeOK and accordingly change the send and receive actions to operate on sets rather than sequences. But indeed, switching to sets could cause the playlists to evolve "backwards in time", contrary to communication that preserves ordering.

- Action SendSeek, definition of newPlayhead: if you prefer, you can replace "playhead.t" by "@" (but I guess you know that).

- Action RecvSkip, definition of newPlayhead: I believe you meant to write "<=" rather than "<" – remember that in TLA+, a sequence s is indexed from 1 to Len(s).

Regards,
Stephan


> On 14 Feb 2018, at 00:13, Jamie White <ja...@xxxxxxxxxxxxx> wrote:
> 
> Hi Chris
> 
> Thank you so much for your message. It’s a treasure trove of knowledge and valuable advice.
> 
> Your assumptions are pretty much spot on, but allow me to clarify the intent a little further:
> 
> The spec in its current state is meant to capture the essence of the system, in order to then demonstrate the process of specifying safety and liveness properties, and finding bugs with TLC.
> 
> My idea is that I can sit down with other Herokai who’ve not yet seen TLA+/TLC in action, and work through adding invariants such as “the playhead should never jump backwards” or “a race of skip messages should not cause the server to miss out tracks”. No doubt there are other invariants I’ve yet to think of that my colleagues will suggest right away.
> 
> So it’s a sort of “jumping off point” for demonstrating the practical applications of TLA+ to the folks here.
> 
> Modelling duplicated and reordered messages would indeed be an interesting extension. In its current environment, we get some guarantees of atomicity from the underlying tools (Phoenix/Elixir/Erlang) but questioning those assumptions (and our understanding of those assumptions) would be a good exercise.
> 
> Finally, I’ll confess that though this is the first spec I’ve written, I have read through a good chunk of Specifying Systems and avidly followed the video course… so i can’t claim to have learnt TLA+ in the space of a week :)
> 
> Thanks again. I’ll keep y’all updated on Heroku’s usage of TLA+.
> 
> -- 
> 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+u...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.