Spec Review Request

[Jamie White <ja...@xxxxxxxxxxxxx>]

Hi there

As part of a recent hack week, a group of folks at Heroku set about learning TLA+. Amongst other exercises, I wrote a spec for a “toy distributed system” we created last year called HKFM. It’s a radio station/jukebox of sorts and (I think) lent itself nicely to temporal specification.

This is my first spec, so I’d hugely appreciate feedback, criticism, and advice for future specs.

You’ll find the ascii version and PDF here:
https://github.com/jgwhite/hkfm-spec

Many thanks in advance!

Jamie