Markus Alexander Kuppe

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...

.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. In case you want to...

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...

`CorrLtl` is not violated, even without a fairness constraint, because `InitNoBcast` causes `CorrLtl` to be vacuously true. Although not as easy to see, the same is true for `RelayLtl` (confirmed...

@konnov As one of the specification authors, could you please share your input?

Strings are sequences in TLA+. Do any of the operators below help with your use case? https://github.com/tlaplus/CommunityModules/blob/626a6bdf03b841dc97a371bc8fe88f7d5992aa76/modules/SequencesExt.tla#L366-L432 By the way, does the TLA+ debugger (VSCode) address your underlying debugging need?

You've discovered a shortcoming of TLC, not of TLA+: TLC does not have characters, which is why, e.g., `Head("abc")` doesn't work (compare: https://github.com/tlaplus/tlaplus/issues/512#issuecomment-717602371).

What would the definition of `TLCExt!Format` look like?

Let's just expose Java's `String#format` as `Format(formatString, sequenceOfParameters)`. It is also consistent with: https://github.com/tlaplus/CommunityModules/blob/626a6bdf03b841dc97a371bc8fe88f7d5992aa76/modules/CSV.tla#L9-L14?