gistfile1.tla

---------------------------- MODULE NodeManager ----------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS ChildNodeIds

NumMoves == 6
MaxHeight == 3

VARIABLES 
    nodes,          \* Array of node records
    resyncQueue,    \* Queue of node IDs waiting for resync
    moveCount,      \* Number of moves performed so far
    pendingMoves,   \* Moves that have been calculated but not yet committed
    pendingResyncs  \* Resync operations that have been calculated but not yet committed

vars == <<nodes, resyncQueue, moveCount, pendingMoves, pendingResyncs>>

Null == "Null"
RootId == "RootId"
NodeIds == {RootId} \cup ChildNodeIds
Symmetry == Permutations(ChildNodeIds)

\* Initialize nodes - node 0 is root, others are children of root
InitNodes == 
    [i \in NodeIds |-> 
        [id |-> i,
         parentId |-> IF i = RootId THEN Null ELSE RootId,
         height |-> IF i = RootId THEN 1 ELSE 0,
         version |-> 0]]

\* Helper function to find maximum of a set of integers
Max(S) == IF S = {} THEN -1 ELSE CHOOSE x \in S : \A y \in S : y <= x

\* Helper function to get range of a sequence
Range(seq) == {seq[i] : i \in 1..Len(seq)}

\* Helper function to reverse a sequence
RECURSIVE Reverse(_)
Reverse(seq) == 
    IF seq = <<>> THEN <<>>
    ELSE Append(Reverse(Tail(seq)), Head(seq))

\* Helper function to get path from node to root (returns sequence in root-to-node order)
RECURSIVE PathFromRoot(_)
PathFromRoot(nodeId) ==
    IF nodeId = Null THEN <<>>
    ELSE LET node == nodes[nodeId]
         IN PathFromRoot(node.parentId) \o <<node>>

\* Check if moving nodeId to parentId would create a cycle
WouldCreateCycle(nodeId, parentId) ==
    LET path == PathFromRoot(parentId)
    IN \E i \in 1..Len(path) : path[i].id = nodeId

\* Check if move would exceed depth limit
WouldExceedDepth(nodeId, parentId) ==
    LET newPath == PathFromRoot(parentId)
        node == nodes[nodeId]
    IN Len(newPath) + node.height > MaxHeight

\* Calculate correct height for a node based on its children
CalculateHeight(nodeId) ==
    LET children == {i \in NodeIds : nodes[i].parentId = nodeId}
    IN IF children = {} THEN 0
       ELSE Max({nodes[child].height : child \in children}) + 1

\* Update heights along path upward from child
RECURSIVE UpdateHeightsUpward(_, _)
UpdateHeightsUpward(pathSeq, childNode) ==
    IF pathSeq = <<>> THEN {}  \* Return empty updates
    ELSE LET parent == Head(pathSeq)
             restPath == Tail(pathSeq)
         IN IF parent.height >= childNode.height + 1
            THEN {parent}  \* Need exclusive lock, "writing" unchanged height.
            ELSE LET newParent == [parent EXCEPT 
                        !.height = childNode.height + 1,
                        !.version = parent.version]  \* Don't increment version yet
                     updates == UpdateHeightsUpward(restPath, newParent)
                 IN updates \cup {newParent}

\* Combined move request processing - immediately calculate when request is made
ProcessMoveRequest ==
    /\ moveCount < NumMoves
    \* /\ Len(pendingMoves) < 3  \* Can improve perf but doesn't cover all possibilities
    \* /\ Len(pendingResyncs) < 3
    /\ \E nodeId \in ChildNodeIds, parentId \in NodeIds :
        /\ nodeId # parentId  \* Don't allow self-parent
        /\ nodes[nodeId].parentId # parentId  \* Don't allow no-op moves
        /\ ~WouldCreateCycle(nodeId, parentId)
        /\ ~WouldExceedDepth(nodeId, parentId)
        /\ moveCount' = moveCount + 1
        /\ LET node == nodes[nodeId]
            oldParentId == node.parentId
            newPath == PathFromRoot(parentId)
            \* Create new node with updated parent
            newNode == [node EXCEPT !.parentId = parentId]
            \* Calculate height updates along new path
            heightUpdates == UpdateHeightsUpward(Reverse(newPath), newNode)
            allUpdates == heightUpdates \cup {newNode}
            \* Create pending move record   
            pendingMove == [updates |-> allUpdates, 
                            oldParentId |-> oldParentId]
            IN /\ pendingMoves' = Append(pendingMoves, pendingMove)
                /\ UNCHANGED <<nodes, resyncQueue, pendingResyncs>>

\* Helper function to check for version conflicts and apply updates
AtomicUpdate(allUpdates) ==
    LET hasUpdateConflict == \E update \in allUpdates : 
                               nodes[update.id].version # update.version
        hasConflict ==  hasUpdateConflict
        newNodes == [i \in NodeIds |-> 
                       IF \E update \in allUpdates : update.id = i 
                       THEN LET update == CHOOSE u \in allUpdates : u.id = i
                            IN [update EXCEPT !.version = update.version + 1]
                       ELSE nodes[i]]
    IN <<hasConflict, newNodes>>

\* Helper function to add node to resync queue if not already present
AddToResyncQueue(nodeId, currentQueue) ==
    IF nodeId = Null THEN currentQueue
    ELSE IF \E i \in 1..Len(currentQueue) : currentQueue[i] = nodeId
         THEN currentQueue  \* Already in queue, don't add duplicate
         ELSE Append(currentQueue, nodeId)  \* Add to end of queue

