----------------------------- MODULE CalmGlance ----------------------------- (***************************************************************************) (* The glance screen of a calm handheld friend-finder: an e-paper device *) (* on a LoRa mesh that shows ONE friend at a time, the one worth walking *) (* toward. This is the display policy of a single device, abstractly. *) (* *) (* Peers. Every friend has a proximity class set by the world, not by the *) (* device: "far" (out of sight, beacons heard), "near" (in sight, within a *) (* few metres) or "lost" (no beacon for a while). `Env` changes any *) (* peer's class in any step; that is the world moving. *) (* *) (* Focus. `focus` is the one friend on the screen, or None. The rule the *) (* whole design hangs on: the screen never shows someone already in sight, *) (* and it is never empty while there is someone to walk toward. So when *) (* the focused friend walks up, focus moves to someone who is not near, or *) (* to None ("everyone's here") when nobody is; and when focus is None and *) (* someone stops being near, the device picks them. The user may press *) (* "next" to cycle among the friends who are not near. *) (* *) (* Messages. A direct message from p fires one haptic tap (`tap` is TRUE *) (* only in the state right after a DM lands) and pulls focus to p unless p *) (* is already in sight. A crew (group) message is stored silently and *) (* leaves focus alone. Messages are ephemeral: `Tick` ages every message *) (* by one and drops any that reaches TTL. The device holds at most *) (* MaxMsgs messages; an arrival that would exceed that is refused (the *) (* firmware evicts the oldest instead, which is invisible to these *) (* properties). Messages are a set, so two identical arrivals in one age *) (* collapse into one. *) (* *) (* `last` is a history variable naming the kind of the last event; it is *) (* read only by TapOnlyForDM. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Peers, \* the crew, as seen from this device TTL, \* a message is dropped when its age reaches TTL MaxMsgs, \* messages held on the device (this is what bounds the model) None \* focus when nobody is worth walking toward ASSUME /\ TTL \in Nat \ {0} /\ MaxMsgs \in Nat /\ None \notin Peers Classes == {"far", "near", "lost"} Kinds == {"dm", "crew"} Events == {"dm", "crew", "env", "tick", "next", "init"} Msgs == [from: Peers, kind: Kinds, age: 0..TTL] VARIABLES class, \* class[p]: p's proximity class, set by the world focus, \* the one friend on the glance screen, or None msgs, \* messages on the device tap, \* TRUE only in the state right after a DM arrived last \* history: the kind of the last event vars == <> \* The friends worth walking toward under a class assignment. NotNearIn(cls) == {p \in Peers : cls[p] # "near"} NotNear == NotNearIn(class) (***************************************************************************) (* The focus rule, as the set of focus values allowed once the classes *) (* are `cls` and the focus was `f`: keep f while f is not in sight; else *) (* anyone not in sight; else None. Every action that can change a class *) (* or leave the screen empty draws its new focus from this set. *) (***************************************************************************) Reselect(cls, f) == IF f # None /\ cls[f] # "near" THEN {f} ELSE IF NotNearIn(cls) # {} THEN NotNearIn(cls) ELSE {None} TypeOK == /\ class \in [Peers -> Classes] /\ focus \in Peers \cup {None} /\ msgs \in SUBSET Msgs /\ tap \in BOOLEAN /\ last \in Events \* The world may start any way; the screen starts by the focus rule. Init == /\ class \in [Peers -> Classes] /\ focus \in Reselect(class, None) /\ msgs = {} /\ tap = FALSE /\ last = "init" \* A direct message from p: one tap, stored, and focus pulled to p unless \* p is already in sight. DirectMessage(p) == LET m == [from |-> p, kind |-> "dm", age |-> 0] IN /\ Cardinality(msgs \cup {m}) <= MaxMsgs /\ msgs' = msgs \cup {m} /\ focus' = IF class[p] # "near" THEN p ELSE focus /\ tap' = TRUE /\ last' = "dm" /\ UNCHANGED class \* A crew (group) message from p: stored silently, focus untouched. CrewMessage(p) == LET m == [from |-> p, kind |-> "crew", age |-> 0] IN /\ Cardinality(msgs \cup {m}) <= MaxMsgs /\ msgs' = msgs \cup {m} /\ tap' = FALSE /\ last' = "crew" /\ UNCHANGED <> \* The world moves: p's class changes, and the screen follows the focus rule. Env(p, c) == /\ c # class[p] /\ class' = [class EXCEPT ![p] = c] /\ focus' \in Reselect(class', focus) /\ tap' = FALSE /\ last' = "env" /\ UNCHANGED msgs \* Time passes: every message ages by one; any that reaches TTL is gone. Tick == /\ msgs' = {[m EXCEPT !.age = @ + 1] : m \in {m \in msgs : m.age + 1 < TTL}} /\ tap' = FALSE /\ last' = "tick" /\ UNCHANGED <> \* The user presses "next": focus cycles to another friend not in sight. PressNext == /\ focus' \in NotNear \ {focus} /\ tap' = FALSE /\ last' = "next" /\ UNCHANGED <> Next == \/ \E p \in Peers : DirectMessage(p) \/ \E p \in Peers : CrewMessage(p) \/ \E p \in Peers, c \in Classes : Env(p, c) \/ Tick \/ PressNext \* Env is always enabled, so there is no deadlock; checked with \* CHECK_DEADLOCK FALSE all the same, as a matter of house style. (***************************************************************************) (* PROPERTIES CHECKED *) (***************************************************************************) \* 1. The screen never shows a friend who is already in sight. FocusNotInSight == focus # None => class[focus] # "near" \* 2. The screen is never empty while there is someone to walk toward. SomeoneToWalkToward == NotNear # {} => focus # None \* 3. Every stored message is younger than TTL. Ephemeral == \A m \in msgs : m.age < TTL \* 4. The haptic tap fires only for a direct message. TapOnlyForDM == tap => last = "dm" =============================================================================