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] Crash in Apalache on spec that works in TLC #914

Closed
jtremback opened this issue Jul 16, 2021 · 1 comment
Closed

[BUG] Crash in Apalache on spec that works in TLC #914

jtremback opened this issue Jul 16, 2021 · 1 comment
Labels
bug

Comments

@jtremback
Copy link

Description

This spec runs correctly on TLC, but crashes on Apalache:

jehan@Jehans-MBP payment_channel_spec % apalache-mc check --inv=Inv PaymentChannel.tla 
# Tool home: /usr/local
# Package:   /usr/local/mod-distribution/target//apalache-pkg-0.15.11-full.jar
# JVM args:  -Xmx4096m -DTLA-Library=/usr/local/src/tla
#
# APALACHE version 0.15.11 build 2803ef0
#
# 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=PaymentChannel.tla, init=, next=, inv=Inv I@08:30:01.674
Tuning:                                                           I@08:30:02.578
PASS #0: SanyParser                                               I@08:30:02.581
Parsing file /Users/jehan/projects/payment_channel_spec/PaymentChannel.tla
Parsing file /private/var/folders/2_/pkgctvg17xl4qcz4w739v5sc0000gn/T/Integers.tla
Parsing file /private/var/folders/2_/pkgctvg17xl4qcz4w739v5sc0000gn/T/TLC.tla
Parsing file /private/var/folders/2_/pkgctvg17xl4qcz4w739v5sc0000gn/T/Naturals.tla
Parsing file /private/var/folders/2_/pkgctvg17xl4qcz4w739v5sc0000gn/T/Sequences.tla
Parsing file /private/var/folders/2_/pkgctvg17xl4qcz4w739v5sc0000gn/T/FiniteSets.tla
PASS #1: TypeCheckerSnowcat                                       I@08:30:04.074
 > Running Snowcat .::.                                           I@08:30:04.074
 > Your types are great!                                          I@08:30:04.825
 > All expressions are typed                                      I@08:30:04.826
PASS #2: ConfigurationPass                                        I@08:30:05.346
  > PaymentChannel.cfg: Loading TLC configuration                 I@08:30:05.352
  > Using the init predicate Init from the TLC config             I@08:30:05.436
  > Using the next predicate Next from the TLC config             I@08:30:05.436
  > PaymentChannel.cfg: found INVARIANTS: Inv                     I@08:30:05.437
  > Overriding with command line arguments: --inv Inv             W@08:30:05.438
  > Set the initialization predicate to Init                      I@08:30:05.439
  > Set the transition predicate to Next                          I@08:30:05.440
  > Set an invariant to Inv                                       I@08:30:05.440
PASS #3: DesugarerPass                                            I@08:30:05.515
  > Desugaring...                                                 I@08:30:05.516
PASS #4: UnrollPass                                               I@08:30:05.578
  > Unroller                                                      I@08:30:05.629
PASS #5: InlinePass                                               I@08:30:05.716
  > InlinerOfUserOper                                             I@08:30:05.720
  > Wrap                                                          I@08:30:05.738
  > CallByNameOperatorEmbedder                                    I@08:30:05.741
  > LetInExpander                                                 I@08:30:05.743
  > Unwrap                                                        I@08:30:05.749
  > InlinerOfUserOper                                             I@08:30:05.751
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Inv, Next I@08:30:05.759
PASS #6: PrimingPass                                              I@08:30:05.814
  > Introducing InitPrimed for Init'                              I@08:30:05.817
PASS #7: VCGen                                                    I@08:30:05.860
  > Producing verification conditions from the invariant Inv      I@08:30:05.861
  > VCGen produced 4 verification condition(s)                    I@08:30:05.867
PASS #8: PreprocessingPass                                        I@08:30:05.933
  > Before preprocessing: unique renaming                         I@08:30:05.933
 > Applying standard transformations:                             I@08:30:05.937
  > PrimePropagation                                              I@08:30:05.938
  > Desugarer                                                     I@08:30:05.994
  > UniqueRenamer                                                 I@08:30:06.063
  > Normalizer                                                    I@08:30:06.147
  > Keramelizer                                                   I@08:30:06.198
  > After preprocessing: UniqueRenamer                            I@08:30:06.340
