Tla Plus, Resilience, Software Development, DevOps.
MODULE provisioning_autoscale ------------------- EXTENDS TLC, Integers, Sequences (*--algorithm provisioning variables VMs \in [1..2 -> 0..10] define ServersHealthy == <>(\E v \in 1..Len(VMs): VMs[v] <= 9) end define; fair process VM_dies = "kill a VM" begin Fail: await Len(VMs) > 1; VMs :=