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 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.
|