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

-------------------------------- MODULE mre --------------------------------

EXTENDS Sequences

CONSTANTS ID

VARIABLES recs

MyRec == [

id: ID, \* ID == {1,2,3}

seek: <<>>

]

ShouldBeTrue(m) ==

/\ m.id \in ID \*should be trivially true bc of record definition?

/\ m.seek = <<>> \*I want this to be "initialized" to an empty sequence

Init ==

/\ recs = {m \in MyRec: ShouldBeTrue(m)}

Next ==

\/ \E rec \in recs:

rec' = [rec EXCEPT !.seek = Append(@, "value")] \* Add to queue

\/ \E rec \in recs:

rec' = [rec EXCEPT !.seek = SubSeq(@, 2, Len(@))] \* Pop the head off

Spec == Init /\ [][Next]_recs

=============================================================================

On Thursday, December 1, 2022 at 1:51:27 AM UTC-5 Stephan Merz wrote:

Your definition is perfectly fine: it defines a set of records with two fields, the second of which is a sequence. However, as the error message indicates, TLC cannot evaluate this operator because the set of these records is infinite (it may contain sequences of arbitrary length). Whether this is a problem or not depends on how you intend to use the operator:

- If it only appears in an invariant, say you write "rec \in MyRec" to check that some variable always takes values in this set, then TLC will be able to evaluate this predicate (it doesn't have to enumerate the entire set MyRec to do so).

- If it appears in the definition of the transition system, say your initial condition has a conjunct "rec \in MyRec" or your next-state relation contains "rec' \in MyRec" then indeed your state space can be infinite because the variable can take an arbitrary value in an infinite set, and TLC will not be able to generate the state space. In that case, you can override the definition of MyRec for TLC and restrict the allowed sequences to a finite set (restricting to fixed maximal length), and check a finite subset of the state space. See the corresponding help pages in the Toolbox.

From what you write, it appears that you'll initialize the variable deterministically, so you'll write something like

Init == rec = [id |-> someValue, seek |-> << >>]

and in that case everything should work fine: MyRec will probably only appear in a (typing) invariant.

Regards,
Stephan

On 1 Dec 2022, at 04:27, Alan Munirji <munir...@xxxxxxxxx> wrote:

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