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

[tlaplus] How can I define a sequence as part of a record's fields?

From Specifying Systems, I read in section 4.1 that:
"The Sequences module defines the following operators on sequences: 

The set of all sequences of elements of the set S. For example, h3, 7i is an element of Seq(Nat)."

I thought then that I could have a sequence as a field of a record by doing:
MyRec == [
    id: recs,
    seek: Seq(Nat)

but it doesn't work, stating:

Attempted to enumerate a set of the form [l1 : v1, ..., ln : vn],

but can't enumerate the value of the 'seek' field:


(Eventually, I'd like to initialize this record's seek field to be <<>> in the init state, and then use it to track ordered operations.)

I am very new to TLA+, any help would be so appreciated.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4351c96e-420c-40f5-b5b4-5ed42fa131dcn%40googlegroups.com.