[FEATURE] Use types to simplify `TypeOK` #723

konnov · 2021-04-10T08:02:27Z

Blocked by #401 Precise type checking for records

We should use type information to simplify membership tests such as x \in BOOLEAN, x \in Int, x \in STRING, x \in Seq(...). By knowing the types, we could write a preprocessing pass that rewrites the above tests to TRUE, if the types are matching the tests.

n \in Nat (Use type information to simplify membership tests #1406)
i \in Int, b \in BOOLEAN, \r \in Real (Use type information to simplify membership tests #1406)
seq \in Seq(_) (Use type information to simplify membership tests #1406)
fun \in [Int -> Int] (Simplify SUBSET and sets of functions [S1 -> S2] in TypeOK #1443)
<<{{1}}>> \in Seq(SUBSET Int) or {<<1>>} \in SUBSET (Seq(Int)) (Simplify SUBSET and sets of functions [S1 -> S2] in TypeOK #1443)
tup \in S1 \X ... \X SN (Simplify tuples in TypeOK #1445)
records (Simplify records in TypeOK #1453, blocked by Meta-issue: variants and precise record types #401 – maybe alternative solution in Optimize membership for record sets #1629)

The text was updated successfully, but these errors were encountered:

thpani · 2022-02-22T09:26:10Z

@konnov What's a good place to implement this? ExprOptimizer or a separate transformation in OptimizationPass or ...?

konnov · 2022-02-22T09:29:36Z

I would implement a separate transformation similar to ExprOptimizer.

Remove #723 as beginner task on the landing page, as it's (almost) fully implemented

thpani · 2022-04-15T17:11:08Z

We should revisit this based on #1629

konnov · 2022-04-15T17:19:23Z

Do we handle the case seq \in Seq(S), when S is a finite set, not Int, Nat, or BOOLEAN? I guess, we could translate it to \A x \in DOMAIN seq: seq[x] \in S.

konnov · 2022-07-13T07:14:54Z

Simplification for records should be unblocked now, since #401 is closed. Shall we revisit this issue any time soon?

thpani · 2022-07-13T08:15:20Z

Simplification for records should be unblocked now, since #401 is closed. Shall we revisit this issue any time soon?

Does it make sense to follow up on this after we enable TypeSystem 1.2 by default in #1943?

konnov · 2022-07-13T08:53:53Z

Yes, we can do it after the switch, though nothing prevents us from implementing this transformation right now.

konnov · 2022-12-21T08:36:41Z

Just labelled this one as unblocked.

@type

…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>

@type

…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>

@type

…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>

@type

…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>

@type

…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>

@type

…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>

@type

…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>

konnov added usability UX improvements Alpha Centauri The first public alpha release labels Apr 10, 2021

konnov added this to the April iteration -- alpha release milestone Apr 10, 2021

konnov self-assigned this Apr 10, 2021

shonfeder modified the milestones: April iteration, May iteration Apr 29, 2021

shonfeder modified the milestones: May iteration, July iteration Jul 5, 2021

konnov added the help wanted label Oct 12, 2021

konnov removed their assignment Oct 12, 2021

konnov added Fprepro Feature: TLA+ preprocessor and removed usability UX improvements Alpha Centauri The first public alpha release labels Nov 8, 2021

konnov removed this from the July iteration milestone Nov 18, 2021

konnov mentioned this issue Jan 31, 2022

[FEATURE] preprocess e \in STRING #603

Closed

thpani self-assigned this Feb 22, 2022

thpani mentioned this issue Feb 24, 2022

Use type information to simplify membership tests #1406

Merged

thpani removed the help wanted label Feb 28, 2022

This was referenced Mar 7, 2022

Simplify SUBSET and sets of functions [S1 -> S2] in TypeOK #1443

Merged

Split TestSetMembershipSimplifier #1449

Merged

Simplify records in TypeOK #1451

Closed

Simplify records in TypeOK #1453

Closed

thpani added a commit that referenced this issue Mar 9, 2022

Remove implemented beginner task

81e0de4

Remove #723 as beginner task on the landing page, as it's (almost) fully implemented

thpani mentioned this issue Mar 9, 2022

Remove implemented beginner task from landing page #1455

Merged

thpani added the blocked Issue blocked by another (for filtering) label May 3, 2022

konnov added the product-owner-triage This should be triaged by the product owner label Jul 13, 2022

konnov removed the blocked Issue blocked by another (for filtering) label Dec 21, 2022

thpani mentioned this issue May 26, 2023

Simplify records in TypeOK #2570

Merged

4 tasks

shonfeder closed this as completed in #2570 Jun 2, 2023

apalache-bot mentioned this issue Jun 2, 2023

[release] 0.40.1 #2587

Merged

lemmy mentioned this issue Aug 16, 2024

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

Merged

2 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[FEATURE] Use types to simplify `TypeOK` #723

[FEATURE] Use types to simplify `TypeOK` #723

konnov commented Apr 10, 2021 •

edited by shonfeder

Loading

thpani commented Feb 22, 2022

konnov commented Feb 22, 2022

thpani commented Apr 15, 2022

konnov commented Apr 15, 2022

konnov commented Jul 13, 2022

thpani commented Jul 13, 2022

konnov commented Jul 13, 2022

konnov commented Dec 21, 2022

[FEATURE] Use types to simplify TypeOK #723

[FEATURE] Use types to simplify TypeOK #723

Comments

konnov commented Apr 10, 2021 • edited by shonfeder Loading

thpani commented Feb 22, 2022

konnov commented Feb 22, 2022

thpani commented Apr 15, 2022

konnov commented Apr 15, 2022

konnov commented Jul 13, 2022

thpani commented Jul 13, 2022

konnov commented Jul 13, 2022

konnov commented Dec 21, 2022

[FEATURE] Use types to simplify `TypeOK` #723

[FEATURE] Use types to simplify `TypeOK` #723

konnov commented Apr 10, 2021 •

edited by shonfeder

Loading