Tla Plus, Resilience, Software Development, DevOps.
creating a set of every possible combination we no longer need cycles at all. But this change requires us to remove our invariant and replace with something else: define ServersHealthy == <>(\E v \in 1..Len(VMs): VMs[v] <= 9) end define; This is a temporal property it’s defined and configured in