search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.26k stars 196 forks source link

ChangRoberts!TypeOK refers to non-existing PlusCal label "n2" #34

Closed lemmy closed 3 years ago

lemmy commented 3 years ago

https://github.com/tlaplus/Examples/blob/22e6b2daae5e0173ac856e8eab5c01abd90b39d4/specifications/chang_roberts/ChangRoberts.tla#L119

lemmy commented 3 years ago

@konnov https://apalache.informal.systems/docs/adr/006rfc-unit-testing.html mentions TypeOK with n2 too.

konnov commented 3 years ago

Is it an issue because TypeOK could be used to prove inductive invariants?

konnov commented 3 years ago

By the way, I guess, you would easily find such a thing with unit tests

lemmy commented 3 years ago

By the way, I guess, you would easily find such a thing with unit tests

The RFC on unit tests is about ChangRoberts, yet missed this issue. At any rate, I think these issues are generally rare for TLA+. From my experience, this is usually an artifact of the user-defined TLA+ operators, such as TypeOK, going out of sync with the TLA+ translation of a PlusCal algorithm. I wager that the PlusCal algorithm was at some point refactored and the n2 label dropped, without updating TypeOK accordingly.

konnov commented 3 years ago

Well, we missed this issue, because the framework is not implemented :)

lemmy commented 3 years ago

Perhaps, the RFC should discuss how it helps catch this issue.

muenchnerkindl commented 3 years ago

Sure, there used to be an “n2” that disappeared at some point. However, note that the predicate remains an inductive invariant, it may simply be too much of an overapproximation for subsequent proofs. In particular, neither n0 nor n1 can fire in a state where pc equals “n2”. It is not clear to me if Apalache could actually find this issue.

On 28 Apr 2021, at 19:35, Markus Alexander Kuppe @.***> wrote:

 By the way, I guess, you would easily find such a thing with unit tests

The RFC on unit tests is about ChangRoberts, yet missed this issue. At any rate, I think these issues are generally rare for TLA+. From my experience, this is usually an artifact of the user-defined TLA+ operators, such as TypeOK, going out of sync with the TLA+ translation of a PlusCal algorithm. I wager that the PlusCal algorithm was at some point refactored and the n2 label dropped without updating TypeOK.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.