You're right :). I sometimes look at that modelling exercise with disappointment; not because I didn't get any value out of it (I got a ton), but because I'm no

You're right :). I sometimes look at that modelling exercise with disappointment; not because I didn't get any value out of it (I got a ton), but because I'm not yet good enough at TLA+ to have been able to successfully write a model that handled all the edge cases.