-
Notifications
You must be signed in to change notification settings - Fork 198
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add b-tree example #147
base: master
Are you sure you want to change the base?
Add b-tree example #147
Conversation
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. |
.oO(This specification is an excellent candidate for creating an animation) |
Sure, I can add this directly to the repo. I'll revise my PR.
Yep, seems reasonable.
Will do.
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 |
Signed-off-by: Lorin Hochstein <lorinh@gmail.com>
Signed-off-by: Lorin Hochstein <lorinh@gmail.com>
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. |
Add an entry for B-tree example.