Pub-Sub for Alloy

pubsub.als

open util/ordering[Time]

let unchanged[x, t, t'] {x.t = x.t'}
sig Time {}

sig Msg {}

sig Pub {
	-- really a topic, but then we're double-using T as a letter
	, msgs: Msg -> Time
}

fact "Each message is only part of one topic" {
	all m: Msg |
		one p: Pub |
			m in p.msgs.Time
}

sig Sub {
	-- subscribers
	, subscribed: Pub -> Time -- what topics subscribed to at T
	, received: Msg -> Time -- what messages we've seen
}


fun publisher[m: Msg]: Pub {
	-- Which Pub published the message. There will only be one
	msgs.Time.m
}

fun origin[m: Msg]: Time {
	-- The time we initially published the message.
	-- NOTE: this works b/c only one publisher can publish a given message
	Pub.msgs[m].min
}

fun received_at[s: Sub, m: Msg]: Time {
	-- The first time a subscriber received the message.
	s.received[m].min
}

fun subs_for_msg[m: Msg]: set Sub {
	-- All of the subs that were subscribed to a topic at the moment
	-- a publisher sent a message. Needed to make sure that NEW subscriptions
	-- don't received the message.

	-- Question: if a subscriber leaves *and comes back* before we message them,
	-- should they receive the message? That sounds like a user requirement problem!
	subscribed.(origin[m]).(m.publisher)
}


//fact "All signatures are used" {
//	all p: Pub |
//		some p.msgs.Time
//}


fact "Published msgs are monotonic" {
	-- maybe this should be an assertion?
	all p: Pub, t': Time - last |
		p.msgs.t' in p.msgs.(t'.next)
}

pred subscribe[s: Sub, p: Pub, t, t': Time] {
	(s -> p) !in subscribed.t
	subscribed.t' = subscribed.t + (s -> p)
}

pred unsubscribe[s: Sub, p: Pub, t, t': Time] {
	(s -> p) in subscribed.t
	subscribed.t' = subscribed.t - (s -> p)

}

pred publish[p: Pub, m: Msg, t, t': Time] {
	(m -> t) !in p.msgs
	-- exactly one change!
	msgs.t' = msgs.t + (p -> m)

}
pred receive[s: Sub, m: Msg, t, t': Time] {
	-- should be s: SET Sub
	s in subs_for_msg[m] -- needed to prevent "delayed subscription" getting msgs
	(m -> t) in s.subscribed.t.msgs	
	(m -> t) !in s.received
	received.t' = received.t + (s -> m)
--	unchanged[msgs, t, t']
}

fact Trace {
	-- Currently we let msgs appear at random: the monotonicity fact
	-- makes sure that they don't "disappear".
	no Pub.msgs.first
  no Sub.received.first
	all t: Time - last |
		let t' = t.next |
			(some p: Pub, s: Sub {
				s.subscribe[p, t, t']
					or
				s.unsubscribe[p, t, t']
--				unchanged[msgs, t, t']
				unchanged[received, t, t']
			}) or 
			(some m: Msg, s: Sub {
				s.receive[m, t, t']
				unchanged[subscribed, t, t']
--				unchanged[received, t, t']

			}) or { --stutter step
				unchanged[subscribed, t, t']
				unchanged[received, t, t']
			}
		
}

pred messages_received_out_of_order[s: Sub, m, m': Msg] {
		m.origin.lt[m'.origin]
		some t: Time {
			(m -> t) !in s.received
			(m' -> t) in s.received
		}
}

-- possible error: subs subscribe to the pub AFTER message, 
-- and then receive it anyway
-- We want to rule that out, so here's a predicate to catch that.

pred messages_only_sent_to_subscribed_topics[s: Sub, m: Msg] {
	all t: Time {
		(m -> t) in s.received => (m.publisher -> origin[m]) in s.subscribed
	}
}
pred messages_only_from_subscribed_topics[s: Sub, m: Msg] {
	all t: Time { -- possibly unnecessary: can do it with a relation trick
--	We can't write
--	(m -> t) in s.received => (m.publisher -> t) in s.subscribed
--  Because that would fail if we unsubscribe after receiving a message.
		(m -> t) in s.received => (m.publisher -> s.received_at[m]) in s.subscribed
	}

}

assert Properties {
	all s: Sub, m: Msg {
		messages_only_sent_to_subscribed_topics[s, m]
		messages_only_from_subscribed_topics[s, m]
	}
}


check Properties for 4 but 10 Time

check {all s: Sub, m: Msg | messages_only_sent_to_subscribed_topics[s, m]} for 4

check {all s: Sub, m: Msg | messages_only_from_subscribed_topics[s, m]} for 4
run {some m, m': Msg, s: Sub | messages_received_out_of_order[s, m, m']} for 4