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.

Sign up for GitHub

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

Jump to bottom

[BUG] Bogus violation with ConstInit and SUBSET (A set filter over PowSet[FinSet[Int]] is not implemented) #878

Closed
lemmy opened this issue Jun 23, 2021 · 2 comments
Closed

[BUG] Bogus violation with ConstInit and SUBSET (A set filter over PowSet[FinSet[Int]] is not implemented) #878

lemmy opened this issue Jun 23, 2021 · 2 comments
Labels
bug product-owner-triage This should be triaged by the product owner

Comments

@lemmy
Copy link
Contributor

lemmy commented Jun 23, 2021 •
edited
Loading 

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

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

ConstInit ==
    S \in ( (SUBSET {1,2}) \ {{}} )

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

Init ==
    x = S

Next ==
    UNCHANGED x

Inv ==
    x # {}
==========================
@!@!@STARTMSG 2262:0 @!@!@
Created by Apalache on Wed Jun 23 15:12:46 PDT 2021
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2110:1 @!@!@
Invariant is violated.
@!@!@ENDMSG 2110 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ S = {}
/\ 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:08:46.696
Tuning:                                                           I@15:08:47.190
PASS #0: SanyParser                                               I@15:08:47.194
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:08:47.945
 > Running Snowcat .::.                                           I@15:08:47.945
 > Your types are great!                                          I@15:08:48.073
 > All expressions are typed                                      I@15:08:48.073
PASS #2: ConfigurationPass                                        I@15:08:48.115
  > Foo: Loading TLC configuration                                I@15:08:48.119
  > No TLC configuration found. Skipping.                         I@15:08:48.126
  > Command line option --init is not set. Using Init             I@15:08:48.126
  > Command line option --next is not set. Using Next             I@15:08:48.126
  > Set the initialization predicate to Init                      I@15:08:48.126
  > Set the constant initialization predicate to ConstInit        I@15:08:48.127
  > Set the transition predicate to Next                          I@15:08:48.127
  > Set an invariant to Inv                                       I@15:08:48.128
PASS #3: DesugarerPass                                            I@15:08:48.167
  > Desugaring...                                                 I@15:08:48.168
PASS #4: UnrollPass                                               I@15:08:48.204
  > Unroller                                                      I@15:08:48.223
PASS #5: PrimingPass                                              I@15:08:48.285
  > Introducing ConstInitPrimed for ConstInit'                    I@15:08:48.293
  > Introducing InitPrimed for Init'                              I@15:08:48.299
PASS #6: CoverAnalysisPass                                        I@15:08:48.354
PASS #7: InlinePass                                               I@15:08:48.356
  > InlinerOfUserOper                                             I@15:08:48.359
  > LetInExpander                                                 I@15:08:48.360
  > FoldOperLetinizer                                             I@15:08:48.361
  > InlinerOfUserOper                                             I@15:08:48.363
Leaving only relevant operators: ConstInit, ConstInitPrimed, Init, InitPrimed, Inv, Next I@15:08:48.367
PASS #8: VCGen                                                    I@15:08:48.423
  > Producing verification conditions from the invariant Inv      I@15:08:48.425
  > VCGen produced 1 verification condition(s)                    I@15:08:48.434
PASS #9: PreprocessingPass                                        I@15:08:48.459
  > Before preprocessing: unique renaming                         I@15:08:48.459
 > Applying standard transformations:                             I@15:08:48.471
  > PrimePropagation                                              I@15:08:48.481
  > Desugarer                                                     I@15:08:48.500
  > UniqueRenamer                                                 I@15:08:48.518
  > Normalizer                                                    I@15:08:48.542
  > Keramelizer                                                   I@15:08:48.568
  > After preprocessing: UniqueRenamer                            I@15:08:48.601
PASS #10: TransitionFinderPass                                    I@15:08:48.657
  > Found 1 initializing transitions                              I@15:08:48.688
  > Found 1 transitions                                           I@15:08:48.695
  > Found constant initializer ConstInit                          I@15:08:48.696
  > Applying unique renaming                                      I@15:08:48.702
PASS #11: OptimizationPass                                        I@15:08:48.733
 > Applying optimizations:                                        I@15:08:48.761
  > ConstSimplifier                                               I@15:08:48.762
  > ExprOptimizer                                                 I@15:08:48.776
  > ConstSimplifier                                               I@15:08:48.814
PASS #12: AnalysisPass                                            I@15:08:48.881
 > Marking skolemizable existentials and sets to be expanded...   I@15:08:48.886
  > SkolemizationMarker                                           I@15:08:48.888
  > ExpansionMarker                                               I@15:08:48.893
 > Running analyzers...                                           I@15:08:48.920
  > Introduced expression grades                                  I@15:08:48.996
  > Introduced 0 formula hints                                    I@15:08:49.012
PASS #13: PostTypeCheckerSnowcat                                  I@15:08:49.013
 > Running Snowcat .::.                                           I@15:08:49.013
 > Your types are great!                                          I@15:08:49.203
 > All expressions are typed                                      I@15:08:49.204
PASS #14: BoundedChecker                                          I@15:08:49.299
State 0: Checking 1 state invariants                              I@15:08:49.994
State 0: state invariant 0 violated. Check the counterexample in: counterexample1.tla, MC1.out, counterexample1.json E@15:08:50.053
Found 1 error(s)                                                  I@15:08:50.060
The outcome is: Error                                             I@15:08:50.061
Checker has found an error                                        I@15:08:50.061
It took me 0 days  0 hours  0 min  3 sec                          I@15:08:50.062
Total time: 3.448 sec                                             I@15:08:50.062
EXITCODE: ERROR (12)
@lemmy lemmy added the bug label Jun 23, 2021
@lemmy
Copy link
Contributor Author

lemmy commented Jun 23, 2021 

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

@lemmy lemmy changed the title [BUG] Bogus violation with ConstInit and SUBSET [BUG] Bogus violation with ConstInit and SUBSET (A set filter over PowSet[FinSet[Int]] is not implemented) Jun 23, 2021
lemmy referenced this issue in lemmy/BlockingQueue Jun 23, 2021
@lemmy
Spec compatible with Apalache 0.15.9-SNAPSHOT
6392bcb
@konnov konnov self-assigned this Jun 25, 2021
@konnov konnov added this to the July iteration milestone Jun 25, 2021
@konnov konnov added the product-owner-triage This should be triaged by the product owner label Jul 13, 2022
@konnov konnov removed their assignment Jul 13, 2022
@thpani thpani mentioned this issue Oct 19, 2023
Open
@thpani
Copy link
Collaborator

thpani commented Oct 19, 2023

The first issue appears to be fixed in v0.43.0-36-g2f8848485.

I've spawned #2762 for the second issue, closing this one.

@thpani thpani closed this as completed Oct 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug product-owner-triage This should be triaged by the product owner
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@thpani @lemmy @konnov @shonfeder