util module

[isaacd...@gmail.com]

Hello,

Thank you for taking time to help!

Let me preface my question with: I have just started learning TLA+. I downloaded the zip 1.6.0 version and started two days ago.

I'm looking at a spec that starts with the statement: EXTENDS Integers, Sequences, util

My first question is what is this util module? Where is it located? TLA+ returns a parsing error due to it...

To naively troubleshoot, I commented it out and apparently it contains Options and the functions SeqToSet, SetToSeq, and MapSeq. I haven't been able to find any information about these functions, though the first two may be more or less obvious, from what I can tell it seems like MapSeq: Record x Seq -> Seq. What I am I missing here?

Any help/suggestions would be greatly appreciated! Thank you!

Best,

Isaac

[Markus Kuppe]

You should ask the author of the spec to send you the util module. A
"util" module is not part of the standard modules or the community
modules [1].

M.

[1] https://github.com/tlaplus/CommunityModules

[Isaac DeFrain]

Thank you for your quick response and helpful suggestion, Markus!

[Isaac DeFrain]

I just wanted to add my conclusion to this thread. Maybe it will be helpful to others.

As Markus correctly stated, there is no "util" module in the standard or community modules. However, there was a workaround using functions from the community modules and a neat hack for options.

My specific problem was that I needed the functions: SeqToSet, SetToSeq, and MapSeq (which maps a function over a seq); and Options.

In the community module SequencesExt, there are functions ToSet: Seq -> Set and SetToSeq: Set -> Seq (the definition of this one is super cool, if you're not familiar with it, check it out).

It was easy enough to define MapSeq. I did this by defining

```

    MapSeq(f(_),s) == [i \in 1..Len(s) |-> f(s[i])]

```

The last thing was to model Option(Data) which I did by defining a CONSTANT None (which I gave a model value) and just modeled Option(Data) as {Data} \cup {None}.

Hopefully this will be of help to someone!

On Sat, Nov 16, 2019 at 9:44 AM Isaac DeFrain <isaacd...@gmail.com> wrote:

Thank you for your quick response and helpful suggestion, Markus!

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/592ba8b3-c3e4-4df9-9d1f-40e453ff7a02%40googlegroups.com.

[Isaac DeFrain]

Of course, I neglected the empty sequence case in my MapSeq definition... In it's full glory:

```

    MapSeq(f(_),s) == IF s = << >> THEN << >> ELSE [i \in 1..Len(s) |-> f(s[i])]

```

Whew! Now I can finally sleep at night ;)

[Stephan Merz]

It should not be necessary to treat the case of the empty sequence separately: in TLA+, sequences are functions, and the function with empty domain is also the empty sequence.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxGw_D%2BwYwx%2Bquo9u9-6khhA1xYS%2BugK6ji84uf7hyTg4w%40mail.gmail.com.

[Isaac DeFrain]

Fantastic! Even better. Thank you.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CF55305D-A844-44E8-939F-AF32D63943E8%40gmail.com.