List Files | Just Commands | Repo | Logs

← back | Copy

------------------------ MODULE BookDependencyResolution ------------------------
(*
 * TLA+ Specification of Book Dependency Resolution
 * From: frontend/src/dataAccess/getDb.ts syncChanges()
 *
 * Models the recursive traversal that collects all books needed for sync:
 *   - Start with org's books
 *   - Walk parent chain upward
 *   - At each node, also resolve dependencies
 *   - Dependencies recursively resolve their parents too
 *)

EXTENDS Naturals, Sequences, FiniteSets

CONSTANTS
    BookIds,            \* Set of all possible book IDs
    OrgBooks            \* Set of book IDs owned by the active org (starting set)

VARIABLES
    books,              \* Accumulated result set: books to sync
    toVisit,            \* Queue of books waiting to be processed
    visited,            \* Set of books already processed (prevent cycles)
    parentOf,           \* Function: book -> parent book (or NULL)
    depsOf              \* Function: book -> set of dependency books

vars == <<books, toVisit, visited, parentOf, depsOf>>

NULL == CHOOSE x : x \notin BookIds

-----------------------------------------------------------------------------
(* Type Invariant *)

TypeOK ==
    /\ books \subseteq BookIds
    /\ toVisit \subseteq BookIds
    /\ visited \subseteq BookIds
    /\ parentOf \in [BookIds -> BookIds \union {NULL}]
    /\ depsOf \in [BookIds -> SUBSET BookIds]

-----------------------------------------------------------------------------
(* Initial State *)

Init ==
    /\ books = {}
    /\ toVisit = OrgBooks          \* Start with org's books
    /\ visited = {}
    /\ parentOf \in [BookIds -> BookIds \union {NULL}]  \* Given by DB
    /\ depsOf \in [BookIds -> SUBSET BookIds]           \* Given by DB

-----------------------------------------------------------------------------
(*
 * Process one book from toVisit queue
 * Corresponds to: getParents(book) which calls getDependencies(parentBook)
 *)

ProcessBook ==
    /\ toVisit # {}
    /\ LET book == CHOOSE b \in toVisit : TRUE
           parent == parentOf[book]
           deps == depsOf[book]
           \* New books to visit: parent (if exists) + all dependencies
           newToVisit == (IF parent # NULL THEN {parent} ELSE {})
                         \union deps
       IN
       /\ books' = books \union {book}           \* Add to result
       /\ visited' = visited \union {book}       \* Mark visited
       /\ toVisit' = (toVisit \ {book})          \* Remove current
                     \union (newToVisit \ visited')  \* Add unvisited relatives
    /\ UNCHANGED <<parentOf, depsOf>>

-----------------------------------------------------------------------------
(* Terminal State - nothing left to process *)

Done ==
    /\ toVisit = {}
    /\ UNCHANGED vars

-----------------------------------------------------------------------------
(* Next State Relation *)

Next == ProcessBook \/ Done

Spec == Init /\ [][Next]_vars /\ WF_vars(ProcessBook)

-----------------------------------------------------------------------------
(* Safety Properties *)

\* All collected books were reachable from org books
AllBooksReachable ==
    \A b \in books:
        \/ b \in OrgBooks
        \/ \E other \in books: parentOf[other] = b
        \/ \E other \in books: b \in depsOf[other]

\* No book processed twice (visited tracking works)
NoDuplicateProcessing ==
    books \subseteq visited

\* Result only contains valid book IDs
ResultValid ==
    books \subseteq BookIds

-----------------------------------------------------------------------------
(* Liveness Properties *)

\* Algorithm eventually terminates
EventuallyDone ==
    <>(toVisit = {})

\* All org books eventually included
OrgBooksIncluded ==
    <>(OrgBooks \subseteq books)

-----------------------------------------------------------------------------
(*
 * Key Insight: The traversal forms a closure over the relation:
 *   related(a,b) <=> parentOf[a] = b \/ b \in depsOf[a]
 *
 * Starting from OrgBooks, we compute the reflexive-transitive closure
 * of `related` to find all books that need syncing.
 *)

\* The complete set that SHOULD be collected (for verification)
ReachableFrom[S \in SUBSET BookIds] ==
    LET Step(T) == T \union {parentOf[b] : b \in T} \union UNION {depsOf[b] : b \in T}
        Closure == LET F[n \in Nat] ==
                       IF n = 0 THEN S
                       ELSE Step(F[n-1])
                   IN UNION {F[n] : n \in 0..Cardinality(BookIds)}
    IN Closure \ {NULL}

\* When done, books equals the reachable closure
CorrectnessOnTermination ==
    (toVisit = {}) => (books = ReachableFrom[OrgBooks])

=============================================================================