[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: 
Seq(S) 

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:

Seq(Nat)


(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.