\* Commit calculated move (atomic write phase)
CommitMoveRequest ==
    /\ pendingMoves # <<>>
    /\ LET pendingMove == Head(pendingMoves)
           allUpdates == pendingMove.updates
           oldParentId == pendingMove.oldParentId
           updateResult == AtomicUpdate(allUpdates)
           hasConflict == updateResult[1]
           newNodes == updateResult[2]
       IN /\ pendingMoves' = Tail(pendingMoves)
          /\ IF hasConflict
             THEN /\ UNCHANGED <<nodes, resyncQueue, moveCount>>
             ELSE /\ nodes' = newNodes
                  /\ \* Add old parent to resync queue if needed
                     resyncQueue' = AddToResyncQueue(oldParentId, resyncQueue)
                  /\ UNCHANGED moveCount
          /\ UNCHANGED pendingResyncs

\* Process resync height calculation (read phase) - takes from front of queue
ProcessResyncHeight ==
    /\ resyncQueue # <<>>
    /\ LET nodeId == Head(resyncQueue)  \* Take from front of queue (FIFO)
           correctHeight == CalculateHeight(nodeId)
           node == nodes[nodeId]
       IN IF node.height = correctHeight
          THEN \* Height is correct, remove from queue
               /\ resyncQueue' = Tail(resyncQueue)
               /\ UNCHANGED <<nodes, moveCount, pendingMoves, pendingResyncs>>
          ELSE \* Calculate height update
               /\ LET newNode == [node EXCEPT !.height = correctHeight]
                      pendingResync == [updates |-> {newNode}, nodeId |-> nodeId]
                  IN /\ resyncQueue' = Tail(resyncQueue)  \* Remove from front
                     /\ pendingResyncs' = Append(pendingResyncs, pendingResync)
                     /\ UNCHANGED <<nodes, moveCount, pendingMoves>>

\* Commit calculated resync (atomic write phase)
CommitResyncHeight ==
    /\ pendingResyncs # <<>>
    /\ LET pendingResync == Head(pendingResyncs)
           allUpdates == pendingResync.updates
           nodeId == pendingResync.nodeId
           updateResult == AtomicUpdate(allUpdates)
           hasConflict == updateResult[1]
           newNodes == updateResult[2]
       IN /\ pendingResyncs' = Tail(pendingResyncs)
          /\ IF hasConflict
             THEN \* Resync failure - add back to end of queue for retry
                  /\ resyncQueue' = AddToResyncQueue(nodeId, resyncQueue)
                  /\ UNCHANGED <<nodes, moveCount>>
             ELSE \* Resync success - apply changes and potentially propagate upward
                  /\ nodes' = newNodes
                  /\ LET oldNode == nodes[nodeId]  \* Use old node to get parent
                     IN resyncQueue' = AddToResyncQueue(oldNode.parentId, resyncQueue)
                  /\ UNCHANGED moveCount
          /\ UNCHANGED pendingMoves

\* Check if we're in a terminal state (all operations complete)
Done == 
    /\ moveCount = NumMoves
    /\ pendingMoves = <<>>
    /\ pendingResyncs = <<>>
    /\ resyncQueue = <<>>

\* Main specification transitions
Next == 
    \/ ProcessMoveRequest
    \/ CommitMoveRequest
    \/ ProcessResyncHeight
    \/ CommitResyncHeight
    \/ (Done /\ UNCHANGED vars)  \* Allow stuttering when done

Init == 
    /\ nodes = InitNodes
    /\ moveCount = 0
    /\ pendingMoves = <<>>
    /\ resyncQueue = <<>>
    /\ pendingResyncs = <<>>

Spec == Init /\ [][Next]_vars

\* INVARIANTS

\* 1. No cycles exist in the tree structure
NoCycles == 
    \A nodeId \in NodeIds :
        LET parentId == nodes[nodeId].parentId
        IN parentId = Null \/ nodeId \notin {node.id : node \in Range(PathFromRoot(parentId))}

\* 2. No node has height > max
MaxHeightBound == 
    \A nodeId \in NodeIds : nodes[nodeId].height <= MaxHeight

\* 3. Height accurately represents the height of subtree
AccurateHeight == 
    \A nodeId \in NodeIds :
        nodes[nodeId].height = CalculateHeight(nodeId)

SteadyState == pendingMoves = <<>> /\ pendingResyncs = <<>> /\ resyncQueue = <<>>

\* Simplified type invariant without explicit type annotations
TypeOK ==
    /\ nodes \in [NodeIds -> [id: NodeIds, parentId: NodeIds \cup {Null}, height: 0..MaxHeight, version: 0..NumMoves]]
    /\ moveCount \in 0..NumMoves
    /\ resyncQueue \in Seq(NodeIds)

\* Main safety property
Safety == 
    /\ TypeOK
    /\ MaxHeightBound
    /\ NoCycles
    /\ SteadyState => AccurateHeight

\* Liveness property - all moves eventually get processed
Liveness == 
    moveCount = NumMoves => <>SteadyState

(*
CONSTANTS
    ChildNodeIds = {n1, n2, n3, n4, n5}

SYMMETRY Symmetry

SPECIFICATION Spec
INVARIANT Safety
*)
=============================================================================