Yes, I suppose I'll try my naive TLA+ approach of modeling what I can as I document various parts of the system and see where it gets me. P looks like an intere

Yes, I suppose I'll try my naive TLA+ approach of modeling what I can as I document various parts of the system and see where it gets me. P looks like an interesting experiment to dabble in.