How to go about property testing a consensus protocol using PropCheck

Consensus can be defined as all nodes reaching the same state given a variety of (generated) inputs { in this paxos context, it would probably be time / proposal id and proposal val). I’m guessing that if more sophistication was required you could use PropCheck’s state machine properties to ensure all nodes (acceptors) are in the same state beyond what I currently have.

You could probably generate symbolic calls as the aforementioned book talks about in Chapter 4: Custom Generators e.g. a sequence of function calls that are generated with different proposal ids and values…

(From the book) ===> Testing prop_generators:prop_dict_symb() ..............! Failed: After 15 test(s). {call,dict,store,[-6,8, {call,dict,store,[46,-13, {call,dict,store,[2,-2, {call,dict,store,[22,-2, {call,dict,store,[-12,-2, {call,dict,new,[]}]}]}]}]}]}

Here’s some more on consensus in a popular context these days Consensus

Super smart people? @adkron @ferd

Just curious..