Tla Plus, Resilience, Software Development, DevOps.
{"Server1","Server2","Server3"} Incidents(set) == set \X set \X set \X set Events == [target: VMs, size: 0..4] (*--algorithm provisioning variables incident \in Incidents(Events), Cluster = [v \in VMs |-> 4], curr = ""; \* helper: current event define ServersHealthy == \A vm \in VMs: Cluster[vm] <=