Filtering set of sequence of records

[Chris Ortiz]

Hi tlaplus,

I am starting to write TLA+ spec with some definitions of filtering set of sequence of records. I have this spec below and I could not get it right where TLC is saying:

Evaluating predicate ...yielded non-Boolean value.

For this expression: { i \in 1..Len(seq): seq[i].ops = o}

I think I understand it is non-Boolean value but how can I get "i" so I can check if the ops match "read" of each of those records in my sequence, minus the empty sequence?

----------------------MODULE WorkLoads------------------------------

EXTENDS Sequences, Naturals

Data == {"a","b"}
LBARange == 0..2

NumIO == 3
IOCommands == [ ops: {"write"}, lba: LBARange, data: Data] \cup [ ops: {"read"}, lba: LBARange ] \* <<>> is considered idle


IOWorkloads == UNION { [1..m -> IOCommands] : m \in 0..NumIO}
ContainOps(S, o) == { seq \in S \ {<<>>}: { i \in 1..Len(seq): seq[i].ops = o}}

OnlyReadWorkloads == ContainOps(IOWorkloads, "read")

-------------------------------------------------------------------------------------------

I appreciate any help and clarification.

Thanks,

Zitro

[Chris Ortiz]

I think I send it too soon. I should have spend more time staring at it. I got it as:

ContainOps(S, o) == { seq \in S \ {<<>>}: \A i \in 1..Len(seq) : seq[i].ops = o}

OnlyReadWorkloads == ContainOps(IOWorkloads, "read")

Thanks,

Zitro