Re:

[par...@xxxxxxxxx]

If you enable Deadlock checking, you'll see that the system deadlocks after a `CRequest` has taken place.

For a `CReply` to take place, this enabling condition must be true:

    /\ status[tasks[c].agent] \in {"ok", "error"}

Looking at where you set to values for `status`, it happens in `assignAgents`

The problem is in your first enabling condition in that action. You have:

    /\	\A c \in Clients: LET a == tasks[c].agent 

But I think you meant that to be `\E c \in Clients: ...`

When I changed it to use \E instead of \A, the model checker performed "as expected".

I hope this helps!

Jay P.