search

informalsystems / verification

Specifications of the protocols and the experiments on their verification
9 stars 2 forks source link

Issue model checking blockchain.tla #1

Closed ebuchman closed 5 years ago

ebuchman commented 5 years ago

So I'm trying model check blockchain.tla.

If I use these initial values, it passes fine:

if I use these initial values, it passes fine:
MaxPower <- 1
initAppState <- 0
initValidators <- {1}
MaxN <- 1

but if I set MaxN <- 2, then it fails.

It seems like we’re at least missing the constant initVotingPower, but if I add it, I can’t figure out how to initialize. This isn't working: [1 |-> 1]

konnov commented 5 years ago

It should work now. The problem was in using prevCommiters instead of prevCommiters' in Next. Hopefully, it makes more sense now, as the spec is rather abstract.