------------------------------- MODULE Cloud -------------------------------
EXTENDS Naturals, FiniteSets, TLC

CONSTANTS Mode, Scenario, ResourceKind, LoseReply, RestartOnce, DelayLists

(* This projection separates OCI resource state, API observations, and publication. *)
(* cloud.Client.Reconcile supplies the create/select/cleanup protocol for each kind. *)

Kinds == {"CPE", "VPN"}
Modes == {"Current", "Fixed"}
Cases == {"Retry", "Routes"}
Ids == 1..3
WANs == {"A", "B"}
VIPs == {"X", "Y"}
Attempts == 0..2
Keys == WANs \X Attempts
Lives == {"Unused", "Provisioning", "Available", "Terminating", "Terminated", "Absent"}
Phases == {"read", "create", "reply", "inspect", "clean", "admit", "publish", "pause"}

ASSUME /\ Mode \in Modes
       /\ Scenario \in Cases
       /\ ResourceKind \in Kinds
       /\ Scenario = "Routes" => ResourceKind = "VPN"
       /\ LoseReply \in BOOLEAN
       /\ RestartOnce \in BOOLEAN
       /\ DelayLists \in BOOLEAN

VARIABLES objects, visible, tokens, invalid, issued, nextId, epoch,
          phase, seen, selected, attempt, reply, routeSeen, pending,
          health, published, admitted, todo, refs, dropped, restarted, badPublish

vars == <<objects, visible, tokens, invalid, issued, nextId, epoch,
          phase, seen, selected, attempt, reply, routeSeen, pending,
          health, published, admitted, todo, refs, dropped, restarted, badPublish>>

LastEpoch == IF Scenario = "Retry" THEN 2 ELSE 1
WAN == IF Scenario = "Retry" /\ epoch = 1 THEN "B" ELSE "A"
VIP == IF Scenario = "Routes" /\ epoch = 1 THEN "Y" ELSE "X"
Key == <<WAN, attempt>>
Active == {i \in Ids : objects[i].life \in {"Provisioning", "Available"}}
Present == {i \in Ids : objects[i].life \notin {"Unused", "Absent"}}
Current == {i \in seen : objects[i].wan = WAN /\
            (ResourceKind = "CPE" \/
             objects[i].life \notin {"Terminating", "Terminated", "Absent"})}
Old == {i \in seen : i # selected}

Init == /\ objects = [i \in Ids |-> [life |-> "Unused", wan |-> "A", route |-> "X"]]
        /\ visible = {}
        /\ tokens = [k \in Keys |-> 0]
        /\ invalid = {}
        /\ issued = {}
        /\ nextId = 1
        /\ epoch = 0
        /\ phase = "read"
        /\ seen = {}
        /\ selected = 0
        /\ attempt = 0
        /\ reply = 0
        /\ routeSeen = "X"
        /\ pending = [i \in Ids |-> "None"]
        /\ health = {}
        /\ published = [epoch |-> 3, id |-> 0, route |-> "X"]
        /\ admitted = {}
        /\ todo = {}
        /\ refs = {}
        /\ dropped = FALSE
        /\ restarted = FALSE
        /\ badPublish = FALSE

(* cloud.Client.Reconcile lists before selecting a CPE or a non-terminating VPN. *)
Read == /\ phase = "read"
        /\ seen' = visible
        /\ phase' = "inspect"
        /\ selected' = 0
        /\ attempt' = 0
        /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                       reply, routeSeen, pending, health, published, admitted, todo,
                       refs, dropped, restarted, badPublish>>

Select == /\ phase = "inspect" /\ selected = 0
          /\ IF Cardinality(Current) = 1
                THEN /\ selected' = CHOOSE i \in Current : TRUE
                     /\ routeSeen' = objects[selected'].route
                     /\ phase' = "inspect"
                ELSE /\ selected' = 0
                     /\ UNCHANGED routeSeen
                     /\ phase' = IF Current = {} THEN "create" ELSE "pause"
          /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                         seen, attempt, reply, pending, health, published, admitted,
                         todo, refs, dropped, restarted, badPublish>>

