zero downtime TLA+ (using https://github.com/alygin/vscode-tlaplus) (tutorial https://www.hillelwayne.com/post/modeling-deployments/)

zerodt.cfg

SPECIFICATION Spec
\* Add statements after this line.

CONSTANTS
  OUTDATED = "outdated"
  UPDATING = "updating"
  UPDATED = "updated"

INVARIANTS
  SameVersion
  ZeroDowntime
  AllUpdated

zerodt.tla

---- MODULE zerodt ----

EXTENDS TLC, Integers

CONSTANTS OUTDATED, UPDATING, UPDATED

(* --algorithm deploy

  variables
    servers = {"s1", "s2", "s3"},
    load_balancer = servers,
    can_update = [s \in servers |-> FALSE],
    state = [s \in servers |-> OUTDATED];

  define
    SameVersion ==
      \A x, y \in load_balancer:
        state[x] = state[y]
    ZeroDowntime ==
      \E server \in load_balancer:
        state[server] /= UPDATING
    AllUpdated ==
      (\A p \in DOMAIN pc: pc[p] = "Done") => load_balancer = servers
  end define;

  fair process update_server \in servers
  begin
    Update:
      await can_update[self];
      state[self] := UPDATING;
    FinishUpdate:
      state[self] := UPDATED;
  end process;

  fair process start_update = "start_update"
  begin
    StartUpdate:
      load_balancer := {"s1"};
      can_update := [s \in servers |->
        IF s = "s1" THEN FALSE ELSE TRUE];
    Transition:
      await \A s \in (servers \ load_balancer):
        state[s] = UPDATED;
      load_balancer := servers \ load_balancer;
      can_update["s1"] := TRUE;
    Finish:
      await state["s1"] = UPDATED;
      load_balancer := load_balancer \union {"s1"};
  end process;
end algorithm *)
====