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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 24 Nov 2020 08:43:04 +0100*References*: <e3a99dad-9df9-48a9-b0ad-c9ba95a25d7dn@googlegroups.com>

Why don't you just write a loop of the form while (TRUE) { with k \in HashKey, v \in HashValue, op \in ClientOps { call PerformOp(k,v,op) } } TLC will explore all possible sequences of operation calls, for all possible combinations of arguments. Whenever it runs into a state that it has seen before (because the store has the same value for every key), it will stop exploring that branch. The power of model checking is that it lets you explore even infinite executions over finite state spaces. There's no need to materialize the search that TLC will perform in the data structures of your specification. Regards, Stephan
--
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/E8F7421E-B99E-430C-A393-120CB3F018B8%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store***From:*recepient recepient

**References**:**[tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store***From:*recepient recepient

- Prev by Date:
**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS** - Next by Date:
**[tlaplus] TLC error when choosing an arbitrary value** - Previous by thread:
**[tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Next by thread:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Index(es):