Re: BPCon TLC Model Variables

[Balaji Arun <ba2...@xxxxxx>]

I figured it out. I did not override the definition of Nat in "Advanced Options" tab

On Sunday, August 26, 2018 at 10:14:23 AM UTC-4, Balaji Arun wrote:

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.