search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
429 stars 40 forks source link

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

Closed lemmy closed 1 month ago

lemmy commented 1 month ago

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:

PR hygiene

lemmy commented 1 month ago

/cc @konnov As discussed last Friday.

lemmy commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

The last step of the release did not work. I will have a look into it: https://github.com/apalache-mc/apalache/issues/2951

lemmy commented 4 weeks ago

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 commented 4 weeks ago

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 https://github.com/heidihoward/pbft-tlaplus/issues/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 commented 4 weeks ago

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