Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
thpani opened this issue Oct 19, 2023 · 0 comments
Open

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

thpani opened this issue Oct 19, 2023 · 0 comments

Comments

@thpani
Copy link
Collaborator

thpani commented Oct 19, 2023

Spin-out from #878, which contained two reports in a single issue.

Apalache throws A set filter over PowSet[FinSet[Int]] is not implemented

------- MODULE Foo -------
EXTENDS Integers

CONSTANT 
    \* @type: Set(Int);
    S

ConstInit ==
    LET ss == SUBSET {1,2}
        sss == ss \ {{}}
    IN S \in sss

VARIABLE 
    \* @type: Set(Int);
    x

Init ==
    x = S

Next ==
    UNCHANGED x

Inv ==
    x # {}
==========================
markus@avocado:~$ apalache check --cinit=ConstInit --inv=Inv Foo
# Tool home: /home/markus/src/TLA/_community/apalache
# Package:   /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.15.9-SNAPSHOT-full.jar
# JVM args:  -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla
#
# APALACHE version 0.15.9-SNAPSHOT build v0.15.8-3-g6a26844
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
# 
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Checker options: filename=Foo, init=, next=, inv=Inv              I@15:14:36.647
Tuning:                                                           I@15:14:37.142
PASS #0: SanyParser                                               I@15:14:37.143
Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/Foo.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Naturals.tla
PASS #1: TypeCheckerSnowcat                                       I@15:14:37.899
 > Running Snowcat .::.                                           I@15:14:37.900
 > Your types are great!                                          I@15:14:38.032
 > All expressions are typed                                      I@15:14:38.033
PASS #2: ConfigurationPass                                        I@15:14:38.099
  > Foo: Loading TLC configuration                                I@15:14:38.102
  > No TLC configuration found. Skipping.                         I@15:14:38.108
  > Command line option --init is not set. Using Init             I@15:14:38.108
  > Command line option --next is not set. Using Next             I@15:14:38.108
  > Set the initialization predicate to Init                      I@15:14:38.109
  > Set the constant initialization predicate to ConstInit        I@15:14:38.110
  > Set the transition predicate to Next                          I@15:14:38.110
  > Set an invariant to Inv                                       I@15:14:38.111
PASS #3: DesugarerPass                                            I@15:14:38.169
  > Desugaring...                                                 I@15:14:38.176
PASS #4: UnrollPass                                               I@15:14:38.254
  > Unroller                                                      I@15:14:38.300
PASS #5: PrimingPass                                              I@15:14:38.352
  > Introducing ConstInitPrimed for ConstInit'                    I@15:14:38.361
  > Introducing InitPrimed for Init'                              I@15:14:38.371
PASS #6: CoverAnalysisPass                                        I@15:14:38.410
PASS #7: InlinePass                                               I@15:14:38.419
  > InlinerOfUserOper                                             I@15:14:38.426
  > LetInExpander                                                 I@15:14:38.436
  > FoldOperLetinizer                                             I@15:14:38.440
  > InlinerOfUserOper                                             I@15:14:38.443
Leaving only relevant operators: ConstInit, ConstInitPrimed, Init, InitPrimed, Inv, Next I@15:14:38.445
PASS #8: VCGen                                                    I@15:14:38.507
  > Producing verification conditions from the invariant Inv      I@15:14:38.508
  > VCGen produced 1 verification condition(s)                    I@15:14:38.520
PASS #9: PreprocessingPass                                        I@15:14:38.566
  > Before preprocessing: unique renaming                         I@15:14:38.567
 > Applying standard transformations:                             I@15:14:38.575
  > PrimePropagation                                              I@15:14:38.576
  > Desugarer                                                     I@15:14:38.621
  > UniqueRenamer                                                 I@15:14:38.717
  > Normalizer                                                    I@15:14:38.837
  > Keramelizer                                                   I@15:14:38.918
  > After preprocessing: UniqueRenamer                            I@15:14:39.033
PASS #10: TransitionFinderPass                                    I@15:14:39.085
  > Found 1 initializing transitions                              I@15:14:39.179
  > Found 1 transitions                                           I@15:14:39.182
  > Found constant initializer ConstInit                          I@15:14:39.182
  > Applying unique renaming                                      I@15:14:39.185
PASS #11: OptimizationPass                                        I@15:14:39.221
 > Applying optimizations:                                        I@15:14:39.263
  > ConstSimplifier                                               I@15:14:39.265
  > ExprOptimizer                                                 I@15:14:39.271
  > ConstSimplifier                                               I@15:14:39.275
PASS #12: AnalysisPass                                            I@15:14:39.291
 > Marking skolemizable existentials and sets to be expanded...   I@15:14:39.294
  > SkolemizationMarker                                           I@15:14:39.298
  > ExpansionMarker                                               I@15:14:39.301
 > Running analyzers...                                           I@15:14:39.311
  > Introduced expression grades                                  I@15:14:39.335
  > Introduced 0 formula hints                                    I@15:14:39.335
PASS #13: PostTypeCheckerSnowcat                                  I@15:14:39.336
 > Running Snowcat .::.                                           I@15:14:39.336
 > Your types are great!                                          I@15:14:39.503
 > All expressions are typed                                      I@15:14:39.504
PASS #14: BoundedChecker                                          I@15:14:39.526
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],scala.NotImplementedError: A set filter over PowSet[FinSet[Int]] is not implemented)
Unhandled exception                                               E@15:14:39.964
scala.NotImplementedError: A set filter over PowSet[FinSet[Int]] is not implemented
	at at.forsyte.apalache.tla.bmcmt.rules.SetFilterRule.apply(SetFilterRule.scala:29)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:336)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:367)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:401)
	at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.bindOperator(LetInRule.scala:44)
	at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.$anonfun$apply$1(LetInRule.scala:25)
	at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
	at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
	at scala.collection.immutable.List.foldLeft(List.scala:91)
	at at.forsyte.apalache.tla.bmcmt.rules.LetInRule.apply(LetInRule.scala:25)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:336)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:367)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:401)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.initializeConstants(TransitionExecutorImpl.scala:60)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.initializeConstants(FilteredTransitionExecutor.scala:96)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.initializeConstants(ConstrainedTransitionExecutor.scala:90)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:44)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:131)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:98)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:37)
	at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:187)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$3(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:322)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:45)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
It took me 0 days  0 hours  0 min  3 sec                          I@15:14:39.966
Total time: 3.398 sec                                             I@15:14:39.967
EXITCODE: ERROR (255)

Originally posted by @lemmy in #878 (comment)

@thpani thpani added the bug label Oct 19, 2023
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 <[email protected]>
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 <[email protected]>
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 <[email protected]>
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 <[email protected]>
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 <[email protected]>
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 <[email protected]>
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 <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant