Hi -
I'm working on a distributed KV store in Pluscal. Using TLA+ our desire is to ``SQLtise" our Pluscal code everywhere possible: describe what is to be done & checked without proscribing the steps ala imperative code to TLA+. Granted, we can fly closer to that mentality by avoiding Pluscal altogether ... but that's out of scope for the moment.
I am stuck on one basic aspect of this work which seems to exist right at the
boundary between allowing TLA+ to explore reachable states, and me telling it what I think reachable states are...
Assume:
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).
Goal:
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?