------------------ MODULE IgnoredWorkspaceHardlinkRouting ------------------
EXTENDS TLC

(***************************************************************************
Generation-level alias safety for ignored-workspace operations and cloning.
***************************************************************************)

CONSTANTS Correct, SplitCloneAliases, MergeCloneObjects, CrossBackingLink,
          LinkedRuntimeRename, UnstableAliasClone, Mode

Modes == {Correct, SplitCloneAliases, MergeCloneObjects, CrossBackingLink,
          LinkedRuntimeRename, UnstableAliasClone}
Names == {"A", "B"}
Policies == {"Host", "Isolated"}
HostObjects == {"H1", "H2"}
IsolatedObjects == {"I1", "I2"}
Objects == HostObjects \cup IsolatedObjects
MaybeObjects == Objects \cup {"None"}
Payloads == {"V1", "V2"}
Phases == {"ReadyHost", "Planning", "Installed", "ReadyCandidate"}
Results == {"None", "Success", "EXDEV"}
Operations == {"None", "SameBackingLink", "CrossBackingLink",
               "LinkedRuntimeRename", "StartupClone"}

ASSUME Mode \in Modes

CloneObject(object) == IF object = "H1" THEN "I1" ELSE "I2"
CandidatePolicies == {
    policy \in [Names -> Policies] : \E name \in Names : policy[name] = "Isolated"
}

VARIABLES phase, online, candidatePolicy, hostNames, isolatedNames, objectValues,
          capturedHostNames, capturedHostValues, operation, result,
          splitCloneAliases, mergedCloneObjects, crossBackingLinked,
          linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted

vars == <<phase, online, candidatePolicy, hostNames, isolatedNames, objectValues,
          capturedHostNames, capturedHostValues, operation, result,
          splitCloneAliases, mergedCloneObjects, crossBackingLinked,
          linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>

SafetyFlags == <<splitCloneAliases, mergedCloneObjects, crossBackingLinked,
                 linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>

TypeOK ==
    /\ phase \in Phases
    /\ online \in BOOLEAN
    /\ candidatePolicy \in [Names -> Policies]
    /\ hostNames \in [Names -> HostObjects]
    /\ isolatedNames \in [Names -> MaybeObjects]
    /\ objectValues \in [Objects -> Payloads]
    /\ capturedHostNames \in [Names -> HostObjects]
    /\ capturedHostValues \in [HostObjects -> Payloads]
    /\ operation \in Operations
    /\ result \in Results
    /\ splitCloneAliases \in BOOLEAN
    /\ mergedCloneObjects \in BOOLEAN
    /\ crossBackingLinked \in BOOLEAN
    /\ linkedRuntimeRenameAdmitted \in BOOLEAN
    /\ unstableAliasCloneAdmitted \in BOOLEAN

Init ==
    /\ phase = "ReadyHost"
    /\ online = TRUE
    /\ candidatePolicy = [name \in Names |-> "Host"]
    /\ hostNames \in [Names -> HostObjects]
    /\ isolatedNames = [name \in Names |-> "None"]
    /\ objectValues \in [Objects -> Payloads]
    /\ capturedHostNames = hostNames
    /\ capturedHostValues = [object \in HostObjects |-> objectValues[object]]
    /\ operation = "None"
    /\ result = "None"
    /\ splitCloneAliases = FALSE
    /\ mergedCloneObjects = FALSE
    /\ crossBackingLinked = FALSE
    /\ linkedRuntimeRenameAdmitted = FALSE
    /\ unstableAliasCloneAdmitted = FALSE

SameBackingLink ==
    /\ online
    /\ phase = "ReadyHost"
    /\ hostNames' = [hostNames EXCEPT !["B"] = hostNames["A"]]
    /\ operation' = "SameBackingLink"
    /\ result' = "Success"
    /\ UNCHANGED <<phase, online, candidatePolicy, isolatedNames, objectValues,
                    capturedHostNames, capturedHostValues, SafetyFlags>>

HostWrite ==
    /\ online
    /\ phase = "ReadyHost"
    /\ \E object \in HostObjects :
        objectValues' = [objectValues EXCEPT ![object] = IF @ = "V1" THEN "V2" ELSE "V1"]
    /\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
                    capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>

BeginClone ==
    /\ online
    /\ phase = "ReadyHost"
    /\ phase' = "Planning"
    /\ candidatePolicy' \in CandidatePolicies
    /\ capturedHostNames' = hostNames
    /\ capturedHostValues' = [object \in HostObjects |-> objectValues[object]]
    /\ operation' = "StartupClone"
    /\ result' = "None"
    /\ UNCHANGED <<online, hostNames, isolatedNames, objectValues, SafetyFlags>>

