ChangRoberts!TypeOK refers to non-existing PlusCal label "n2" about examples

[lemmy]

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

[lemmy]

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

[konnov]

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

[konnov]

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

[lemmy]

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]

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

[muenchnerkindl]

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.