Rewrite for set membership of the powerset of a record where the record has infinite co-domains.

[lemmy]

Simplified real-world scenario:

EXTENDS Integers

VARIABLE
  \* @type: Set({ p: (Int) });
  v

TypeOK ==
  v \in SUBSET [ p: Int ]

Init ==
  v = { [p |-> 42] }

Next ==
  UNCHANGED v

Apalache Error:

$ apalache-mc check --inv=TypeOK APARecSub.tla
[...]
Input error (see the manual): Found a set map over an infinite set of CellTFrom(Int). Not supported.

Rewrite:

S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T

Related commits, issues, PRs:

• 625a164

• 785e269

• [FEATURE] Use types to simplify TypeOK #723

• An optimization for membership in a record set #1627

• A set filter over PowSet[FinSet[Int]] is not implemented #2762

• Simplify records in TypeOK #1453

• Optimize membership for record sets #1629

PR hygiene

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)

[konnov]

Looks good to me. Thanks you for the contribution! Could you add a release note like this one, so your contribution would be visible in the next release.

[lemmy]

Looks good to me. Thanks you for the contribution! Could you add a release note like this one, so your contribution would be visible in the next release.

Done

[lemmy]

May I assume that you won't be releasing a new minor release with this change because of the move to the independent github org anytime soon?

[konnov]

May I assume that you won't be releasing a new minor release with this change because of the move to the independent github org anytime soon?

I have started a job on cutting 0.45.0. It should be fairly easy to do.

[konnov]

The last step of the release did not work. I will have a look into it: #2951

[lemmy]

Blast, I've found that it rewrites APARecSub but not APARecRecSub:

------------------------- MODULE APARecSub ------------------------------           
EXTENDS Integers

VARIABLE
    \* @type: Set({ p: Int });
    v

TypeOK ==
    v \in SUBSET [ p: Int ]

Init ==
    v = { [p |-> 42] }

Next ==
    UNCHANGED v
========================================================================== 

------------------------- MODULE APARecRecSub -------------------------
EXTENDS Integers

VARIABLE
    \* @type: { p : Set ({ t : Int }) };
    v

TypeOK ==
    v \in [ p : SUBSET [t : Int] ]  

Init ==
    v = [ p |-> [t : Int] ]

Next ==
    UNCHANGED v
========================================================================== 

Will investigate...

[lemmy]

Blast, I've found that it rewrites APARecSub but not APARecRecSub:

------------------------- MODULE APARecSub ------------------------------           
EXTENDS Integers

VARIABLE
    \* @type: Set({ p: Int });
    v

TypeOK ==
    v \in SUBSET [ p: Nat \ {0} ]

Init ==
    v = { [p |-> 42] }

Next ==
    UNCHANGED v
========================================================================== 

------------------------- MODULE APARecRecSub -------------------------
EXTENDS Integers

VARIABLE
    \* @type: { p : Set ({ t : Int }) };
    v

TypeOK ==
    v \in [ p : SUBSET [t : Int] ]  

Init ==
    v = [ p |-> [t : Int] ]

Next ==
    UNCHANGED v
========================================================================== 

Will investigate...

The rewrite works correctly and Apalache successfully handles a finite domain as in heidihoward/pbft-tlaplus#5. I presume another rewrite is able to handle the simpler ∀t_4 ∈ v: ((DOMAIN t_4 = {"p"}) ∧ t_4["p"] ∈ Int) but fails to handle ∀t_9 ∈ v["p"]: ((DOMAIN t_9 = {"t"}) ∧ t_9["t"] ∈ Int).

[konnov]

We have the release 0.45.1 cut, which includes your PR: https://github.com/apalache-mc/apalache/actions/runs/10452011929