Heidi Howard
Heidi Howard
Checkpointing successfully finished ~20 mins ago (and model checking has resumed) but the running status still shows ``Checkpointing``. I am running v1.5.4. 
*Currently, the function of this PR is to improve visibility of the ongoing work on the [TLA+ specifications](https://github.com/microsoft/CCF/tree/main/tla). It is not yet ready to be reviewed/merged.* This PR will fix...
Suggested by @achamayou. **Is your feature request related to a problem? Please describe.** If we have many instances of CCF stacked onto one set of VMs then the leaders may...
It is my understanding that newly added nodes begin ticking (see: https://github.com/microsoft/CCF/blob/src/consensus/aft/raft.h#L1305) and thus can become a candidate when their reconfiguration txn becomes committable (followed by a signature txn). If...
**Describe the bug** TLC found a violation of the ``MoreUpToDateCorrectInv`` invariant when checking the current TLA+ specification in https://github.com/microsoft/CCF/blob/main/tla/raft_spec/ccfraft.tla. Note that this is different TLA+ specification (and thus a different...
**Describe the bug** The current install docs (https://microsoft.github.io/CCF/main/build_apps/install_bin.html#install) are describing v2.x RCs, however, the commands provided install v1.0.19 by default. **To Reproduce** Follow the current install instructions: https://microsoft.github.io/CCF/main/build_apps/install_bin.html#install **Expected behavior**...
It might be useful to highlight in the docs where different default configurations options are used by `sandbox.sh`. For instance, the documentation for the sig delay says this is 1s/1000ms,...
Would it make sense to rename the second column of the states table, currently called `Diameter`, to something like `Depth` or `Length`? This would make it more sense to me...
Whilst comparing `raft.h` to the TLA+, I spotted a few possible opportunities to tidy up `raft.h`. None of these changes should alter the behavior of `raft.h` (though I might be...
Former candidates can vote twice in one term in CCF Raft. This is not a safe violation as it cannot lead to two leaders in a term but it is...