MutateCapturedAlias ==
    /\ online
    /\ phase = "Planning"
    /\ hostNames' = [hostNames EXCEPT !["B"] = IF @ = "H1" THEN "H2" ELSE "H1"]
    /\ UNCHANGED <<phase, online, candidatePolicy, isolatedNames, objectValues,
                    capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>

MutateCapturedValue ==
    /\ online
    /\ phase = "Planning"
    /\ \E object \in HostObjects :
        objectValues' = [objectValues EXCEPT ![object] = IF @ = "V1" THEN "V2" ELSE "V1"]
    /\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
                    capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>

StableCapture ==
    /\ hostNames = capturedHostNames
    /\ \A object \in HostObjects : objectValues[object] = capturedHostValues[object]

InstallClone ==
    /\ online
    /\ phase = "Planning"
    /\ StableCapture
    /\ phase' = "Installed"
    /\ isolatedNames' = [name \in Names |->
        IF candidatePolicy[name] = "Isolated"
            THEN CloneObject(capturedHostNames[name]) ELSE "None"]
    /\ objectValues' = [objectValues EXCEPT
        !["I1"] = capturedHostValues["H1"],
        !["I2"] = capturedHostValues["H2"]]
    /\ UNCHANGED <<online, candidatePolicy, hostNames, capturedHostNames,
                    capturedHostValues, operation, result, SafetyFlags>>

InstallSplitAliases ==
    /\ Mode = SplitCloneAliases
    /\ online
    /\ phase = "Planning"
    /\ StableCapture
    /\ candidatePolicy["A"] = "Isolated"
    /\ candidatePolicy["B"] = "Isolated"
    /\ capturedHostNames["A"] = capturedHostNames["B"]
    /\ phase' = "Installed"
    /\ isolatedNames' = [name \in Names |-> IF name = "A" THEN "I1" ELSE "I2"]
    /\ splitCloneAliases' = TRUE
    /\ UNCHANGED <<online, candidatePolicy, hostNames, objectValues,
                    capturedHostNames, capturedHostValues, operation, result,
                    mergedCloneObjects, crossBackingLinked,
                    linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>

InstallMergedObjects ==
    /\ Mode = MergeCloneObjects
    /\ online
    /\ phase = "Planning"
    /\ StableCapture
    /\ candidatePolicy["A"] = "Isolated"
    /\ candidatePolicy["B"] = "Isolated"
    /\ capturedHostNames["A"] # capturedHostNames["B"]
    /\ phase' = "Installed"
    /\ isolatedNames' = [name \in Names |-> "I1"]
    /\ mergedCloneObjects' = TRUE
    /\ UNCHANGED <<online, candidatePolicy, hostNames, objectValues,
                    capturedHostNames, capturedHostValues, operation, result,
                    splitCloneAliases, crossBackingLinked,
                    linkedRuntimeRenameAdmitted, unstableAliasCloneAdmitted>>

PublishClone ==
    /\ online
    /\ phase = "Installed"
    /\ StableCapture
    /\ phase' = "ReadyCandidate"
    /\ result' = "Success"
    /\ UNCHANGED <<online, candidatePolicy, hostNames, isolatedNames, objectValues,
                    capturedHostNames, capturedHostValues, operation, SafetyFlags>>

AbortUnstableClone ==
    /\ online
    /\ phase = "Planning"
    /\ ~StableCapture
    /\ phase' = "ReadyHost"
    /\ candidatePolicy' = [name \in Names |-> "Host"]
    /\ isolatedNames' = [name \in Names |-> "None"]
    /\ operation' = "StartupClone"
    /\ result' = "EXDEV"
    /\ UNCHANGED <<online, hostNames, objectValues, capturedHostNames,
                    capturedHostValues, SafetyFlags>>

PublishUnstableAliasClone ==
    /\ Mode = UnstableAliasClone
    /\ online
    /\ phase = "Planning"
    /\ ~StableCapture
    /\ phase' = "ReadyCandidate"
    /\ isolatedNames' = [name \in Names |->
        IF candidatePolicy[name] = "Isolated"
            THEN CloneObject(capturedHostNames[name]) ELSE "None"]
    /\ result' = "Success"
    /\ unstableAliasCloneAdmitted' = TRUE
    /\ UNCHANGED <<online, candidatePolicy, hostNames, objectValues,
                    capturedHostNames, capturedHostValues, operation,
                    splitCloneAliases, mergedCloneObjects, crossBackingLinked,
                    linkedRuntimeRenameAdmitted>>

CrossBackingLinkAttempt ==
    /\ online
    /\ phase = "ReadyCandidate"
    /\ \E hostName, isolatedName \in Names :
        /\ candidatePolicy[hostName] = "Host"
        /\ candidatePolicy[isolatedName] = "Isolated"
    /\ operation' = "CrossBackingLink"
    /\ result' = "EXDEV"
    /\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
                    objectValues, capturedHostNames, capturedHostValues, SafetyFlags>>