(* OCI Retry Token and InvalidatedRetryToken define these three create outcomes. *)
(* https://docs.oracle.com/en-us/iaas/Content/API/References/apierrors.htm *)
Create == /\ phase = "create"
          /\ Key \notin invalid
          /\ tokens[Key] = 0
          /\ nextId \in Ids
          /\ objects' = [objects EXCEPT ![nextId] =
                           [life |-> IF ResourceKind = "VPN" THEN "Provisioning" ELSE "Available",
                            wan |-> WAN, route |-> VIP]]
          /\ tokens' = [tokens EXCEPT ![Key] = nextId]
          /\ issued' = issued \cup {<<Key, nextId>>}
          /\ reply' = nextId
          /\ nextId' = nextId + 1
          /\ visible' = IF DelayLists THEN visible ELSE visible \cup {nextId}
          /\ phase' = "reply"
          /\ UNCHANGED <<invalid, epoch, seen, selected, attempt, routeSeen, pending,
                         health, published, admitted, todo, refs, dropped,
                         restarted, badPublish>>

Replay == /\ phase = "create" /\ Key \notin invalid /\ tokens[Key] # 0
          /\ reply' = tokens[Key]
          /\ phase' = "reply"
          /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                         seen, selected, attempt, routeSeen, pending, health,
                         published, admitted, todo, refs, dropped, restarted, badPublish>>

(* Fixed follows a deterministic successor only on InvalidatedRetryToken; restart replays that chain. *)
Reject == /\ phase = "create" /\ Key \in invalid
          /\ IF Mode = "Fixed" /\ attempt < 2
                THEN /\ attempt' = attempt + 1 /\ phase' = "create"
                ELSE /\ UNCHANGED attempt /\ phase' = "pause"
          /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                         seen, selected, reply, routeSeen, pending, health, published,
                         admitted, todo, refs, dropped, restarted, badPublish>>

Receive == /\ phase = "reply"
           /\ selected' = reply
           /\ routeSeen' = objects[reply].route
           /\ seen' = seen \cup {reply}
           /\ phase' = "inspect"
           /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                          attempt, reply, pending, health, published, admitted, todo,
                          refs, dropped, restarted, badPublish>>

(* A timed-out create may already have committed; only its response is lost. *)
DropReply == /\ LoseReply /\ ~dropped /\ phase = "reply"
             /\ dropped' = TRUE
             /\ phase' = "read"
             /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                            seen, selected, attempt, reply, routeSeen, pending, health,
                            published, admitted, todo, refs, restarted, badPublish>>

Restart == /\ RestartOnce /\ ~restarted
           /\ restarted' = TRUE
           /\ phase' = "read"
           /\ selected' = 0
           /\ attempt' = 0
           /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                          seen, reply, routeSeen, pending, health, published, admitted,
                          todo, refs, dropped, badPublish>>

(* UpdateIPSecConnectionDetails.StaticRoutes replaces the managed route set. *)
UpdateRoute == /\ phase = "inspect" /\ selected # 0
               /\ objects[selected].life = "Available"
               /\ ResourceKind = "VPN" /\ Mode = "Fixed" /\ routeSeen # VIP
               /\ pending' = [pending EXCEPT ![selected] = VIP]
               /\ phase' = "pause"
               /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId,
                              epoch, seen, selected, attempt, reply, routeSeen, health,
                              published, admitted, todo, refs, dropped, restarted, badPublish>>

(* CPE unavailability here represents a rejected child-IPsec call, not a readable CPE lifecycle. *)
WaitReady == /\ phase = "inspect" /\ selected # 0
             /\ objects[selected].life # "Available"
             /\ phase' = "pause"
             /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                            seen, selected, attempt, reply, routeSeen, pending, health,
                            published, admitted, todo, refs, dropped, restarted, badPublish>>

BeginClean == /\ phase = "inspect" /\ selected # 0
              /\ objects[selected].life = "Available"
              /\ ResourceKind = "CPE" \/ Mode = "Current" \/ routeSeen = VIP
              /\ todo' = IF selected \in health THEN Old ELSE {}
              /\ phase' = "clean"
              /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                             seen, selected, attempt, reply, routeSeen, pending, health,
                             published, admitted, refs, dropped, restarted, badPublish>>

