Hello,your solution is fine – I find it a little simpler to write it asEvaluate == \E u \in U :                 /\ u.status="started"                 /\ U' = IF Predicate(u) THEN (U\{u}) \cup {termUpdate(u)}                         ELSE (U\{u}) \cup {denUpdate(u)}Using a set of records is most appropriate when your specification handles a set of objects that are not known a priori. If the set of objects is fixed (say, with oid as the key for identifying objects) then you could represent the state of these objects using a table (a TLA+ function) and write your action along the lines of the followingEvaluate == \E oid \in OID :               /\ obj[oid].status = "started"               /\ obj' = [obj EXCEPT ![oid].status =                              IF Predicate(obj[oid]) THEN "terminated"                              ELSE "denied"]StephanOn 9 Jun 2019, at 09:33, groban wrote: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.gu1== [ 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?thanks in advance!  -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3c1c1132-b17a-40f4-8503-6d92e8ce13bf%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/12958B59-6019-4BCF-B751-1C611CBA0545%40gmail.com. For more options, visit https://groups.google.com/d/optout.