TokenLabels

---------------------------- MODULE TokenLabels ---------------------------- (***************************************************************************) (* A data-publishing pipeline for energy "nutrition labels". *) (* *) (* Source measurements come from a benchmark repo. Each measurement has: *) (* - an arm (runtime identifier) *) (* - a methodology group (e.g. battery-delta vs. wall-power windows; *) (* abstracted here as model values) *) (* - a quantization/build string (possibly missing, modeled as NoQuant) *) (* - an energy value jPerTok (abstracted as a small natural) *) (* *) (* A build step derives labels from measurements. The label's kcal value *) (* is derived ONLY from jPerTok via an abstract derivation function. *) (* Labels are published grouped by methodology group, and ranking badges *) (* ("class best") are computed only among labels of the same group. *) (* *) (* Checked invariants: *) (* PublishedHasQuant - every published label carries a non-empty *) (* quantization/build *) (* PublishedHasSource - every published label references an existing *) (* source measurement *) (* NoCrossGroupRanking - badges compare only same-group labels *) (* DerivationConsistent - a published label's kcal corresponds to its *) (* measurement's jPerTok (and group/quant match) *) (***************************************************************************) EXTENDS Naturals, FiniteSets, TLC CONSTANTS Arms, \* runtime identifiers Groups, \* methodology groups Quants, \* valid (non-empty) quantization/build strings NoQuant, \* marker for a measurement lacking a quantization string Ids, \* measurement / source-file identifiers JVals \* possible jPerTok energy values (small naturals) ASSUME NoQuant \notin Quants ASSUME JVals \subseteq Nat (***************************************************************************) (* Abstract derivation: stands in for kcal = jPerTok * 1e6 / 4184. *) (* All that matters for the design is that kcal is a function of jPerTok *) (* alone, applied identically at build time and demanded by the invariant. *) (***************************************************************************) Derive(j) == j * 239 MeasRec == [arm: Arms, group: Groups, quant: Quants \cup {NoQuant}, j: JVals] LabelRec == [src: Ids, group: Groups, quant: Quants, kcal: {Derive(j) : j \in JVals}] BadgeRec == [src: Ids, group: Groups, comparedWith: SUBSET Ids] VARIABLES meas, \* partial function Ids -> MeasRec: ingested measurements labels, \* set of LabelRec: labels derived by the build step published, \* subset of labels published onto the site badges \* set of BadgeRec: "class best" style ranking badges vars == <<meas, labels, published, badges>> TypeOK == /\ DOMAIN meas \subseteq Ids /\ \A id \in DOMAIN meas : meas[id] \in MeasRec /\ labels \subseteq LabelRec /\ published \subseteq labels /\ badges \subseteq BadgeRec ----------------------------------------------------------------------------- Init == /\ meas = [id \in {} |-> {}] /\ labels = {} /\ published = {} /\ badges = {} (* A new measurement arrives from the benchmark repo, possibly one that *) (* lacks a quantization/build string (quant = NoQuant). *) Ingest == \E id \in Ids \ DOMAIN meas : \E r \in MeasRec : /\ meas' = meas @@ (id :> r) /\ UNCHANGED <<labels, published, badges>> (* The build step derives a label from a measurement. Design decisions *) (* under check: it refuses measurements without a quantization string, *) (* and kcal comes only from the measurement's jPerTok via Derive. *) Build == \E id \in DOMAIN meas : /\ meas[id].quant # NoQuant /\ ~\E l \in labels : l.src = id /\ labels' = labels \cup {[src |-> id, group |-> meas[id].group, quant |-> meas[id].quant, kcal |-> Derive(meas[id].j)]} /\ UNCHANGED <<meas, published, badges>> (* A built label goes onto the site. *) Publish == \E l \in labels \ published : /\ published' = published \cup {l} /\ UNCHANGED <<meas, labels, badges>> (* A ranking badge is granted to a published label. The comparison set is *) (* exactly the published labels of the SAME methodology group (the design *) (* rule NoCrossGroupRanking checks). At most one badge per source. *) GrantBadge == \E l \in published : /\ ~\E b \in badges : b.src = l.src /\ badges' = badges \cup {[src |-> l.src, group |-> l.group, comparedWith |-> {p.src : p \in {q \in published : q.group = l.group}}]} /\ UNCHANGED <<meas, labels, published>> Next == Ingest \/ Build \/ Publish \/ GrantBadge Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- (* Invariants *) (* 1. Every published label carries a non-empty quantization/build. *) PublishedHasQuant == \A l \in published : l.quant \in Quants (* 2. Every published label's source reference exists among the ingested *) (* measurements. *) PublishedHasSource == \A l \in published : l.src \in DOMAIN meas (* 3. Ranking badges are computed only among labels of the same *) (* methodology group. *) NoCrossGroupRanking == \A b \in badges : \A s \in b.comparedWith : /\ s \in DOMAIN meas /\ meas[s].group = b.group (* 4. A published label's kcal value is exactly the abstract derivation *) (* applied to its source measurement's jPerTok; group and quant carry *) (* through unchanged. *) DerivationConsistent == \A l \in published : /\ l.src \in DOMAIN meas /\ l.kcal = Derive(meas[l.src].j) /\ l.group = meas[l.src].group /\ l.quant = meas[l.src].quant =============================================================================

SPECIFICATION Spec CONSTANTS Arms = {a1, a2} Groups = {g1, g2} Quants = {q1, q2} NoQuant = noq Ids = {m1, m2} JVals = {1, 2} INVARIANTS TypeOK PublishedHasQuant PublishedHasSource NoCrossGroupRanking DerivationConsistent CHECK_DEADLOCK FALSE