(* CPE disposal follows child-IPsec retirement; this abstracts that completed subprotocol. *)
RetireChild(i) == /\ ResourceKind = "CPE" /\ phase = "clean" /\ i \in todo /\ i \in refs
                 /\ refs' = refs \ {i}
                 /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId,
                                epoch, phase, seen, selected, attempt, reply, routeSeen,
                                pending, health, published, admitted, todo, dropped,
                                restarted, badPublish>>

Delete(i) == /\ phase = "clean" /\ i \in todo /\ i \notin refs
             /\ objects' = IF i \in Active
                              THEN [objects EXCEPT ![i].life = "Terminating"]
                              ELSE objects
             /\ todo' = todo \ {i}
             /\ health' = health \ {i}
             /\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch, phase,
                            seen, selected, attempt, reply, routeSeen, pending,
                            published, admitted, refs, dropped, restarted, badPublish>>

CleanDone == /\ phase = "clean" /\ todo = {}
             /\ phase' = "admit"
             /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                            seen, selected, attempt, reply, routeSeen, pending, health,
                            published, admitted, todo, refs, dropped, restarted, badPublish>>

Admit == /\ phase = "admit"
         /\ admitted' = {i \in seen : objects[i].life = "Available"}
         /\ phase' = "publish"
         /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                        seen, selected, attempt, reply, routeSeen, pending, health,
                        published, todo, refs, dropped, restarted, badPublish>>

(* controller.Runner.step publishes after admission and two retrievable peer configurations. *)
Publish == /\ phase = "publish"
           /\ published' = [epoch |-> epoch, id |-> selected, route |-> VIP]
           /\ badPublish' = (badPublish \/ (ResourceKind = "VPN" /\ routeSeen # VIP))
           /\ refs' = IF ResourceKind = "CPE" THEN refs \cup {selected} ELSE refs
           /\ phase' = "pause"
           /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                          seen, selected, attempt, reply, routeSeen, pending, health,
                          admitted, todo, dropped, restarted>>

Poll == /\ phase = "pause" /\ phase' = "read"
        /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
                       seen, selected, attempt, reply, routeSeen, pending, health,
                       published, admitted, todo, refs, dropped, restarted, badPublish>>

Provision(i) == /\ objects[i].life = "Provisioning"
                /\ objects' = [objects EXCEPT ![i].life = "Available"]
                /\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch,
                               phase, seen, selected, attempt, reply, routeSeen, pending,
                               health, published, admitted, todo, refs, dropped,
                               restarted, badPublish>>

Expose(i) == /\ i \in Present /\ i \notin visible
             /\ visible' = visible \cup {i}
             /\ UNCHANGED <<objects, tokens, invalid, issued, nextId, epoch, phase,
                            seen, selected, attempt, reply, routeSeen, pending, health,
                            published, admitted, todo, refs, dropped, restarted, badPublish>>

Finish(i) == /\ objects[i].life = "Terminating"
             /\ objects' = [objects EXCEPT ![i].life =
                              IF ResourceKind = "VPN" THEN "Terminated" ELSE "Absent"]
             /\ invalid' = invalid \cup {k \in Keys : tokens[k] = i}
             /\ UNCHANGED <<visible, tokens, issued, nextId, epoch, phase, seen,
                            selected, attempt, reply, routeSeen, pending, health,
                            published, admitted, todo, refs, dropped, restarted, badPublish>>

Purge(i) == /\ objects[i].life = "Terminated"
            /\ objects' = [objects EXCEPT ![i].life = "Absent"]
            /\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch, phase,
                           seen, selected, attempt, reply, routeSeen, pending, health,
                           published, admitted, todo, refs, dropped, restarted, badPublish>>

Forget(i) == /\ objects[i].life = "Absent" /\ i \in visible
             /\ visible' = visible \ {i}
             /\ UNCHANGED <<objects, tokens, invalid, issued, nextId, epoch, phase,
                            seen, selected, attempt, reply, routeSeen, pending, health,
                            published, admitted, todo, refs, dropped, restarted, badPublish>>

ApplyRoute(i) == /\ pending[i] \in VIPs /\ objects[i].life = "Available"
                 /\ objects' = [objects EXCEPT ![i].route = pending[i]]
                 /\ pending' = [pending EXCEPT ![i] = "None"]
                 /\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch,
                                phase, seen, selected, attempt, reply, routeSeen,
                                health, published, admitted, todo, refs, dropped,
                                restarted, badPublish>>

