Re: [tlaplus] How do I extract particular mapping from each element in a set?

Got it.Thanks!

On Wednesday, April 3, 2019 at 5:45:28 AM UTC-4, Stephan Merz wrote:

Not sure I understand correctly what you are after but how about the following (assuming that all `value' [or `val'?] fields indeed hold pairs):

get(t) ==
LET filtered == {el \in elements : el.key > t}
IN {el.value : el \in filtered}

TLA+ offers two forms of set comprehension (generalized to several variables):

{ x \in S : P(x) } computes the subset of S whose elements satisfy the predicate P
{ f(x) : x \in S } yields the result of applying f to all elements of S (analogous to map in functional programming)

The set _expression_ in your original definition of get matches neither of these forms.

Stephan

On 2 Apr 2019, at 22:53, Balaji Arun <ba2...@xxxxxx> wrote:

I have a set of functions, and I want to extract a particular mapping from each element in the set. I tried the following, but dint work.

get(t) == {<<x, y>>: \A element \in elements: element.key > t => <<x, y>> \in element.value}

I get a syntax error at \A. So, I tried to split them as:

get1(t) == {element \in elements: element.key > t} get2(t) == {element.value : element \in get1(t)} get3(t) == {val : val \in get2(t)} get4(t) == {<<x, y>> : <<x, y>> \in val}

and combined it into:

committed(t) == {<<x, y>> : <<x, y>> \in {val : val \in {element.val : element \in {element \in elements: element.key > t}}}}

Is this correct? Can this be simplified further?

Thanks!

--
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.
For more options, visit https://groups.google.com/d/optout.