141 lines
6.6 KiB
Text
141 lines
6.6 KiB
Text
---- MODULE Runtime ----
|
|
EXTENDS Naturals, FiniteSets
|
|
|
|
\* Incumbent-owner projection of e063bc9 run.go/parameters.yaml, after successful setup and claim.
|
|
\* Probe/endpoint convergence is asynchronous; shutdown here is graceful, unlike Lease.tla.
|
|
CONSTANTS Fixed, PublishUnready, Scenario
|
|
ASSUME Fixed \in BOOLEAN /\ PublishUnready \in BOOLEAN /\ Scenario \in {"health", "ports", "proxy", "outage"}
|
|
|
|
Heads == {0, 1}
|
|
None == 2
|
|
VARIABLES stage, daemon, configured, label, sas, sample, route, flag,
|
|
observedHealthy, reported, podReady, endpoint, proxy,
|
|
ports, appliedPorts, portRestart, lost, reachable
|
|
vars == <<stage, daemon, configured, label, sas, sample, route, flag,
|
|
observedHealthy, reported, podReady, endpoint, proxy,
|
|
ports, appliedPorts, portRestart, lost, reachable>>
|
|
|
|
TypeOK ==
|
|
/\ stage \in {"Load", "Scan", "Route", "Report", "Idle", "Stop"}
|
|
/\ sas \subseteq Heads /\ sample \subseteq Heads
|
|
/\ route \in Heads \cup {None}
|
|
/\ ports \in 0..1 /\ appliedPorts \in 0..1
|
|
/\ \A value \in {daemon, configured, label, flag, observedHealthy,
|
|
reported, podReady, endpoint, proxy, portRestart, lost, reachable} : value \in BOOLEAN
|
|
|
|
Init ==
|
|
/\ stage = "Load" /\ daemon = FALSE /\ configured = FALSE /\ label = FALSE
|
|
/\ sas = {} /\ sample = {} /\ route = None /\ flag = FALSE
|
|
/\ observedHealthy = FALSE /\ reported = FALSE
|
|
/\ podReady = FALSE /\ endpoint = FALSE /\ proxy = TRUE
|
|
/\ ports = 0 /\ appliedPorts = 0 /\ portRestart = FALSE /\ lost = FALSE /\ reachable = TRUE
|
|
|
|
Load ==
|
|
/\ stage = "Load"
|
|
/\ daemon' = TRUE /\ configured' = TRUE /\ label' = TRUE
|
|
/\ stage' = "Scan" /\ appliedPorts' = ports /\ flag' = FALSE
|
|
/\ UNCHANGED <<sas, sample, route, observedHealthy, reported, podReady,
|
|
endpoint, proxy, ports, portRestart, lost, reachable>>
|
|
|
|
Scan ==
|
|
/\ stage = "Scan" /\ daemon
|
|
/\ sample' = sas /\ stage' = "Route"
|
|
/\ UNCHANGED <<daemon, configured, label, sas, route, flag, observedHealthy,
|
|
reported, podReady, endpoint, proxy, ports, appliedPorts, portRestart, lost, reachable>>
|
|
|
|
Route ==
|
|
/\ stage = "Route"
|
|
/\ route' = IF sample = {} THEN route ELSE IF 0 \in sample THEN 0 ELSE 1
|
|
/\ stage' = "Report"
|
|
/\ UNCHANGED <<daemon, configured, label, sas, sample, flag, observedHealthy,
|
|
reported, podReady, endpoint, proxy, ports, appliedPorts, portRestart, lost, reachable>>
|
|
|
|
Report ==
|
|
/\ stage = "Report"
|
|
/\ flag' = IF Fixed THEN sample /= {} ELSE TRUE
|
|
/\ observedHealthy' = (sample /= {} /\ route \in sample)
|
|
/\ reported' = TRUE /\ stage' = "Idle"
|
|
/\ UNCHANGED <<daemon, configured, label, sas, sample, route, podReady,
|
|
endpoint, proxy, ports, appliedPorts, portRestart, lost, reachable>>
|
|
|
|
Poll ==
|
|
/\ stage = "Idle" /\ ports = appliedPorts
|
|
/\ stage' = "Scan"
|
|
/\ UNCHANGED <<daemon, configured, label, sas, sample, route, flag, observedHealthy,
|
|
reported, podReady, endpoint, proxy, ports, appliedPorts, portRestart, lost, reachable>>
|
|
|
|
ChangePorts ==
|
|
/\ Scenario = "ports" /\ ports = 0 /\ stage = "Idle" /\ daemon
|
|
/\ sas /= {} /\ route \in sas
|
|
/\ ports' = 1
|
|
/\ UNCHANGED <<stage, daemon, configured, label, sas, sample, route, flag,
|
|
observedHealthy, reported, podReady, endpoint, proxy, appliedPorts,
|
|
portRestart, lost, reachable>>
|
|
|
|
Reload ==
|
|
/\ stage = "Idle" /\ ports /= appliedPorts
|
|
/\ stage' = IF Fixed THEN "Scan" ELSE "Stop"
|
|
/\ appliedPorts' = IF Fixed THEN ports ELSE appliedPorts
|
|
/\ UNCHANGED <<daemon, configured, label, sas, sample, route, flag, observedHealthy,
|
|
reported, podReady, endpoint, proxy, ports, portRestart, lost, reachable>>
|
|
|
|
Stop ==
|
|
/\ stage = "Stop"
|
|
/\ daemon' = FALSE /\ sas' = {} /\ flag' = FALSE /\ stage' = "Load"
|
|
/\ portRestart' = (portRestart \/ (daemon /\ ports /= appliedPorts))
|
|
/\ UNCHANGED <<configured, label, sample, route, observedHealthy, reported,
|
|
podReady, endpoint, proxy, ports, appliedPorts, lost, reachable>>
|
|
|
|
Probe ==
|
|
LET desired == configured /\ flag /\ (Fixed \/ proxy)
|
|
IN /\ podReady /= desired /\ podReady' = desired
|
|
/\ UNCHANGED <<stage, daemon, configured, label, sas, sample, route, flag,
|
|
observedHealthy, reported, endpoint, proxy, ports, appliedPorts,
|
|
portRestart, lost, reachable>>
|
|
|
|
\* Publishing the active endpoint before serving readiness breaks the initial IKE dependency cycle.
|
|
Realize ==
|
|
LET desired == label /\ (PublishUnready \/ podReady)
|
|
IN /\ endpoint /= desired /\ endpoint' = desired
|
|
/\ UNCHANGED <<stage, daemon, configured, label, sas, sample, route, flag,
|
|
observedHealthy, reported, podReady, proxy, ports, appliedPorts,
|
|
portRestart, lost, reachable>>
|
|
|
|
Negotiate ==
|
|
/\ daemon /\ configured /\ endpoint /\ reachable /\ sas /= Heads
|
|
/\ sas' \in SUBSET Heads /\ sas \subseteq sas' /\ sas' /= sas
|
|
/\ UNCHANGED <<stage, daemon, configured, label, sample, route, flag, observedHealthy,
|
|
reported, podReady, endpoint, proxy, ports, appliedPorts, portRestart, lost, reachable>>
|
|
|
|
LosePeers ==
|
|
/\ ~lost /\ sas = Heads
|
|
/\ IF Scenario = "outage" THEN sas' = {} ELSE sas' \in (SUBSET Heads) \ {Heads}
|
|
/\ lost' = TRUE
|
|
/\ reachable' = (Scenario /= "outage")
|
|
/\ UNCHANGED <<stage, daemon, configured, label, sample, route, flag, observedHealthy,
|
|
reported, podReady, endpoint, proxy, ports, appliedPorts, portRestart>>
|
|
|
|
ProxyFails ==
|
|
/\ Scenario = "proxy" /\ proxy /\ podReady /\ endpoint
|
|
/\ sas /= {} /\ route \in sas
|
|
/\ proxy' = FALSE
|
|
/\ UNCHANGED <<stage, daemon, configured, label, sas, sample, route, flag,
|
|
observedHealthy, reported, podReady, endpoint, ports, appliedPorts,
|
|
portRestart, lost, reachable>>
|
|
|
|
Next == Load \/ Scan \/ Route \/ Report \/ Poll \/ ChangePorts \/ Reload \/ Stop
|
|
\/ Probe \/ Realize \/ Negotiate \/ LosePeers \/ ProxyFails
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
/\ WF_vars(Load) /\ WF_vars(Scan) /\ WF_vars(Route) /\ WF_vars(Report)
|
|
/\ WF_vars(Poll) /\ WF_vars(Reload) /\ WF_vars(Stop)
|
|
/\ WF_vars(Probe) /\ WF_vars(Realize) /\ WF_vars(Negotiate)
|
|
/\ SF_vars(ChangePorts) /\ SF_vars(ProxyFails) /\ SF_vars(LosePeers)
|
|
|
|
HealthyObservation == reported => (~flag \/ observedHealthy)
|
|
PortContinuity == ~portRestart
|
|
TransportRecovery == <>[]endpoint
|
|
Usable == daemon /\ endpoint /\ sas /= {} /\ route \in sas /\ ports = appliedPorts
|
|
ServingRecovery == (<>[]reachable) => <>[]Usable
|
|
LossReported == (<>[]~reachable) => <>[](~flag /\ ~podReady)
|
|
====
|