How should two microservices communicate?

Let’s analyze two different communication patterns:

• Polling: Service B periodically query Service A for the current state of the users and updates its local storage.
• Event driven: Service A publishes in a queue every time user information is updated. Service B consumes the updates to stay up to date.

Using TLA+ we are going to model the two different patterns to see how well they fit our requirements. In our specification, we are also going to take into account unexpected failures that can affect the system and show how to model them in TLA+.