key \in {0,1}, value \in {100,101}, {OP_GET, OP_PUT, OP_DELETE} for {0,1} \X {100,101} \X {OP_GET_PUT,OP_DELETE} or 12 unique possible client requests. (Note: get/delete operations never use the value part).
Have TLA+ check correctness properties (not shown) by exploring all possible ways a client can send KV requests. Imperatively all possible ways are given by:
For each subset s in {0,1} \X {100,101} \X {OP_GET_PUT,OP_DELETE}:
For each permutation p in s:
(re)initialize model
model check operations in p by running p[i] where i \in 1..Len(p)
Candidate Process 1 (elided): BAD: Doesn't do all permutations or subsets
with v \in HashKey, v \in HashValue, op \in ClientOps
do
call PerformOp(k,v.op);
end with;
Enabling DOT visualization & writing some python to print all paths from initial to final states using the DOT data, we can show that TLA+ tries the first rpc tuple, then tries rpc tuples 1 and 2, then 1 and 2 and 3 ... and on up to 1..12. But that's it!
Candidate Process 2 (elided): BAD: Doesn't do permutations or subsets:
\* Alternative formulation of process 1. Choose approach much the same ...
with i \in HashKey \X HashValue \X ClientOps
do
call PerformOp(i[1],i[2],i[3]);
end with;
At this point TLA+ can't read our minds:
it needs to be told to try all permutations of all subsets. But if one writes writes something like the following, JAVA runs out of stack:
Candidate Process 3 (elided): BAD: Won't work; runs out of stack
variables rpcs=Permutations(SUBSET(HashKey, v \in HashValue, op \in ClientOps))
with i \in rpcs
do
// now try to dig out individual RPCs and run them...
call PerformOp(....);
end with;
Moreover, even if this compiled and ran it's not clear if this achieves the goal. Did it check all permutations on subsets of size 5 starting from the initial state or did it run that
on top of permutations on subsets size 4?
What does one do here?