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?
thanks in advance!