u1== [ sid |-> 1, oid |-> 1, status="started"]
termUpdate(x) == [x EXCEPT !.status="terminated"]
denUpdate(x) == [x EXCEPT !.status="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)}} )
On 9 Jun 2019, at 09:33, groban <gro...@gmail.com> 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.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)) THENU' = UNION { (U\{u}) , {termUpdate(u)}}ELSEU' = 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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.