Bogus safety violation checking if a set is a subset of Nat.

[lemmy]

Fixes Github issue #2948
#2948

[lemmy]

5724d0d causes Apalache to report a proper error message: SetInRule is not implemented for type PowSet[Set(Int)] (found in {1, 2, 3, 4} ∈ SUBSET Nat).

[lemmy]

@thpani @konnov c69c355 and 830caa7 cause Apalache to no longer hit this code path for the given inputs (the expressions are rewritten elsewhere). Would you like to add the safeguard below anyway? If you do, I'll update the tests to expect the corresponding error message.

https://github.com/apalache-mc/apalache/pull/2960/files#diff-455ee0089c33ede12710ae233adedc17473d8ac7cc6a2ca7246f127a7482512aR58-R60

[konnov]

@thpani @konnov c69c355 and 830caa7 cause Apalache to no longer hit this code path for the given inputs (the expressions are rewritten elsewhere). Would you like to add the safeguard below anyway? If you do, I'll update the tests to expect the corresponding error message.

https://github.com/apalache-mc/apalache/pull/2960/files#diff-455ee0089c33ede12710ae233adedc17473d8ac7cc6a2ca7246f127a7482512aR58-R60

Hey Markus! The Apalache encoding was not designed to deal with infinite sets. The only exception (a hack?) was made for Int and Nat, for the case of introducing an integer constant like \E x \in Int: P in an action. Since both OOPSLA19 and TACAS23 encodings are using arenas, it is expected that a set cell carries an overapproximation of the set.

I have two thoughts about this:

• If you are trying to deal with infinite sets in the bmcmt rewriting rules, it is, most likely, too late in the rewriting process. These rules have non-trivial invariants about arenas (which are not really documented). For what you are doing, OptimizationPass seems to be the right place.
• We could probably extend an encoding for infinite sets, though in practice what one probably needs the most is generating bounded-size sets that may contain unbounded integers. Developing a consistent encoding is a focused effort. I feel like hacking the current encoding here and there may lead to very unexpected results in model checking.

[lemmy]

@konnov This PR does not aim to extend the encoding. Instead, it ensures that Apalache throws an error when an infinite set is encountered in a context where it isn't properly handled.

[konnov]

Ah, sorry, I missed that. Yes, this makes sense to add. Thanks a lot!

[konnov]

A safeguard would definitely help!

[lemmy]

This is ready for review and merging. Although commits c69c355 and 830caa7 prevent any of the three encodings from reporting a bogus invariant violation for expressions like {1, 2, 3} \in SUBSET Nat (due to rewriting), this update ensures that Apalache generates a clear error message when handling infinite sets, should the rewrites ever be removed in the future.

[konnov]

This makes sense! Thanks for adding the safeguards

[konnov]

I cannot add an entry in .unchanged, since it's your PR. Could you add one?

[lemmy]

What should that entry be?

[konnov]

What should that entry be?

Oh, just one line describing the nature of the change, see https://github.com/apalache-mc/apalache/blob/main/CONTRIBUTING.md#how-to-record-a-change

I guess, it should technically go into bug-fixes.

[lemmy]

done

[thpani]

LGTM