CalmGlance

----------------------------- 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 it fires) 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. *) (* *) (* Dancing. A dancer is not interrupted. The accelerometer tells the *) (* device when its owner is dancing (`dancing`, set by the owner, not the *) (* device). A direct message that lands while dancing is stored and moves *) (* focus exactly as usual, but the tap is deferred (`owed`) instead of *) (* fired. When the dance stops, the single deferred tap is paid once, *) (* however many messages arrived meanwhile. *) (* *) (* `last` is a history variable naming the kind of the last event; it is *) (* read only by TapOnlyForAPerson. *) (***************************************************************************) 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", "dance", "stopdance"} 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 haptic tap fired last, \* history: the kind of the last event dancing, \* the owner is dancing (accelerometer) owed \* a haptic tap was deferred while dancing and is still owed vars == <<class, focus, msgs, tap, last, dancing, owed>> \* 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 /\ dancing \in BOOLEAN /\ owed \in BOOLEAN \* 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" /\ dancing = FALSE /\ owed = FALSE \* A direct message from p: stored, and focus pulled to p unless p is \* already in sight. One tap, fired now, or owed until the dance stops. 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' = ~dancing /\ owed' = (owed \/ dancing) /\ last' = "dm" /\ UNCHANGED <<class, dancing>> \* 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 <<class, focus, dancing, owed>> \* 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, dancing, owed>> \* 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 <<class, focus, dancing, owed>> \* The user presses "next": focus cycles to another friend not in sight. PressNext == /\ focus' \in NotNear \ {focus} /\ tap' = FALSE /\ last' = "next" /\ UNCHANGED <<class, msgs, dancing, owed>> \* The owner starts dancing (accelerometer). Nothing on screen changes. StartDance == /\ ~dancing /\ dancing' = TRUE /\ tap' = FALSE /\ last' = "dance" /\ UNCHANGED <<class, focus, msgs, owed>> \* The owner stops dancing: the one deferred tap, if any, is paid now. StopDance == /\ dancing /\ dancing' = FALSE /\ tap' = owed /\ owed' = FALSE /\ last' = "stopdance" /\ UNCHANGED <<class, focus, msgs>> 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 \/ StartDance \/ StopDance \* 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 person: a direct message, or the \* tap that message earned, paid when the dance stops. TapOnlyForAPerson == tap => last \in {"dm", "stopdance"} \* 5. A dancer is not interrupted. NoTapWhileDancing == tap => ~dancing \* 6. A tap is owed only while dancing; stopping always settles it. OwedOnlyWhileDancing == owed => dancing =============================================================================

\* Three friends, messages live two ticks, at most two held on the device \* (three fits the design but not the checker's budget once dancing is in). CONSTANTS Peers = {a, b, c} TTL = 2 MaxMsgs = 2 None = None INIT Init NEXT Next INVARIANTS TypeOK FocusNotInSight SomeoneToWalkToward Ephemeral TapOnlyForAPerson NoTapWhileDancing OwedOnlyWhileDancing CHECK_DEADLOCK FALSE