Re: [tlaplus] Re:

[Jay Parlar <par...@xxxxxxxxx>]

On Saturday, 10 February 2018 06:50:36 UTC-5, Pedro Paiva  wrote:
> @ Jay P.: the idea behind /\  \A c \in Clients: LET a == tasks[c].agent is doing an assignment in batches. I have a doubt, however, using existential quantifier \E would not make it possible to leave some task unassigned forever? With \A it checks every task and whether it can be assigned or not. But in fact, it doesn't work properly, for what I intended.

That sound like you're trying to use \A as a "for loop", which isn't correct. Remember that your action has to take a single step. That step might involve your `assigned` and `status` variables changing quite a bit, but you can't explicitly "loop" in your formula to make that happen.

Does this do what you want?

assignAgents ==
    LET toAssign == {a \in Agents : available(a)} IN
      /\ assigned' = assigned \cup toAssign    
      /\ status' = [s \in DOMAIN status |-> IF s \in toAssign THEN "working" ELSE status[s]]
      /\ UNCHANGED <<regAgents, tasks, notifications>>


--
Jay Parlar