tlaplus
Spec claims to check (safety-prop) `UnforgLtl` but config actually also checks (liveness-props) `CorrLtl` and `RelayLtl`
https://github.com/tlaplus/Examples/blob/c9938239d07bb16031c5a692b30f14c6bfb34471/specifications/bcastByz/bcastByz.tla#L173-L176
https://github.com/tlaplus/Examples/blob/c9938239d07bb16031c5a692b30f14c6bfb34471/specifications/bcastByz/bcastByz.tla#L210-L222
https://github.com/tlaplus/Examples/blob/c9938239d07bb16031c5a692b30f14c6bfb34471/specifications/bcastByz/bcastByzNoBcast.cfg#L6
CorrLtl is not violated, even without a fairness constraint, because InitNoBcast causes CorrLtl to be vacuously true. Although not as easy to see, the same is true for RelayLtl (confirmed by checking that the invariant \A i \in Corr: pc[i] # "AC" holds).
@konnov As one of the specification authors, could you please share your input?
I was the one who added the models as part of work last year to mass-add models for all specs in the repo (#110). I did not pay particularly close attention to things like this, just added things that looked like properties to check to the model file then ran TLC to see whether it worked. So if this property shouldn't be checked then that's fine, it can be removed.
I was the one who added the models as part of work last year to mass-add models for all specs in the repo (#110). I did not pay particularly close attention to things like this, just added things that looked like properties to check to the model file then ran TLC to see whether it worked. So if this property shouldn't be checked then that's fine, it can be removed.
@lemmy you are right. In case of SpecNoBcast, both CorrLtl and RelayLtl are vacuously true, as no correct process ever reaches V1 or AC. This works as intended. Since SpecNoBcast is the special case of Spec, and CorrLtl and RelayLtl hold true on Spec, they also hold true on SpecNoBcast.
The above implication is obvious, but it's not machine-checked. So we could probably still keep the LTL formulas in both cases, just to show the properties on both kinds of specs.
It's interesting how both CorrLtl and RelayLtl work without fairness in case of SpecNoBcast. I am not sure about whether $SpecNoBcast \Rightarrow Spec$ holds true.