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