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
.