A simple message delivery model

models
1

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/. 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
2

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.

3

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.