(* health denotes both associated IPsec tunnels being up; CPE itself has no health field. *)
Establish(i) == /\ published.id = i /\ objects[i].life = "Available"
                /\ objects[i].wan = WAN /\ i \notin health
                /\ health' = health \cup {i}
                /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId,
                               epoch, phase, seen, selected, attempt, reply, routeSeen,
                               pending, published, admitted, todo, refs, dropped,
                               restarted, badPublish>>

Converged == /\ published.epoch = epoch /\ published.id \in health
             /\ objects[published.id].wan = WAN
             /\ ResourceKind = "CPE" \/ objects[published.id].route = VIP

Advance == /\ epoch < LastEpoch /\ phase = "pause" /\ Converged
           /\ \A i \in Ids : i = published.id \/ objects[i].life \in {"Unused", "Absent"}
           /\ visible = {published.id}
           /\ epoch' = epoch + 1
           /\ health' = {}
           /\ phase' = "read"
           /\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, seen,
                          selected, attempt, reply, routeSeen, pending, published,
                          admitted, todo, refs, dropped, restarted, badPublish>>

Work == Read \/ Select \/ Create \/ Replay \/ Reject \/ Receive \/ UpdateRoute \/
        WaitReady \/ BeginClean \/ CleanDone \/ Admit \/ Publish \/ Poll \/
        (\E i \in Ids : RetireChild(i) \/ Delete(i))

Provider(i) == Provision(i) \/ Expose(i) \/ Finish(i) \/ Purge(i) \/ Forget(i) \/
               ApplyRoute(i) \/ Establish(i)

Next == Work \/ Advance \/ DropReply \/ Restart \/ (\E i \in Ids : Provider(i))

(* Liveness assumes a stable final target and eventual API visibility, provisioning, and tunnel progress. *)
Fairness == /\ WF_vars(Work)
            /\ SF_vars(Advance)
            /\ \A i \in Ids : /\ WF_vars(Provision(i)) /\ WF_vars(Expose(i))
                              /\ WF_vars(Finish(i)) /\ WF_vars(Purge(i))
                              /\ WF_vars(Forget(i)) /\ WF_vars(ApplyRoute(i))
                              /\ WF_vars(Establish(i))

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

TypeOK == /\ objects \in [Ids -> [life : Lives, wan : WANs, route : VIPs]]
          /\ visible \subseteq Ids /\ seen \subseteq Ids
          /\ tokens \in [Keys -> (Ids \cup {0})] /\ invalid \subseteq Keys
          /\ issued \subseteq (Keys \X Ids) /\ nextId \in 1..4
          /\ epoch \in 0..LastEpoch /\ phase \in Phases
          /\ selected \in Ids \cup {0} /\ reply \in Ids \cup {0}
          /\ attempt \in Attempts /\ routeSeen \in VIPs
          /\ pending \in [Ids -> VIPs \cup {"None"}]
          /\ health \subseteq Ids /\ admitted \subseteq Ids
          /\ todo \subseteq Ids /\ refs \subseteq Ids
          /\ published \in [epoch : 0..3, id : Ids \cup {0}, route : VIPs]
          /\ dropped \in BOOLEAN /\ restarted \in BOOLEAN /\ badPublish \in BOOLEAN

(* OCI Retry Token guarantees expire after 24 hours; expiry is outside this projection. *)
(* https://docs.oracle.com/en-us/iaas/Content/API/Concepts/usingapi.htm *)
OCIRetry == \A a, b \in issued : a[1] = b[1] => a[2] = b[2]
(* DeleteCpe requires the CPE to be disconnected from its DRG. *)
(* https://docs.oracle.com/en-us/iaas/tools/python/latest/api/core/client/oci.core.VirtualNetworkClient.html#oci.core.VirtualNetworkClient.delete_cpe *)
OCIDelete == \A i \in refs : objects[i].life \notin {"Terminating", "Terminated", "Absent"}
OCITokens == \A k \in invalid : tokens[k] # 0

RoutePublish == ~badPublish
Admission == phase = "publish" => selected \in admitted
Recovery == <>[](epoch = LastEpoch /\ Converged)
=============================================================================