A set filter over PowSet[FinSet[Int]] is not implemented #2762
Labels
Milestone
Comments
thpani
added this to the X16: Advanced structures: Unbounded sets, choose, powersets, function sets milestone
lemmy
added a commit
to lemmy/apalache
that referenced
this issue
Aug 16, 2024
…rd has infinite co-domains. Simplified real-world scenario: ```tla EXTENDS Integers VARIABLE \* @type: Set({ p: (Int) }); v TypeOK == v \in SUBSET [ p: Int ] Init == v = { [p |-> 42] } Next == UNCHANGED v ``` Apalache Error: ```sh $ 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: ```tla S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T ``` Related commits, issues, PRs: * 625a164 * 785e269 * apalache-mc#723 * apalache-mc#1627 * apalache-mc#2762 * apalache-mc#1453 * apalache-mc#1629 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to lemmy/apalache
that referenced
this issue
Aug 16, 2024
…rd has infinite co-domains. Simplified real-world scenario: ```tla EXTENDS Integers VARIABLE \* @type: Set({ p: (Int) }); v TypeOK == v \in SUBSET [ p: Int ] Init == v = { [p |-> 42] } Next == UNCHANGED v ``` Apalache Error: ```sh $ 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: ```tla S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T ``` Related commits, issues, PRs: * 625a164 * 785e269 * apalache-mc#723 * apalache-mc#1627 * apalache-mc#2762 * apalache-mc#1453 * apalache-mc#1629 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to lemmy/apalache
that referenced
this issue
Aug 16, 2024
…rd has infinite co-domains. Simplified real-world scenario: ```tla EXTENDS Integers VARIABLE \* @type: Set({ p: (Int) }); v TypeOK == v \in SUBSET [ p: Int ] Init == v = { [p |-> 42] } Next == UNCHANGED v ``` Apalache Error: ```sh $ 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: ```tla S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T ``` Related commits, issues, PRs: * 625a164 * 785e269 * apalache-mc#723 * apalache-mc#1627 * apalache-mc#2762 * apalache-mc#1453 * apalache-mc#1629 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
2 tasks
lemmy
added a commit
to lemmy/apalache
that referenced
this issue
Aug 16, 2024
…rd has infinite co-domains. Simplified real-world scenario: ```tla EXTENDS Integers VARIABLE \* @type: Set({ p: (Int) }); v TypeOK == v \in SUBSET [ p: Int ] Init == v = { [p |-> 42] } Next == UNCHANGED v ``` Apalache Error: ```sh $ 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: ```tla S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T ``` Related commits, issues, PRs: * 625a164 * 785e269 * apalache-mc#723 * apalache-mc#1627 * apalache-mc#2762 * apalache-mc#1453 * apalache-mc#1629 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to lemmy/apalache
that referenced
this issue
Aug 16, 2024
…rd has infinite co-domains. Simplified real-world scenario: ```tla EXTENDS Integers VARIABLE \* @type: Set({ p: (Int) }); v TypeOK == v \in SUBSET [ p: Int ] Init == v = { [p |-> 42] } Next == UNCHANGED v ``` Apalache Error: ```sh $ 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: ```tla S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T ``` Related commits, issues, PRs: * 625a164 * 785e269 * apalache-mc#723 * apalache-mc#1627 * apalache-mc#2762 * apalache-mc#1453 * apalache-mc#1629 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to lemmy/apalache
that referenced
this issue
Aug 16, 2024
…rd has infinite co-domains. Simplified real-world scenario: ```tla EXTENDS Integers VARIABLE \* @type: Set({ p: (Int) }); v TypeOK == v \in SUBSET [ p: Int ] Init == v = { [p |-> 42] } Next == UNCHANGED v ``` Apalache Error: ```sh $ 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: ```tla S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T ``` Related commits, issues, PRs: * 625a164 * 785e269 * apalache-mc#723 * apalache-mc#1627 * apalache-mc#2762 * apalache-mc#1453 * apalache-mc#1629 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
lemmy
added a commit
to lemmy/apalache
that referenced
this issue
Aug 16, 2024
…rd has infinite co-domains. Simplified real-world scenario: ```tla EXTENDS Integers VARIABLE \* @type: Set({ p: (Int) }); v TypeOK == v \in SUBSET [ p: Int ] Init == v = { [p |-> 42] } Next == UNCHANGED v ``` Apalache Error: ```sh $ 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: ```tla S \in SUBSET [a : T] ~~> \A r \in S: DOMAIN r = { "a" } /\ r.a \in T ``` Related commits, issues, PRs: * 625a164 * 785e269 * apalache-mc#723 * apalache-mc#1627 * apalache-mc#2762 * apalache-mc#1453 * apalache-mc#1629 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Spin-out from #878, which contained two reports in a single issue.
Apalache throws
A set filter over PowSet[FinSet[Int]] is not implementedOriginally posted by @lemmy in #878 (comment)
The text was updated successfully, but these errors were encountered: