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

[tlaplus] Is TLA spec shorter than code?

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!

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7fb23501-ca11-437d-9351-b5967765815f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Attachment: chatDataCache.tla
Description: Binary data