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

*From*: groban <grobano@xxxxxxxxx>*Date*: Mon, 10 Jun 2019 12:34:34 -0700 (PDT)*References*: <3c1c1132-b17a-40f4-8503-6d92e8ce13bf@googlegroups.com> <12958B59-6019-4BCF-B751-1C611CBA0545@gmail.com>

Thank you for your prompt answer!

Τη Κυριακή, 9 Ιουνίου 2019 - 7:46:29 μ.μ. UTC+3, ο χρήστης Stephan Merz έγραψε:

-- Yes, the set of uses (U) is known apriori. Unfortunately, I am a little bit confused on how to specify a table (function) that is also a variable in the specification. I will make a try and if I fail, I will probably open another thread!!! :-)

However, do I have any advantage of using a table instead of a set?

Τη Κυριακή, 9 Ιουνίου 2019 - 7:46:29 μ.μ. UTC+3, ο χρήστης Stephan Merz έγραψε:

Hello,your solution is fine – I find it a little simpler to write it asEvaluate == \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 followingEvaluate == \E oid \in OID :/\ obj[oid].status = "started"/\ obj' = [obj EXCEPT ![oid].status =IF Predicate(obj[oid]) THEN "terminated"ELSE "denied"]StephanOn 9 Jun 2019, at 09:33, groban <gro...@xxxxxxxxx> wrote:My specification has a simple variable which is a set of elementsU. Each elementukof the setUis a record with the same number of fields.e.g

u1== [ sid |-> 1, oid |-> 1, status="started"]

Suppose that in one stateUhas the elements{u1, u2, u3}I want to write a step that in the new state variableU’has the same elements as with the previous state with only one difference.A specific element (let’s sayu1) will change in the new state only in one record field (for example fromstatuswill go to=”started”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 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 .

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/c6c28d20-f084-4361-87f3-6c10d54cbef2%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

**References**:**[tlaplus] A problem in expressing a step***From:*groban

**Re: [tlaplus] A problem in expressing a step***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] A problem in expressing a step** - Next by Date:
**Re: [tlaplus] TLC reports error (undefined identifier), but it's defined...** - Previous by thread:
**Re: [tlaplus] A problem in expressing a step** - Next by thread:
**[tlaplus] TLC reports error (undefined identifier), but it's defined...** - Index(es):