search

tlaplus / Examples

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

Add Raft spec with Apalache type annotations #42

Closed lemmy closed 3 years ago

lemmy commented 3 years ago

@konnov Do you have a variant of raft.tla that has been annotated with types for Apalache?

We did it at least once. There was one issue with Raft, where they used a function as a sequence:

https://github.com/ongardie/raft.tla/blob/974fff7236545912c035ff8041582864449d0ffe/raft.tla#L378-L379

There is a simple fix for that: just use SubSeq instead of this explicit construction. I cannot find an annotated version of raft on my laptop though. We could probably add one in tlaplus-examples.

Originally posted by @konnov in https://github.com/tlaplus/tlaplus/issues/677#issuecomment-948433148

dranov commented 3 years ago

@lemmy apalache_no_membership in https://github.com/dranov/raft-tla has type annotations.

lemmy commented 3 years ago

@dranov Do you want to create a PR for the Readme with a link to your spec?

dranov commented 3 years ago

@lemmy Sure. I will clean up the repo a bit on my side and make sure the spec works with the latest version of Apalache, and then make a PR here to link to it.

lemmy commented 3 years ago

Great, afterward it will make sense to move forward on https://github.com/tlaplus/Examples/issues/33.