Properties `Unforg_Ltl` and `Corr_Ltl` of `aba_asyn_byz` hold if all nodes *start* in `V0` or `V1`

[lemmy]

@konnov @josef-widder Are the liveness properties Unforg_Ltl and Corr_Ltl supposed to only hold if all processes start in V0 or V1, respectively? Should the properties be box-quantified?

https://github.com/tlaplus/Examples/blob/8cef3cfa2094195d3a01f09f66f6d1ec7115c3c6/specifications/aba-asyn-byz/aba_asyn_byz.tla#L147-L152

[konnov]

hey @lemmy, the first option is the right one:

Are the liveness properties Unforg_Ltl and Corr_Ltl supposed to only hold if all processes start in V0 or V1, respectively?

Basically, the right-hand side of unforgeability should hold true, if all correct processes start with V0, i.e., they have not seen the broadcast message. The right-hand side of correctness should hold true, if all correct processes start with V1, that is, they all have see the broadcast message.

So I think the way the properties are written now is correct.

[lemmy]

Thanks for the clarification. The specification could benefit from adding a comment or two for better understanding. ;-)