Re: [tlaplus] Is TLA spec shorter than code?

[Hillel Wayne <hwayne@xxxxxxxxx>]

It could just be inexperience. I can't go through the whole spec for you, but one thing that I notice is you have

IsValidData(d) == d /= NULL /\ d.id \in Nat /\ d.value \in Nat /\ d.version <= MaxVersion
TypeInvariant ==
    /\ \/ UpdateRequestQueue = <<>>
       \/ \A i \in 1..Len(UpdateRequestQueue):
          /\ UpdateRequestQueue[i].client \in Clients
          /\ IsValidData(UpdateRequestQueue[i].data)
    /\ \/ DeleteRequestQueue = <<>>
       \/ \A i \in 1..Len(DeleteRequestQueue):
          /\ DeleteRequestQueue[i].client \in Clients
          /\ IsValidData(DeleteRequestQueue[i].data)

Assuming you have no additional keys in your structs, this can be shorted to:

ValidData == [id: Nat, value: Nat, version: 1..MaxVersion]

TypeInvariant ==

    /\ UpdateRequestQueue \in Seq([client: Clients, data: ValidData])

    /\ DeleteRequestQueue \in Seq([client: Clients, data: ValidData])

Which is less than half the length and much clearer. I'd guess there are similar places you can clean up the spec.

H

On 7/1/19 2:10 PM, zll zbw wrote:

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.

--
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/0a59e189-36a2-b727-3cf3-226c27df4f70%40gmail.com.
For more options, visit https://groups.google.com/d/optout.