`InvalidNotObservedInv` vacuously true, `InvalidNotObservedInv` and `CommittedRwSerializableInv` slow to evaluated by TLC due to combinatorial explosion.

microsoft / CCF

Confidential Consortium Framework

https://microsoft.github.io/CCF/

Apache License 2.0

761 stars 205 forks source link

`InvalidNotObservedInv` vacuously true, `InvalidNotObservedInv` and `CommittedRwSerializableInv` slow to evaluated by TLC due to combinatorial explosion. #6164

Closed lemmy closed 2 weeks ago

lemmy commented 2 weeks ago

See commit messages for proof of equivalence that passed TLAPS scrutiny. Please do not squash to preserve the commit messages. TLC now checks all models within a couple of seconds.