# safety: mutual exclusion
G !(ackA=1 * ackB=1 + ackB=1 * ackC=1 + ackC=1 * ackA=1);

# liveness: 
G(reqA=1 -> F ackA=1);
G(reqB=1 -> F ackB=1);
G(reqC=1 -> F ackC=1);