[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

BPCon TLC Model Variables

I am trying to model check the BPCon algorithm provided in http://lamport.azurewebsites.net/tla/byzpaxos.html. I tried to specifying the model parameters, but the model checker fails with a runtime exception "TLC encountered a non-enumerable quantifier bound Nat"

What am I doing wrong with the variables? Thank you in advance.