uwplse / verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
BSD 2-Clause "Simplified" License
183 stars 19 forks source link

allow zero as node name for vard to enable equivalence with all_fin #11

Closed palmskog closed 8 years ago

palmskog commented 8 years ago

Extraction for all_fin was changed to start from 0 rather than 1 to match fin_to_nat. Here is an update to vard.ml to enable setting node names to 0 when using extracted code. The README is updated to reflect this. Ideally, whether the collection of nodes passed on the command line matches the extracted all_fin names should be checked.