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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 25 Nov 2020 19:23:35 +0100*References*: <e3a99dad-9df9-48a9-b0ad-c9ba95a25d7dn@googlegroups.com> <E8F7421E-B99E-430C-A393-120CB3F018B8@gmail.com> <ce825f7b-4614-4031-8395-91765f479fe9n@googlegroups.com> <E92DE534-170B-4D79-B587-6A21FD6D11C5@gmail.com> <CAPz6axO+X6O83z6d6Nj9JZ+O-_6eKzugEa+cyxGihHQHrrqHZw@mail.gmail.com>

TLC explores all successors of every state it analyzes. The algorithm for checking invariants can be given as follows: queue = [s : s is an initial state of the spec] \* queue of states to explore visited = [] \* set of states already visited while queue != [] : s = head(queue) queue = tail(queue) if ~(s in visited) : visited += [s] if ~(s satisfies invariant) : return false \* compute and display counter-example succs = [t : t is a successor of s w.r.t. the next-state relation] queue += succs return true You can visualize the state graph as a .dot file, this works for small state spaces (it might still be OK for your example). In any case, it is a good idea to check properties that you expect to be false and inspect the counter-example to check that it corresponds to the computation that you expect. For example, you could check properties such as hash[10] ~= 101 (invariant stating that one can not assign value 101 to key 10) [][hash[10] = 101 => hash'[10] = 101]_vars (temporal property asserting that once key 10 has that value, it will never be assigned a different value) etc. I am sure that more could be done for visualizing and exploring state graphs. 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/55951053-AB1D-477A-B8F2-D520694557D4%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

**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

**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:*recipient

- Prev by Date:
**[tlaplus] Specifying an arbitrary function and then using it in TLC** - Next by Date:
**Re: [tlaplus] Specifying an arbitrary function and then using it in TLC** - 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):