[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Filtering set of sequence of records

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")


On Tuesday, October 31, 2023 at 2:16:13 PM UTC-7 Chris Ortiz wrote:
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.


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/265395a3-2417-4fd3-9ad7-741b02a61e16n%40googlegroups.com.