Spec claims to check (safety-prop) `UnforgLtl` but config actually also checks (liveness-props) `CorrLtl` and `RelayLtl`

[lemmy]

Examples/specifications/bcastByz/bcastByz.tla

Lines 173 to 176 in c993823

	(* This formula SpecNoBcast is used to only check Unforgeability.
	No fairness is needed, as Unforgeability is a safety property.
	*)
	SpecNoBcast == InitNoBcast /\ [][Next]_vars

Examples/specifications/bcastByz/bcastByz.tla

Lines 210 to 222 in c993823

	(* If a correct process broadcasts, then every correct process eventually accepts. *)
	CorrLtl == (\A i \in Corr: pc[i] = "V1") => <>(\A i \in Corr: pc[i] = "AC")
	(* If a correct process accepts, then every correct process accepts. *)
	RelayLtl == []((\E i \in Corr: pc[i] = "AC") => <>(\A i \in Corr: pc[i] = "AC"))
	(* If no correct process don't broadcast ECHO messages then no correct processes accept. *)
	UnforgLtl == (\A i \in Corr: pc[i] = "V0") => [](\A i \in Corr: pc[i] /= "AC")
	(* The special case of the unforgeability property. When our algorithms start with InitNoBcast,
	we can rewrite UnforgLtl as a first-order formula.
	*)
	Unforg == (\A i \in Proc: i \in Corr => (pc[i] /= "AC"))

Examples/specifications/bcastByz/bcastByzNoBcast.cfg

Line 6 in c993823

PROPERTIES CorrLtl RelayLtl

[lemmy]

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).

[lemmy]

@konnov As one of the specification authors, could you please share your input?

[ahelwer]

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.

[konnov]

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.

[konnov]

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.