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

*From*: Chris Ortiz <zitroomega@xxxxxxxxx>*Date*: Tue, 31 Oct 2023 14:25:09 -0700 (PDT)*References*: <8984762d-425b-4c7b-a29c-6d94cccd8e70n@googlegroups.com>

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

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

**References**:**[tlaplus] Filtering set of sequence of records***From:*Chris Ortiz

- Prev by Date:
**[tlaplus] Filtering set of sequence of records** - Next by Date:
**Re: [tlaplus] Re: Strategies for scalable modeling of append-only logs** - Previous by thread:
**[tlaplus] Filtering set of sequence of records** - Next by thread:
**[tlaplus] Surjective functions as records** - Index(es):