# A simple message delivery model

**URL:** <https://alloytools.discourse.group/t/a-simple-message-delivery-model/133>\
**Category:** models\
**Created:** [December 18, 2020, 3:45pm UTC](https://alloytools.discourse.group/t/a-simple-message-delivery-model/133 "2020-12-18T15:45:01Z")\
**Posts on this page:** 3\
**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:** [December 18, 2020, 3:45pm UTC](https://alloytools.discourse.group/t/a-simple-message-delivery-model/133/1 "2020-12-18T15:45:01Z")

</div>

I’ve been reworking a simple at-least-once delivery model written up in TLA+ here [https://blog.gchinis.com/posts/serverless-specification-with-tla/](https://blog.gchinis.com/posts/serverless-specification-with-tla/). It’s probably not entirely idiomatic Alloy (using Electrum), but it’ll do. I can get the success cases, but I can’t force the liveness failures mentioned in the article. What screamingly obvious thing am I missing?

Incidentally, the `or` clauses in `traces` look to me like a naive version of the `fair` marker in TLA+ in the original. Is that plausible or is there a deeper comparison?

Thanks all  
S

```
module queues
open util/ordering[Generation]
open util/ternary

// https://blog.gchinis.com/posts/serverless-specification-with-tla/

sig Generation {}

sig Message {}

one sig System {
  , var generation: one Generation
  , var queue : Message -> Generation
  , var received : Message -> Generation
}

pred init {
  no queue
  no received
  System.generation = Generation <: first
}

pred skip[] {
  queue' = queue
  received' = received
  generation' = generation
}

pred publish[m: Message] {
  queue' = queue ++ System -> m -> System.generation

  received' = received
  generation' = generation
}

pred consume[m: Message] {
	let gen = System.queue[m] | {
    some gen

    received' = received ++ System -> m -> gen
    queue' = queue - System -> m -> gen
  }
  generation' = generation
}

pred receive[m: Message] {
	let gen = System.queue[m] | {
    some gen

    received' = received ++ System -> m-> gen
  }

	queue' = queue
  generation' = generation
}

pred nextGeneration[] {
  some generation.next

  queue' = queue
  received' = received
  generation' = generation.next
}

fact traces {
  init
  always (
    skip[] or 
	nextGeneration[] or 
    (some m: Message | publish[m] or consume[m] or receive[m])
  )
}

liveness: check {
  eventually (
		let lastGeneration = (Generation <: last) {
      all g: ran[received] | g = lastGeneration
    }
  )	
} for 5 but 2 Generation

run {
	some Message
  eventually (
		let lastGeneration = (Generation <: last) {
			System.generation = lastGeneration
      all m: Message | System.received[m] = lastGeneration
    }
  )
} for 5 but 2 Generation
```

---

<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:** [December 21, 2020, 2:42pm UTC](https://alloytools.discourse.group/t/a-simple-message-delivery-model/133/2 "2020-12-21T14:42:34Z")

</div>

Hi,  
I haven’t looked at your problem in detail but it seems you forgot an `always` after your `eventually`, if you want to follow the PlusCal spec, don’t you?  
Regarding fairness, it’s not linked to disjunction in `traces`. Disjunction in `traces` just says what can happen (this event, or that one, or that other one…). OTOH fairness constraints are here to _exclude_ **executions** that _formally_ comply with the specification of traces, but that you don’t want to see.

---

<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:** [December 23, 2020, 4:51pm UTC](https://alloytools.discourse.group/t/a-simple-message-delivery-model/133/3 "2020-12-23T16:51:16Z")

</div>

Thanks for helping. I’m confused. I’m not sure what `always` would add to the check. I thought that the point of a check was to look for counterexamples, so it should be able to find situations in which there were messages that are not in the latest generation. To clarify, the condition in the check is only required at the end, there will be intermediate steps where it’s not true.