Re: [tlaplus] Trying to search for a specific entry in each member of a set of sequences

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

you don't give us too many details of your data structure, but I presume that the reqIDs are stored in the entries that WriteResponse creates. For the sake of this answer I'll assume that they are records that contain a field reqID.

You can then write something like

entries(id) ==
  LET
      posInQ(inst, id) == { i \in 1 .. Len(WriteRespQs[inst]) : 
                              WriteRespQs[inst][i].reqID = id }
      entriesInQ(inst, id) == { WriteRespQs[inst][i] : i \in posInQ(inst, id) }
  IN
      UNION { entriesInQ(inst, id) : inst \in Instances }

to obtain the set of all requests for a given id that occur in some queue. (Actually, it may be more useful to return pairs of the queue index and the entry, for example if you want to remove the entry from the queue after handling it.) Of course, you do not have to decompose your definition in this way, this is mainly for readability.

The key is to remember that sequences in TLA+ are just functions whose domain is of the form 1..n, for some natural number n. Alternatively, you could base your definitions on the operator SelectSeq defined in the Sequences module, but usually it's easier to use sets than sequences later on.

Note that I have not actually tried this, so there may be typos in the above definition.

Hope this helps,

Stephan


On Jul 16, 2013, at 6:12 AM, reh...@xxxxxxxxx wrote:

> In CCal, I have a set of sequences
> 
> variables
>        WriteRespQs = [qPerInstance \in Instances |-> <<>>];
> Where I append responses
> macro writeProcess() {
> ...
>        WriteRespQs[self] := Append(WriteRespQs[self], WriteResponse(WriteResp, currentVersion, ResponseFailure, msg.reqID));
> ...
> }
> 
> There is a process for each Instance.
> One the receiver side, I need to look for a secific reqID across all the entire WriteRespQs set.
> 
> What could be an optimal way to do this?
> 
> ---Ritesh
> 
> -- 
> 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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/groups/opt_out.
> 
>