Base Communication model

I want to model MQTT, a message based protocol for publish-subscribe. Does anybody have a good base model for message based communication models that supports unreliable communication and connections breaking?

None that I’m aware of, so I started work on a base model. Will try to get it up when it’s done.

so I started work on a base model

Great!

Can you work on such a base model in a place where I can contribute/comment? Will you leverage the new temporal features?

Sure, I’ll throw up a gist when I have something. I stick to official versions for teaching purposes, so I’m not using the new temporal features.

Have a draft up: Pub-Sub for Alloy · GitHub

Plan to also write a prose breakdown to people learning Alloy, once we decide the model isn’t terrible or anything

EDIT: This is implicit, but one of the ways it models “unreliable communication” is that we don’t have the fact that all s: Sub, m: Message | some t: Time | (m -> t) in s.received.