PASS #9: TransitionFinderPass                                     I@08:30:06.435
  > Found 1 initializing transitions                              I@08:30:06.448
  > Found 10 transitions                                          I@08:30:06.476
  > No constant initializer                                       I@08:30:06.477
  > Applying unique renaming                                      I@08:30:06.478
PASS #10: OptimizationPass                                        I@08:30:06.529
 > Applying optimizations:                                        I@08:30:06.534
  > ConstSimplifier                                               I@08:30:06.536
  > ExprOptimizer                                                 I@08:30:06.544
  > ConstSimplifier                                               I@08:30:06.552
PASS #11: AnalysisPass                                            I@08:30:06.586
 > Marking skolemizable existentials and sets to be expanded...   I@08:30:06.587
  > SkolemizationMarker                                           I@08:30:06.588
  > ExpansionMarker                                               I@08:30:06.589
 > Running analyzers...                                           I@08:30:06.595
  > Introduced expression grades                                  I@08:30:06.640
  > Introduced 21 formula hints                                   I@08:30:06.640
PASS #12: PostTypeCheckerSnowcat                                  I@08:30:06.641
 > Running Snowcat .::.                                           I@08:30:06.641
 > Your types are great!                                          I@08:30:07.131
 > All expressions are typed                                      I@08:30:07.132
PASS #13: BoundedChecker                                          I@08:30:07.200
State 0: Checking 4 state invariants                              I@08:30:09.123
Step 0: picking a transition out of 1 transition(s)               I@08:30:10.478
State 1: Checking 2 state invariants                              I@08:30:10.513
State 1: Checking 1 state invariants                              I@08:30:11.185
State 1: Checking 1 state invariants                              I@08:30:11.317
State 1: Checking 1 state invariants                              I@08:30:11.588
Step 1: Transition #7 is disabled                                 I@08:30:11.803
Step 1: Transition #9 is disabled                                 I@08:30:11.810
Step 1: picking a transition out of 4 transition(s)               I@08:30:11.810
State 2: Checking 2 state invariants                              I@08:30:11.866
State 2: Checking 1 state invariants                              I@08:30:12.334
State 2: Checking 3 state invariants                              I@08:30:12.448
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],java.lang.IndexOutOfBoundsException: 4)
Unhandled exception                                               E@08:30:12.536
java.lang.IndexOutOfBoundsException: 4
	at scala.collection.LinearSeqOptimized.apply(LinearSeqOptimized.scala:67)
	at scala.collection.LinearSeqOptimized.apply$(LinearSeqOptimized.scala:65)
	at scala.collection.immutable.List.apply(List.scala:91)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.keyEq$1(LazyEquality.scala:432)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.$anonfun$mkRecordEq$1(LazyEquality.scala:448)
	at scala.collection.immutable.List.map(List.scala:297)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkRecordEq(LazyEquality.scala:448)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:145)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.makeOne$1(LazyEquality.scala:101)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.$anonfun$cacheEqConstraints$2(LazyEquality.scala:104)
	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.LazyEquality.cacheEqConstraints(LazyEquality.scala:104)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.subsetEq(LazyEquality.scala:309)
	at at.forsyte.apalache.tla.bmcmt.rules.SetInclusionRule.apply(SetInclusionRule.scala:37)
	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.NegRule.apply(NegRule.scala:28)
	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.assertState(TransitionExecutorImpl.scala:196)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.assertState(FilteredTransitionExecutor.scala:88)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.assertState(ConstrainedTransitionExecutor.scala:102)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2(SeqModelChecker.scala:267)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2$adapted(SeqModelChecker.scala:255)
	at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.checkInvariants(SeqModelChecker.scala:255)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6(SeqModelChecker.scala:177)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6$adapted(SeqModelChecker.scala:141)
	at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:141)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:63)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:51)
	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 11 sec                          I@08:30:12.537
Total time: 11.22 sec                                             I@08:30:12.537
EXITCODE: ERROR (255)

Input specification

https://github.com/jtremback/payment_channel_spec/tree/cc9d55a8c2e5102462be69b14d8832860d2b327e

The command line parameters used to run the tool

apalache-mc check --inv=Inv PaymentChannel.tla

Expected behavior

Spec should run, with failing invariant.

Log files

