One thing I want to caution is that that's the translation of PlusCal to "raw TLA+". If you were not using PlusCal, you might write it a different way. For exam

One thing I want to caution is that that's the translation of PlusCal to "raw TLA+". If you were not using PlusCal, you might write it a different way. For example, you wouldn't need a `pc` variable because you could express sending and receiving as short guarded actions.