Your formula, somewhat simplified, is \A c \in Client : LET a == tasks[c].agent IN IF available(a) THEN status' = [status EXCEPT ![a] = "working"] ELSE status' = status Suppose that you have two clients c1 and c2, and that the corresponding task agents are distinct, say, a1 and a2. Further assuming that available(a1) holds, this formula implies either [status EXCEPT ![a1] = "working"] = [status EXCEPT ![a2] = "working"] or [status EXCEPT ![a1] = "working"] = status depending on available(a2), and both of these are false [1]. So, the formula is satisfiable only in particular cases, e.g. if both a1 and a2 are unavailable, in which case the action just stutters, or if a1=a2. Your action as you have written it only makes sense if the action updates the status of just one client, hence the existential quantifier. If you want to update the status of several clients, you have to reformulate the entire action using set expressions. Stephan
