search

heidihoward / pbft-tlaplus

Formal specification of PBFT in TLA+
MIT License
7 stars 1 forks source link

Initial predicate suitable for validating inductive invariants probabilistically #1

Closed lemmy closed 3 months ago

lemmy commented 3 months ago

See https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

The parameters of RandomSetOfSubsets can be adjusted to generate fewer or more initial states.