[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
BPCon TLC Model Variables
- From: Balaji Arun <ba2...@xxxxxx>
- Date: Sun, 26 Aug 2018 07:14:23 -0700 (PDT)
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.