08:33:16.662 [main] INFO  a.f.a.t.Tool$ - Checker options: filename=PaymentChannel.tla, init=, next=, inv=Inv
08:33:17.641 [main] INFO  a.f.a.t.Tool$ - Tuning: 
08:33:17.647 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
08:33:19.044 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
08:33:19.046 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
08:33:19.046 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
08:33:19.135 [main] DEBUG a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > JSON output: /Users/jehan/projects/payment_channel_spec/x/08.33-16.07.2021-1662615525926948631/out-pre-TypeCheckerSnowcat.json
08:33:19.795 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Your types are great!
08:33:19.796 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > All expressions are typed
08:33:20.239 [main] DEBUG a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > JSON output: /Users/jehan/projects/payment_channel_spec/x/08.33-16.07.2021-1662615525926948631/out-post-TypeCheckerSnowcat.json
08:33:20.331 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
08:33:20.333 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
08:33:20.339 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > PaymentChannel.cfg: Loading TLC configuration
08:33:20.419 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Using the init predicate Init from the TLC config
08:33:20.419 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Using the next predicate Next from the TLC config
08:33:20.421 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > PaymentChannel.cfg: found INVARIANTS: Inv
08:33:20.421 [main] WARN  a.f.a.t.p.p.ConfigurationPassImpl -   > Overriding with command line arguments: --inv Inv
08:33:20.422 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
08:33:20.423 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
08:33:20.423 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to Inv
08:33:20.492 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
08:33:20.492 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
08:33:20.493 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
08:33:20.554 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
08:33:20.557 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #4: UnrollPass
08:33:20.612 [main] INFO  a.f.a.t.p.p.UnrollPassImpl -   > Unroller
08:33:20.698 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: UnrollPass [OK]
08:33:20.701 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #5: InlinePass
08:33:20.703 [main] INFO  a.f.a.t.p.p.InlinePassImpl -   > InlinerOfUserOper
08:33:20.719 [main] INFO  a.f.a.t.p.p.InlinePassImpl -   > Wrap
08:33:20.722 [main] INFO  a.f.a.t.p.p.InlinePassImpl -   > CallByNameOperatorEmbedder
08:33:20.724 [main] INFO  a.f.a.t.p.p.InlinePassImpl -   > LetInExpander
08:33:20.730 [main] INFO  a.f.a.t.p.p.InlinePassImpl -   > Unwrap
08:33:20.732 [main] INFO  a.f.a.t.p.p.InlinePassImpl -   > InlinerOfUserOper
08:33:20.737 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Inv, Next
08:33:20.793 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: InlinePass [OK]
08:33:20.794 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #6: PrimingPass
08:33:20.795 [main] INFO  a.f.a.t.a.p.PrimingPassImpl -   > Introducing InitPrimed for Init'
08:33:20.841 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: PrimingPass [OK]
08:33:20.842 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #7: VCGen
08:33:20.842 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant Inv
08:33:20.847 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 4 verification condition(s)
08:33:20.904 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: VCGen [OK]
08:33:20.905 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #8: PreprocessingPass
08:33:20.906 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
08:33:20.910 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
08:33:20.910 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
08:33:20.957 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
08:33:21.022 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
08:33:21.099 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
08:33:21.150 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
08:33:21.260 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
08:33:21.361 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: PreprocessingPass [OK]
08:33:21.362 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #9: TransitionFinderPass
08:33:21.376 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 initializing transitions
08:33:21.404 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 10 transitions
08:33:21.405 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > No constant initializer
08:33:21.406 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Applying unique renaming
08:33:21.473 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: TransitionFinderPass [OK]
08:33:21.474 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #10: OptimizationPass
08:33:21.477 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
08:33:21.477 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
08:33:21.486 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
08:33:21.495 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
08:33:21.536 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: OptimizationPass [OK]
08:33:21.537 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #11: AnalysisPass
08:33:21.538 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
08:33:21.538 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > SkolemizationMarker
08:33:21.540 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > ExpansionMarker
08:33:21.546 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
08:33:21.599 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
08:33:21.599 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced 21 formula hints
08:33:21.599 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: AnalysisPass [OK]
08:33:21.600 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #12: PostTypeCheckerSnowcat
08:33:21.600 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Running Snowcat .::.
08:33:21.616 [main] DEBUG a.f.a.t.b.p.PostTypeCheckerPassImpl -  > JSON output: /Users/jehan/projects/payment_channel_spec/x/08.33-16.07.2021-1662615525926948631/out-pre-PostTypeCheckerSnowcat.json
08:33:22.078 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Your types are great!
08:33:22.078 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > All expressions are typed
08:33:22.107 [main] DEBUG a.f.a.t.b.p.PostTypeCheckerPassImpl -  > JSON output: /Users/jehan/projects/payment_channel_spec/x/08.33-16.07.2021-1662615525926948631/out-post-PostTypeCheckerSnowcat.json
08:33:22.135 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #12: PostTypeCheckerSnowcat [OK]
08:33:22.136 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #13: BoundedChecker
08:33:23.938 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
08:33:23.942 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:24.143 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
08:33:24.146 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
08:33:24.147 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: Checking 4 state invariants
08:33:24.148 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 0
08:33:24.163 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 1
08:33:24.701 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 2
08:33:25.426 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 3
08:33:25.479 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
08:33:25.502 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
08:33:25.502 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:25.563 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0. Is it enabled?
08:33:25.565 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0 is enabled
08:33:25.565 [main] INFO  a.f.a.t.b.SeqModelChecker - State 1: Checking 2 state invariants
08:33:25.565 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 1
08:33:25.809 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 2
08:33:26.171 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #1
08:33:26.171 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.186 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #1. Is it enabled?
08:33:26.186 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #1 is enabled
08:33:26.186 [main] INFO  a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
08:33:26.186 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 1
08:33:26.296 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #2
08:33:26.296 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.303 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Transition 2 produces partial assignment. Disabled.
08:33:26.303 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #3
08:33:26.303 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.307 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Transition 3 produces partial assignment. Disabled.
08:33:26.307 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #4
08:33:26.307 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.314 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #4. Is it enabled?
08:33:26.314 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #4 is enabled
08:33:26.314 [main] INFO  a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
08:33:26.314 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 1
08:33:26.530 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #5
08:33:26.530 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.537 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #5. Is it enabled?
08:33:26.537 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #5 is enabled
08:33:26.537 [main] INFO  a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
08:33:26.537 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 1
08:33:26.726 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #6
08:33:26.727 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.729 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Transition 6 produces partial assignment. Disabled.
08:33:26.729 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #7
08:33:26.729 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.739 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #7. Is it enabled?
08:33:26.739 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 1: Transition #7 is disabled
08:33:26.739 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #8
08:33:26.740 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.742 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Transition 8 produces partial assignment. Disabled.
08:33:26.742 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #9
08:33:26.742 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.745 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #9. Is it enabled?
08:33:26.745 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 1: Transition #9 is disabled
08:33:26.745 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 1: picking a transition out of 4 transition(s)
08:33:26.797 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #0
08:33:26.797 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:26.803 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #0. Is it enabled?
08:33:26.803 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #0 is enabled
08:33:26.803 [main] INFO  a.f.a.t.b.SeqModelChecker - State 2: Checking 2 state invariants
08:33:26.803 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 1
08:33:27.011 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 2
08:33:27.310 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #1
08:33:27.310 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:27.314 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #1. Is it enabled?
08:33:27.314 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #1 is enabled
08:33:27.314 [main] INFO  a.f.a.t.b.SeqModelChecker - State 2: Checking 1 state invariants
08:33:27.314 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 1
08:33:27.541 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #2
08:33:27.543 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
08:33:27.601 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #2. Is it enabled?
08:33:27.601 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #2 is enabled
08:33:27.601 [main] INFO  a.f.a.t.b.SeqModelChecker - State 2: Checking 3 state invariants
08:33:27.601 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 1
08:33:27.691 [main] ERROR a.f.a.t.Tool$ - Unhandled exception
java.lang.IndexOutOfBoundsException: 4
	at scala.collection.LinearSeqOptimized.apply(LinearSeqOptimized.scala:67)
	at scala.collection.LinearSeqOptimized.apply$(LinearSeqOptimized.scala:65)
	at scala.collection.immutable.List.apply(List.scala:91)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.keyEq$1(LazyEquality.scala:432)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.$anonfun$mkRecordEq$1(LazyEquality.scala:448)
	at scala.collection.immutable.List.map(List.scala:297)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.mkRecordEq(LazyEquality.scala:448)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.cacheOneEqConstraint(LazyEquality.scala:145)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.makeOne$1(LazyEquality.scala:101)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.$anonfun$cacheEqConstraints$2(LazyEquality.scala:104)
	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.LazyEquality.cacheEqConstraints(LazyEquality.scala:104)
	at at.forsyte.apalache.tla.bmcmt.LazyEquality.subsetEq(LazyEquality.scala:309)
	at at.forsyte.apalache.tla.bmcmt.rules.SetInclusionRule.apply(SetInclusionRule.scala:37)
	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.NegRule.apply(NegRule.scala:28)
	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.assertState(TransitionExecutorImpl.scala:196)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.assertState(FilteredTransitionExecutor.scala:88)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.assertState(ConstrainedTransitionExecutor.scala:102)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2(SeqModelChecker.scala:267)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$checkInvariants$2$adapted(SeqModelChecker.scala:255)
	at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.checkInvariants(SeqModelChecker.scala:255)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6(SeqModelChecker.scala:177)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.$anonfun$prepareTransitionsAndCheckInvariants$6$adapted(SeqModelChecker.scala:141)
	at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:985)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:984)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:141)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:63)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:51)
	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)
