---------------------------- MODULE HeadingModel ---------------------------- (***************************************************************************) (* The decision state machine of a self-calibrating magnetometer. *) (* *) (* A handheld compass learns its hard-iron offset from whatever samples *) (* the device happens to take. This spec drops every number (sphere fit, *) (* ellipsoid, priors, RMS) and keeps only the decisions around them: *) (* *) (* - The magnetic ENVIRONMENT is a symbol. The true one, `env`, can *) (* change at any step (a magnet on the case, a new battery, a car). *) (* - The sample BUFFER is a bounded sequence of samples, each tagged *) (* with the environment it was taken in, in insertion order (newest *) (* last). A sample either JOINS (a full ring overwrites the oldest) *) (* or REFRESHES a buffered sample from the same environment, which *) (* then counts as newest. Refresh never touches a sample from another *) (* environment: those sit on a different ring in field space. *) (* - A REFIT over a single-environment buffer yields a candidate for *) (* that environment. A mixed buffer fits no sphere: if it holds at *) (* least DropMin samples the older half is dropped and the consensus *) (* queue cleared, no candidate; below DropMin the fit goes through and *) (* yields a BLEND candidate, a model of neither environment. *) (* A candidate can also fail the field-strength plausibility check. *) (* - The QUEUE keeps the last Q candidates. The live model becomes a *) (* member of the largest same-environment cluster when that cluster *) (* has size >= 2, else the newest candidate. *) (* - A FLUSH (the off-model detector, or any false alarm of it) empties *) (* buffer and queue, keeps the live model but marks it SUSPECT, and in *) (* the same loop iteration drives confidence to zero and drops the *) (* valid latch. Suspect clears on the next adopted candidate. *) (* - CONFIDENCE is abstract, {low, mid, high}: the valid latch rises at *) (* high, falls at low, holds at mid (0.35 / 0.25 hysteresis). *) (* - PERSIST saves the live model, only when one exists and is not *) (* suspect. *) (* *) (* Abstracted away: sample ageing (a 15-minute eviction; every bound here *) (* is shown without it), the refit cadence (a refit needs at least one *) (* sample since the last), the best-RMS tie-break inside a cluster, the *) (* gyro, the GPS cross-check that feeds confidence. *) (* *) (* HeadingModelNoDrop.tla is the negative control: an inconsistent buffer *) (* yields no candidate but keeps every sample. BoundedBlend fails there. *) (***************************************************************************) EXTENDS Naturals, Sequences, FiniteSets CONSTANTS Envs, \* magnetic environments, e.g. {E1, E2} Blend, \* the "environment" of a model fitted to a mixed buffer NoModel, \* no live / persisted model yet BufMax, \* sample buffer capacity MinFit, \* samples needed before a refit runs (MIN_SAMPLES) DropMin, \* samples needed for an inconsistent refit to drop the older \* half instead of fitting through both rings (2*MIN_SAMPLES \* as built; MinFit for the corrected design) Q, \* consensus queue length MaxBlendRefits \* the bound BoundedBlend checks ASSUME /\ Blend \notin Envs /\ NoModel \notin Envs /\ Blend # NoModel /\ BufMax \in Nat \ {0} /\ MinFit \in 1..BufMax /\ DropMin \in MinFit..BufMax /\ Q \in Nat \ {0} /\ MaxBlendRefits \in Nat Low == "low" Mid == "mid" High == "high" Conf == {Low, Mid, High} CandEnvs == Envs \cup {Blend} Models == {NoModel} \cup [env: CandEnvs, passed: BOOLEAN] Seqs(S, n) == UNION {[1..k -> S] : k \in 0..n} VARIABLES env, \* the true magnetic environment right now buf, \* sample buffer: sequence of environment tags, newest last touched, \* a sample was admitted since the last refit queue, \* consensus queue: candidate environments, newest last live, \* the live model suspect, \* live model kept after a flush, not trusted until a refit conf, \* confidence as last computed latched, \* the valid latch (what the UI calls "compass valid") persisted, \* the model in flash blendRefits \* history: refits run on a mixed buffer since env last changed vars == <> TypeOK == /\ env \in Envs /\ buf \in Seqs(Envs, BufMax) /\ touched \in BOOLEAN /\ queue \in Seqs(CandEnvs, Q) /\ live \in Models /\ suspect \in BOOLEAN /\ conf \in Conf /\ latched \in BOOLEAN /\ persisted \in Models /\ blendRefits \in 0..(MaxBlendRefits + 1) Init == /\ env \in Envs /\ buf = << >> /\ touched = FALSE /\ queue = << >> /\ live = NoModel /\ suspect = FALSE /\ conf = Low /\ latched = FALSE /\ persisted = NoModel /\ blendRefits = 0 \* ---- buffer helpers --------------------------------------------------------- Has(b, e) == \E i \in 1..Len(b) : b[i] = e Consistent(b) == \A i, j \in 1..Len(b) : b[i] = b[j] Mixed(b) == Has(b, env) /\ \E i \in 1..Len(b) : b[i] # env Without(b, i) == SubSeq(b, 1, i - 1) \o SubSeq(b, i + 1, Len(b)) KeepNewer(b) == SubSeq(b, Len(b) - Len(b) \div 2 + 1, Len(b)) \* dropOlderHalf \* ---- queue helpers ---------------------------------------------------------- Count(q, e) == Cardinality({i \in 1..Len(q) : q[i] = e}) Push(q, c) == IF Len(q) < Q THEN Append(q, c) ELSE Append(Tail(q), c) MaxCount(q) == CHOOSE m \in 0..Q : /\ \E e \in CandEnvs : Count(q, e) = m /\ \A e \in CandEnvs : Count(q, e) <= m \* the largest cluster wins once it has two members; a lone newcomer waits. \* Ties inside the largest cluster go to the best RMS, which is abstracted \* to "any member of a largest cluster". Winners(q) == IF MaxCount(q) >= 2 THEN {e \in CandEnvs : Count(q, e) = MaxCount(q)} ELSE {q[Len(q)]} (***************************************************************************) (* The adversary: the magnetic surroundings change. *) (***************************************************************************) EnvChange == /\ \E e \in Envs \ {env} : env' = e /\ blendRefits' = 0 /\ UNCHANGED <> (***************************************************************************) (* admit(): a sample far from every buffered one joins (a full ring *) (* overwrites the oldest slot); one near a buffered sample of the same *) (* environment refreshes it and becomes the newest. *) (***************************************************************************) Join == buf' = IF Len(buf) < BufMax THEN Append(buf, env) ELSE Append(Tail(buf), env) Refresh == \E i \in 1..Len(buf) : buf[i] = env /\ buf' = Append(Without(buf, i), env) Sample == /\ Join \/ Refresh /\ touched' = TRUE /\ UNCHANGED <> (***************************************************************************) (* refit(): one batch fit over the buffer. *) (***************************************************************************) Candidate == IF Consistent(buf) THEN buf[1] ELSE Blend Refit == /\ touched /\ Len(buf) >= MinFit /\ touched' = FALSE /\ blendRefits' = IF Mixed(buf) THEN blendRefits + 1 ELSE blendRefits /\ IF ~Consistent(buf) /\ Len(buf) >= DropMin THEN \* two environments in one buffer: keep the newer half, forget the \* candidates that were fitted through both, no candidate now /\ buf' = KeepNewer(buf) /\ queue' = << >> /\ UNCHANGED <> ELSE \E passed \in BOOLEAN : \* plausibleField IF ~passed THEN UNCHANGED <> ELSE LET q == Push(queue, Candidate) IN \E w \in Winners(q) : /\ queue' = q /\ live' = [env |-> w, passed |-> passed] \* adopt() /\ suspect' = FALSE /\ UNCHANGED buf /\ UNCHANGED <> (***************************************************************************) (* flush(): the off-model detector fired. The buffer and queue go, the *) (* live model stays but is suspect. In the same loop() iteration *) (* confidence() returns 0 because of the suspect flag, and the latch falls: *) (* no state observable between iterations shows a suspect model as valid. *) (***************************************************************************) Flush == /\ live # NoModel /\ buf' = << >> /\ queue' = << >> /\ touched' = FALSE /\ suspect' = TRUE /\ conf' = Low /\ latched' = FALSE /\ UNCHANGED <> (***************************************************************************) (* The tail of loop(): confidence and the valid latch with hysteresis. *) (***************************************************************************) Tick == /\ \E c \in Conf : /\ (suspect \/ live = NoModel) => c = Low /\ conf' = c /\ latched' = IF c = High THEN TRUE ELSE IF c = Low THEN FALSE ELSE latched /\ UNCHANGED <> (***************************************************************************) (* save(): periodic, only with a model that is not suspect. *) (***************************************************************************) Persist == /\ live # NoModel /\ ~suspect /\ persisted' = live /\ UNCHANGED <> Next == EnvChange \/ Sample \/ Refit \/ Flush \/ Tick \/ Persist (***************************************************************************) (* PROPERTIES CHECKED *) (***************************************************************************) \* What the UI shows: the compass when the latch is up, else the GPS course \* while walking, else nothing. Walking is an input, so quantify over it. Shown(walking) == IF latched THEN "mag" ELSE IF walking THEN "gps" ELSE "none" \* 1. A suspect model is never the shown heading source. NoSuspectShown == \A walking \in BOOLEAN : Shown(walking) = "mag" => ~suspect \* 2. The live model was a candidate that passed the plausibility check and, \* whenever the queue is non-empty, is a member of it. LiveFromQueue == live # NoModel => /\ live.passed /\ queue # << >> => Has(queue, live.env) \* 3. A cluster of two or more agreeing candidates always owns the live model, \* so a lone newest candidate of another environment is never adopted. OutlierRejected == \A e \in CandEnvs : Count(queue, e) >= 2 => (live # NoModel /\ live.env = e) \* 4. Flash is only ever written with a model that is not suspect. PersistStep == persisted' # persisted => ~suspect PersistNotSuspect == [][PersistStep]_vars \* 5. The latch moves only with confidence at the matching rail. LatchStep == latched' # latched => \/ (latched' /\ conf' = High) \/ (~latched' /\ conf' = Low) LatchHysteresis == [][LatchStep]_vars \* 6. Bounded blend: since the environment last changed, at most \* MaxBlendRefits refits have run over a buffer holding samples from both \* the current environment and another. Each such refit halves the \* buffer from the old end, so a buffer of BufMax samples is clean after \* ceil(log2 BufMax) of them; with no drop the count is unbounded. BoundedBlend == blendRefits <= MaxBlendRefits =============================================================================