tlaplus
Add b-tree example
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.
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.
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.
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
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.
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.
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?)
The title in the README "B-trees" is a foreign key that has to match the title in manifest "btree"
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.
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.
I'm going to close this one out for now, because I don't currently have the cycles to work on it.