A Chord ring maintenance protocol implementation. Significantly lacking in the invariant department, but has decent implementation of all the events of the protocol.
A stripped down version of Chord with only things required to replicate the Ordered Ring counterexample from Figure 7 of Using Lightweight Modeling To Understand Chord by Pamela Zave. This implementation features "god knowledge" to simplify track of node states, and safe() table to identify nodes that shouldn't be crashed.
There are lots of comments within the files themselves.
A tiny change to the parser to enable the <= and >= operators.
A Chord ring maintenance protocol implementation. Significantly lacking in the invariant department, but has decent implementation of all the events of the protocol. A stripped down version of Chord with only things required to replicate the Ordered Ring counterexample from Figure 7 of Using Lightweight Modeling To Understand Chord by Pamela Zave. This implementation features "god knowledge" to simplify track of node states, and safe() table to identify nodes that shouldn't be crashed. There are lots of comments within the files themselves. A tiny change to the parser to enable the <= and >= operators.