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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 25 Nov 2020 08:41:55 +0100*References*: <e3a99dad-9df9-48a9-b0ad-c9ba95a25d7dn@googlegroups.com> <E8F7421E-B99E-430C-A393-120CB3F018B8@gmail.com> <ce825f7b-4614-4031-8395-91765f479fe9n@googlegroups.com>

Think of it the other way round: the model that you described in your previous message has two keys and two values (plus a null value when a key is not assigned), so your store has 9 possible values. I'm assuming that the operation that was performed last is not stored in the state (so it doesn't contribute to the number of states) but you may have one or two more variables, for exemple for displaying the result of an operation or for storing the point of control, and these contribute more states. Let's assume that the result variable has 4 possible values (the two values in your store, a "success" for a PUT and an "error" for a GET or DELETE on an unassigned key), then we get 9*4 = 36 possible states. Your spec may be different, but a state graph of 178 distinct states does not sound wrong to me. TLC cannot and does not generate executions one by one: as you say, every execution is of infinite size because of the infinite loop, and there are infinitely many of them because operation calls can be interleaved in arbitrary orders. Instead, it computes the graph of reachable states and explores successors only once per state. As you say there are 12 possible successors for each state, but many of them will loop back to states that TLC has already seen before (e.g., a GET or a DELETE for an unassigned key don't change the state of the store, two PUT operations for two different keys executed in one order or the other lead to the same state etc). So there is no need to actually explore all permutations of all subsets of operations, the only thing that matters is that no reachable state is missed. 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/E92DE534-170B-4D79-B587-6A21FD6D11C5%40gmail.com. |

**Follow-Ups**:

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

**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store***From:*Stephan Merz

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

- Prev by Date:
**[tlaplus] Re: Including TLA+ in a Pandoc paper.** - Next by Date:
**[tlaplus] Conjoining a spec with an invariant** - Previous by thread:
**Re: [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):