Add b-tree example

[lorin]

Add an entry for B-tree example.

[ahelwer]

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]

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]

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

[lorin]

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]

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]

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]

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]

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

[lorin]

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]

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

[ahelwer]

Would be nice to have a little blurb saying what this spec is and what interesting features or approaches it has!

[ahelwer]

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]

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]

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