How to model a composite trace?

[mt40]

A composite trace in my case is a sequence of "write request", each entry is:

{
  key: str,
  value: str,
  time: int
}

I tried to use List and Record to represent this but seems not possible because Record requires specifying value so I cannot write List[Record].

List and Tuple is another choice but then it's very hard to remember what field does Tuple._1 maps to.

Is it possible to do in Quint? Or am I going in the wrong direction. Please let me know your ideas.

Thanks!

[bugarela]

Hi! I don't think I understand what you mean by "composite trace". You can specify a state variable with type "list of write requests" by writing:

var writeRequests: List[{ key: str, value: str, time: int }]

Moreover, you can also create a type alias for the write request and use it in the type:

type WriteRequest = { key: str, value: str, time: int }

var writeRequests: List[WriteRequest]

Does this help with what you are trying to achieve?

[mt40]

Wait what, I can write type WriteRequest = { key: str, value: str, time: int }. ooh... this solves everything. Exactly the kind of goodness expected from Quint.
Thanks @bugarela this solves my case.

Btw, a "composite trace" is just a theory term for a sequence of state changes. You can see from my example this is a sequence of global read/write. This idea is 1 of a way to model consistency.

Let's use the extreme Linearizability Consistency as example, there can be only 1 such "composite trace" because all nodes agree on all read/write all the time. Any read at position i on the trace must return the latest write in the trace with position less than i.