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

Spec Review Request

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:

Many thanks in advance!