Tla Plus, Resilience, Software Development, DevOps.
provisioning_naive ------------------- EXTENDS TLC, Integers, Sequences VMs == {"Server1","Server2","Server3"} (*--algorithm provisioning variables Cluster = [v \in VMs |-> 4], define ServersHealthy == \A vm \in VMs: Cluster[vm] <= 9 end define; end algorithm *)