Hello,
your solution is fine – I find it a little simpler to write it as
Evaluate == \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 following
Evaluate == \E oid \in OID :
/\ obj[oid].status = "started"
/\ obj' = [obj EXCEPT ![oid].status =
IF Predicate(obj[oid]) THEN "terminated"
ELSE "denied"]
Stephan
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!
--
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
tla...@googlegroups.com.
To post to this group, send email to
tla...@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.