Hello from MCP server
--------------------------- MODULE BookInheritance ---------------------------
(*
* PlusCal specification for the simplified book inheritance model.
*
* Key concepts:
* - Upstream books (e.g., "TNFR Legacy Plumbing") owned by TNFR org
* - Child books (e.g., "Homer's Plumbing") that inherit from upstream
* - Each record has an org_id to track origin
* - Queries prefer child org data, fall back to parent org data
*)
EXTENDS Integers, Sequences, FiniteSets, TLC
CONSTANTS
TNFR_ORG, \* The upstream organization (e.g., "tnfr")
HOMER_ORG, \* A child organization (e.g., "homers_plumbing")
TNFR_BOOK, \* Upstream book ID (e.g., "tnfr_legacy_plumbing")
HOMER_BOOK, \* Child book ID (e.g., "homers_plumbing_book")
ITEMS \* Set of possible item refIds (e.g., {"platinum_tier", "drain_cleaning"})
(*--algorithm BookSync
variables
\* The remote API state (source of truth for each org's changes)
api_tnfr_items = [i \in ITEMS |-> [exists |-> FALSE, name |-> "", price |-> 0]],
api_homer_items = [i \in ITEMS |-> [exists |-> FALSE, name |-> "", price |-> 0]],
\* Local SQLite database - stores items with org_id to track origin
\* Each item can have entries from multiple orgs
local_db = [i \in ITEMS |-> [
tnfr |-> [exists |-> FALSE, name |-> "", price |-> 0],
homer |-> [exists |-> FALSE, name |-> "", price |-> 0]
]],
\* Sync timestamps per book
last_sync_tnfr = 0,
last_sync_homer = 0,
\* API change timestamps (incremented when changes occur)
api_timestamp_tnfr = 0,
api_timestamp_homer = 0,
\* Query result
query_result = [i \in ITEMS |-> [exists |-> FALSE, name |-> "", price |-> 0]];
define
\* INVARIANT: Homer's customizations are never lost
\* If Homer has an item, it should always be in local_db after sync
HomerDataPreserved ==
\A i \in ITEMS:
api_homer_items[i].exists => local_db[i].homer.exists
\* INVARIANT: Query always prefers Homer's data over TNFR
\* When both exist, query_result should match Homer's version
QueryPrefersChild ==
\A i \in ITEMS:
(local_db[i].homer.exists /\ local_db[i].tnfr.exists) =>
(query_result[i].name = local_db[i].homer.name)
\* INVARIANT: Query falls back to TNFR when Homer doesn't have item
QueryFallsBackToParent ==
\A i \in ITEMS:
(local_db[i].tnfr.exists /\ ~local_db[i].homer.exists) =>
(query_result[i].name = local_db[i].tnfr.name)
end define;
\* ============================================================================
\* TNFR (upstream) makes changes to their book
\* ============================================================================
process TNFRMakesChanges = "tnfr_changes"
begin
TNFRUpdate:
while TRUE do
with item \in ITEMS, newName \in {"Platinum", "Diamond", "Gold"}, newPrice \in {100, 200, 300} do
api_tnfr_items[item] := [exists |-> TRUE, name |-> newName, price |-> newPrice];
api_timestamp_tnfr := api_timestamp_tnfr + 1;
end with;
end while;
end process;
\* ============================================================================
\* Homer (child org) makes customizations to their book
\* ============================================================================
process HomerMakesChanges = "homer_changes"
begin
HomerUpdate:
while TRUE do
with item \in ITEMS, newName \in {"Homer Special", "Budget", "Premium"}, newPrice \in {150, 250, 350} do
api_homer_items[item] := [exists |-> TRUE, name |-> newName, price |-> newPrice];
api_timestamp_homer := api_timestamp_homer + 1;
end with;
end while;
end process;
\* ============================================================================
\* Sync process - runs periodically (every 10 minutes in real system)
\* KEY: Syncs parent FIRST, then child, with separate org_id tracking
\* ============================================================================
process SyncDatabase = "sync"
begin
SyncLoop:
while TRUE do
\* Step 1: Sync TNFR (parent) book FIRST
SyncTNFR:
if api_timestamp_tnfr > last_sync_tnfr then
\* Apply TNFR changes to local_db with org_id = tnfr
local_db := [i \in ITEMS |-> [
tnfr |-> api_tnfr_items[i], \* Update TNFR layer
homer |-> local_db[i].homer \* Preserve Homer layer
]];
last_sync_tnfr := api_timestamp_tnfr;
end if;
\* Step 2: Sync Homer (child) book SECOND
SyncHomer:
if api_timestamp_homer > last_sync_homer then
\* Apply Homer changes to local_db with org_id = homer
local_db := [i \in ITEMS |-> [
tnfr |-> local_db[i].tnfr, \* Preserve TNFR layer
homer |-> api_homer_items[i] \* Update Homer layer
]];
last_sync_homer := api_timestamp_homer;
end if;
end while;
end process;
\* ============================================================================
\* Query process - demonstrates the "prefer child, fallback to parent" pattern
\* ============================================================================
process ExecuteQuery = "query"
begin
QueryLoop:
while TRUE do
\* Build query result: prefer Homer data, fall back to TNFR
query_result := [i \in ITEMS |->
IF local_db[i].homer.exists THEN
local_db[i].homer \* Child org data takes precedence
ELSE
local_db[i].tnfr \* Fall back to parent org data
];
end while;
end process;
end algorithm; *)
\* ============================================================================
\* PROPERTIES TO VERIFY
\* ============================================================================
\* Temporal property: Eventually, if TNFR publishes data, it becomes queryable
\* (unless Homer overrides it)
TNFRDataEventuallyVisible ==
\A i \in ITEMS:
[](api_tnfr_items[i].exists =>
<>(query_result[i].exists))
\* Temporal property: Homer's customizations are always reflected in queries
HomerCustomizationsReflected ==
\A i \in ITEMS:
[](api_homer_items[i].exists =>
<>(query_result[i].name = api_homer_items[i].name))
=============================================================================
(*
SUMMARY OF THE MODEL:
1. DATA STRUCTURE
- Each item in local_db has TWO layers: {tnfr: {...}, homer: {...}}
- This maps to: org_id column distinguishes records from different orgs
2. SYNC ORDER (Critical!)
- Parent book (TNFR) syncs FIRST
- Child book (Homer) syncs SECOND
- Each sync only touches its own org layer
3. QUERY PATTERN
- SELECT with COALESCE-like logic:
"Give me Homer's version if it exists, otherwise TNFR's version"
4. SQL IMPLEMENTATION SKETCH:
-- Store with org_id
INSERT INTO offers (id, refId, name, price, org_id, book)
VALUES (?, ?, ?, ?, 'tnfr', 'tnfr_legacy_plumbing');
-- Query with preference
SELECT COALESCE(homer.name, tnfr.name) as name,
COALESCE(homer.price, tnfr.price) as price
FROM (SELECT * FROM offers WHERE org_id = 'tnfr' AND refId = ?) as tnfr
LEFT JOIN (SELECT * FROM offers WHERE org_id = 'homer' AND refId = ?) as homer
ON tnfr.refId = homer.refId;
-- Or simpler with ORDER BY and LIMIT:
SELECT * FROM offers
WHERE refId = ?
ORDER BY CASE org_id WHEN 'homer' THEN 0 ELSE 1 END
LIMIT 1;
5. KEY INVARIANTS:
- Homer's data is NEVER overwritten by TNFR sync
- Queries ALWAYS prefer Homer's data when it exists
- TNFR data is always available as fallback
*)