# [tlaplus] A problem in expressing a step

My specification has a simple variable which is a set of elements U. Each element uk of the set U is a record with the same number of fields.
e.g

u1== [ sid |-> 1, oid |-> 1, status="started"]

Suppose that in one state U has the elements {u1, u2, u3}

I want to write a step that in the new state variable U’ has the same elements as with the previous state with only one difference.
A specific element (let’s say u1) will change in the new state only in one record field (for example from status=”started” will go to status=”terminated”)

My current solution is
• extract the specific element set u1 from U and
• re-insert it with the status field changed (with the help of the EXCEPT construct).
A code example is the following (Predicate is checking u other attributes)

termUpdate(x) == [x EXCEPT !.status="terminated"]denUpdate(x) == [x EXCEPT !.st="denied"]Predicate(x) == x.sid =< x.oid  Evaluate == \E u \in U:  (                     /\ u.status="started"                    /\ IF (Predicate(u)) THEN                               U' = UNION { (U\{u}) , {termUpdate(u)}}                         ELSE                             U' = UNION { (U\{u}) , {denUpdate(u)}} )

I want to ask if there is an alternative / better way to specify that?