[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] A problem in expressing a step

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.

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