search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

Add b-tree example #147

Closed lorin closed 1 week ago

lorin commented 4 months ago

Add an entry for B-tree example.

ahelwer commented 4 months ago

Would of course be appreciated if you added the spec to the repo itself instead of just a link! It's fine if you only want to add a link though.

lemmy commented 4 months ago

Considering the widespread use of B-trees in computer science education, would it be appropriate to label this as 'Beginner'?

By the way, you will have to sign-off on the commit to pass the DCO check.

lemmy commented 4 months ago

.oO(This specification is an excellent candidate for creating an animation)

lorin commented 4 months ago

Would of course be appreciated if you added the spec to the repo itself instead of just a link! It's fine if you only want to add a link though.

Sure, I can add this directly to the repo. I'll revise my PR.

Considering the widespread use of B-trees in computer science education, would it be appropriate to label this as 'Beginner'?

Yep, seems reasonable.

By the way, you will have to sign-off on the commit to pass the DCO check.

Will do.

.oO(This specification is an excellent candidate for creating an animation)

I've never done animations with TLA+ before. I'll look through the existing specifications and see if I can figure out how to do that.

lemmy commented 4 months ago

I've never done animations with TLA+ before. I'll look through the existing specifications and see if I can figure out how to do that.

In case you want to give it a try... Writing animation specifications is straightforward. There is a module that provides TLA+ definitions of SVG primitives. Below are a few examples. The first three are for TLC, and the other ones are for Will Schultz's TLA-web. Despite being for different systems, the definitions are quite similar.

https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/EWD998_anim.tla https://github.com/tlaplus/Examples/blob/master/specifications/ewd687a/EWD687a_anim.tla https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840_anim.tla https://github.com/will62794/tla-web/blob/master/specs/EWD998.tla#L123-L201 https://github.com/will62794/tla-web/blob/master/specs/AbstractRaft_anim.tla#L210-L280

lemmy commented 3 months ago

Just a suggestion: have you considered refining, for example, the KV of https://github.com/tlaplus/Examples/tree/master/specifications/KeyValueStore or any other existing KV specification? Given how many database specs there are, it would be really nice to show that they all refine the same abstract KV.

ahelwer commented 3 months ago

I think that might take a lot of work because I never wrote the KVStore spec with the intention of it being an abstract specification. In particular it focuses on implementing snapshot isolation, which I don't think is the case here.

@lorin take a look at the README.md of this repo for instructions on how to onboard your spec & model to the manifest so it can be checked by the CI.

ahelwer commented 1 month ago

Hi @lorin do you intend to see this PR through? Thanks!

lorin commented 1 month ago

Hi @lorin do you intend to see this PR through? Thanks!

Hey @ahelwer. Sorry, yes, I do intend to circle back to this at some point (maybe this week?)

ahelwer commented 4 weeks ago

The title in the README "B-trees" is a foreign key that has to match the title in manifest "btree"

ahelwer commented 4 weeks ago

Ooops the description also has to match. Sorry about that, I don't think the README table requirements are documented in the README directions itself.

ahelwer commented 4 weeks ago

Oh you need to move your b-tree record to the first README table, the one of specs that are contained within the repository. Follow the format of others there.

lorin commented 1 week ago

I'm going to close this one out for now, because I don't currently have the cycles to work on it.