Hey guys, I wrote a spec for my cache algorithm, in which I cache data per id in memory after the first read from DB.
There're two parts in my spec, part 1 is the core algorithm for handling data update and deletion in cache of my server, as well as cache expiration. part 2 is a mimic of client and DB. Each part contributed about 200 lines in the final spec.
While in the actual program, the core algorithm, as specified in part 1 of my spec, only takes 200 lines too. I also not able to think abstractly of the algorithm, because to make it right and to explore all state spaces, I have to cover every detail of the algorithm.
So my problem/question is how could TLA spec be both shorter and less detailed than the actual program.
Things that I think I did abstractly is the mimic of request/response from/to DB and client using sequence, but in actual code, the request/response code are well encapsulated, so I also only need one line for them. I think also specified cache expiration abstractly, but I don't have to write it in the actual program, since it's in a library already.
I attached the spec, please help point out where I did wrong. Thanks!