kadirozde commented on code in PR #2461: URL: https://github.com/apache/phoenix/pull/2461#discussion_r3203173281
########## src/main/tla/ConsistentFailover/README.md: ########## @@ -0,0 +1,380 @@ +# Phoenix Consistent Failover -- TLA+ Specification + +Formal specification of the Phoenix Consistent Failover protocol using TLA+ and the TLC model checker. The spec verifies safety properties (mutual exclusion, zero RPO, abort correctness) under arbitrary interleavings of admin actions, HDFS failures, RS crashes, ZK connection/session failures, watcher retry exhaustion, and the anti-flapping timer. Review Comment: This claims that the model is for verifying safety properties but at the end of this README file, it states that three liveness properties are also verified. Should we revise this statement? -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