08:33:27.692 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min 11 sec
08:33:27.692 [main] INFO  a.f.a.t.Tool$ - Total time: 11.180 sec

System information

% apalache-mc version  
# Tool home: /usr/local
# Package:   /usr/local/mod-distribution/target//apalache-pkg-0.15.11-full.jar
# JVM args:  -Xmx4096m -DTLA-Library=/usr/local/src/tla
#
# APALACHE version 0.15.11 build 2803ef0
#
# 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.

0.15.11 build 2803ef0
EXITCODE: OK

macOS Big Sur, Apple M1 chip.

It is running the x86 version of OpenJDK through the Rosetta translation layer (I believe): #751 (comment)

% java --version
openjdk 16.0.1 2021-04-20
OpenJDK Runtime Environment Zulu16.30+15-CA (build 16.0.1+9)
OpenJDK 64-Bit Server VM Zulu16.30+15-CA (build 16.0.1+9, mixed mode, sharing)
@jtremback jtremback added the bug label Jul 16, 2021
@shonfeder shonfeder mentioned this issue Jul 18, 2021
Closed
@shonfeder
Copy link
Contributor

shonfeder commented Jul 19, 2021 •
edited
Loading

I haven't been able to come up with a minimal reproduction case so far, or determine exactly where we are in the spec when we hit the error, but I think I've at least manged to determine the gist of the problem.

