[tlaplus] Filtering set of records

[Chris Ortiz <zitroomega@xxxxxxxxx>]

Hi tlaplus,

I am starting to write TLA+ spec with some definitions of filtering set 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

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cec40aeb-21ad-4fcd-8de9-b9ba2019185bn%40googlegroups.com.