I have no experience modeling append-only logs, but this scaling problem comes up when adding history variables to a spec, right?
Even though you’re modeling an append-only log, the solution for scalability, while retaining some log in the state space, might be removing event sequences that leave the state unchanged from the log. One could achieve this “solution” by optimizing the state space inside the spec itself.
Since we’re dealing with a sequence of events, symmetry sets wouldn’t really help, but memoization and data compression might (?).
The “solution” (in many quotes) from a spec:
Some spec has avariable that represents the append-only log. Every action that updates would check whether there’s an equivalent, but smaller, event sequence, thus compressing the log and the state space. This optimization would reduce the state space, reduce overall memory consumption but, even in parallel (thanks to TLC), might add substantial processing cost. It’s not a lossless compression, either.
Let’s say we had states
A spec that optimizes for log size would only have one state: .
A spec that applies a view would also have only one state , but with complete information loss.
One way to achieve this compression is by checking equivalent suffixes.
Let’s say some spec has variables and (an integer). Possible events are :
We know a few suffixes leave the system as if nothing had happened before (except time passing):.
Suppose we’re in a state where
Suppose we’re in a state where +1’ happens, so we add it to the log: . But this suffix is marked as redundant: the log would be transformed into .
The community modulecontains a operator. Every action that changes the would be written like :
By compressing, the state space would contain a subset of possible logs, which might be a problem…
I haven’t tested any of this, by the way, but I’m curious to know if there are any other solutions.
Since TLA+ sees use in distributed systems, it often has to be used to model append-only logs. However, logs of this sort place a path dependence on states; if event A happens before event B, and it leads to the same outward system state as if event B happened before event A, TLC will nonetheless have these as two separate states because their order was recorded in the log. This means the state tree scales in size factorially and greatly limits the viability of modeling systems beyond two, perhaps three nodes and a small depth.I've run into this problem a few times and have never come up with a decent way of handling it. Perhaps it's possible to write your spec so the append-only log is analogous to the clock in real-time specs (ignored & excluded from the model checker view). What strategies have others developed?Andrew