The out of bounds error is getting hit on the second to last line here, when trying to access the leftElem from the letRec:

https://github.com/informalsystems/apalache/blob/858281ea1ee3c31cee7c275fd58b5f0711db1aac/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala#L429-L433

We're using typing information to determine which fields to access when building the record equality expression, and the typing info is leading the indexing astray, because we don't have a field corresponding to the type.

Via printf debugging, I've been able to see the types of the two records being compared:

The left record:

Map(balance -> Int, lastUpdate -> Record["balance" -> Int, "seq" -> Int, "type" -> Const], receiverSig -> Bool, senderSig -> Bool, seq -> Int, type -> Const)

And the right:

Map(balance -> Int, receiverSig -> Bool, senderSig -> Bool, seq -> Int, type -> Const)

I'll put together a simple fix, tho I'm not 100% sure it's the correct approach, and we'll want a minimal reproduction case for a regression test before merging.

iiuc, given our (unsound) typing rules for records, these are of the same type, so it's not directly related to #915.

shonfeder pushed a commit that referenced this issue Jul 19, 2021
Shallow "fix" for #914
d0ce48b 
An exploratory fix, to probe the problem, and get feedback.
@shonfeder shonfeder mentioned this issue Jul 19, 2021
Merged
shonfeder pushed a commit that referenced this issue Aug 23, 2021
Shallow "fix" for #914
85394f0 
An exploratory fix, to probe the problem, and get feedback.
shonfeder pushed a commit that referenced this issue Aug 23, 2021
Add regression test for #914
503f763
shonfeder pushed a commit that referenced this issue Aug 27, 2021
Shallow "fix" for #914
97d5b87 
An exploratory fix, to probe the problem, and get feedback.
shonfeder pushed a commit that referenced this issue Aug 27, 2021
Add regression test for #914
a483617
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jtremback @shonfeder