AllowCrossBackingLink ==
    /\ Mode = CrossBackingLink
    /\ online
    /\ phase = "ReadyCandidate"
    /\ candidatePolicy["A"] = "Host"
    /\ candidatePolicy["B"] = "Isolated"
    /\ isolatedNames' = [isolatedNames EXCEPT !["B"] = hostNames["A"]]
    /\ operation' = "CrossBackingLink"
    /\ result' = "Success"
    /\ crossBackingLinked' = TRUE
    /\ UNCHANGED <<phase, online, candidatePolicy, hostNames, objectValues,
                    capturedHostNames, capturedHostValues, splitCloneAliases,
                    mergedCloneObjects, linkedRuntimeRenameAdmitted,
                    unstableAliasCloneAdmitted>>

LinkedRuntimeRenameAttempt ==
    /\ online
    /\ phase = "ReadyCandidate"
    /\ candidatePolicy["A"] = "Host"
    /\ candidatePolicy["B"] = "Isolated"
    /\ hostNames["A"] = hostNames["B"]
    /\ operation' = "LinkedRuntimeRename"
    /\ result' = "EXDEV"
    /\ UNCHANGED <<phase, online, candidatePolicy, hostNames, isolatedNames,
                    objectValues, capturedHostNames, capturedHostValues, SafetyFlags>>

AllowLinkedRuntimeRename ==
    /\ Mode = LinkedRuntimeRename
    /\ online
    /\ phase = "ReadyCandidate"
    /\ candidatePolicy["A"] = "Host"
    /\ candidatePolicy["B"] = "Isolated"
    /\ hostNames["A"] = hostNames["B"]
    /\ isolatedNames' = [isolatedNames EXCEPT !["B"] = CloneObject(hostNames["A"])]
    /\ operation' = "LinkedRuntimeRename"
    /\ result' = "Success"
    /\ linkedRuntimeRenameAdmitted' = TRUE
    /\ UNCHANGED <<phase, online, candidatePolicy, hostNames, objectValues,
                    capturedHostNames, capturedHostValues, splitCloneAliases,
                    mergedCloneObjects, crossBackingLinked,
                    unstableAliasCloneAdmitted>>

Crash ==
    /\ online
    /\ phase \in {"Planning", "Installed"}
    /\ online' = FALSE
    /\ UNCHANGED <<phase, candidatePolicy, hostNames, isolatedNames, objectValues,
                    capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>

Recover ==
    /\ ~online
    /\ online' = TRUE
    /\ UNCHANGED <<phase, candidatePolicy, hostNames, isolatedNames, objectValues,
                    capturedHostNames, capturedHostValues, operation, result, SafetyFlags>>

Next == SameBackingLink \/ HostWrite \/ BeginClone \/ MutateCapturedAlias
        \/ MutateCapturedValue \/ InstallClone \/ InstallSplitAliases
        \/ InstallMergedObjects \/ PublishClone \/ AbortUnstableClone
        \/ PublishUnstableAliasClone \/ CrossBackingLinkAttempt
        \/ AllowCrossBackingLink \/ LinkedRuntimeRenameAttempt
        \/ AllowLinkedRuntimeRename \/ Crash \/ Recover

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

ReadyCloneTopology ==
    phase = "ReadyCandidate" =>
        \A left, right \in Names :
            (candidatePolicy[left] = "Isolated" /\ candidatePolicy[right] = "Isolated")
                => ((capturedHostNames[left] = capturedHostNames[right])
                    <=> (isolatedNames[left] = isolatedNames[right]))

ReadyClonePayload ==
    phase = "ReadyCandidate" =>
        \A name \in Names : candidatePolicy[name] = "Isolated" =>
            objectValues[isolatedNames[name]] = capturedHostValues[capturedHostNames[name]]

BackingIdentitySeparated ==
    \A name \in Names : isolatedNames[name] \notin HostObjects

UnchangedHostAtPublication ==
    phase = "ReadyCandidate" =>
        /\ hostNames = capturedHostNames
        /\ \A object \in HostObjects : objectValues[object] = capturedHostValues[object]

NoUnsafeOutcome ==
    /\ ~splitCloneAliases
    /\ ~mergedCloneObjects
    /\ ~crossBackingLinked
    /\ ~linkedRuntimeRenameAdmitted
    /\ ~unstableAliasCloneAdmitted

LinkSafety == ReadyCloneTopology /\ ReadyClonePayload /\ BackingIdentitySeparated
              /\ UnchangedHostAtPublication /\ NoUnsafeOutcome

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