[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