# Modelling failures in a protocol

**URL:** <https://alloytools.discourse.group/t/modelling-failures-in-a-protocol/122>\
**Category:** Questions\
**Created:** [October 11, 2020, 10:06am UTC](https://alloytools.discourse.group/t/modelling-failures-in-a-protocol/122 "2020-10-11T10:06:26Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [October 11, 2020, 10:06am UTC](https://alloytools.discourse.group/t/modelling-failures-in-a-protocol/122/1 "2020-10-11T10:06:26Z")

</div>

I’m working on a message protocol between various participants and I’d like to check what happens when a message is dropped, first to show the failure and then to show I’ve fixed it. I believe I’d like to show this in an assertion, as a property of the system, rather than not finding an instance in a run.

I started by trying to show that the various messages line up in an exchange but the generated counterexample I get is to just stop after the first message, which is not very useful.

Suggestions, references to obvious materials, etc?

Thanks all  
S

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [October 12, 2020, 10:38am UTC](https://alloytools.discourse.group/t/modelling-failures-in-a-protocol/122/2 "2020-10-12T10:38:26Z")

</div>

As your description remains a bit vague, it’s not easy to answer. Have you considered checking a _liveness_ property on your protocol? For instance, you may check that _every error will be recovered_ or that _if there’s a point in time when errors don’t happen anymore, then your system will reach a desired state (and remain in it)_. HTH.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [October 12, 2020, 10:52am UTC](https://alloytools.discourse.group/t/modelling-failures-in-a-protocol/122/3 "2020-10-12T10:52:48Z")

</div>

Thanks for responding. It’s a bit vague, because I’m not quite sure how to start. So, perhaps I could check that, eventually, every dropped message is associated with (followed by?) a successful message.

---

<div class="post-metadata">

**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\
**Post date:** [October 12, 2020, 1:59pm UTC](https://alloytools.discourse.group/t/modelling-failures-in-a-protocol/122/4 "2020-10-12T13:59:36Z")

</div>

I’d suggest two things. First, brainstorm a set of properties that you expect the protocol to satisfy. These don’t need to comprise a complete specification, but they will likely be helpful in understanding what can go wrong. Second, make sure that your model of the protocol itself is loose enough to actually account for how the implementation may behave if messages are dropped etc. So make sure, for example, that the receiver of a message does not have any global knowledge of message order or something like that, which would not be available to it in an implementation.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [October 13, 2020, 8:52am UTC](https://alloytools.discourse.group/t/modelling-failures-in-a-protocol/122/5 "2020-10-13T08:52:32Z")

</div>

Thanks. I already have some of this (avoiding global order), but working through the rest. My hope was that I would be able to write checks to produce counterexamples for protocol failures, but I’m struggling to make those non-trivial. More to do…