Thank you for your quick response and helpful suggestion, Markus!
On Friday, November 15, 2019 at 8:10:42 PM UTC-5, Markus Alexander Kuppe wrote:
On 15.11.19 15:14, isaacd...@xxxxxxxxx wrote:
> 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!
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