search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
427 stars 40 forks source link

[BUG] rewriter error: Expected a constant integer range in .., found 0..tpos #425

Closed lemmy closed 2 years ago

lemmy commented 3 years ago

Spec/Model from https://github.com/tlaplus/Examples/tree/master/specifications/ewd840

markus@avocado:/tmp/apalache(unstable)$ bin/apalache-mc check --length=24 /home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla 
# Tool home: /tmp/apalache
# Package:   /tmp/apalache/mod-distribution/target/apalache-pkg-0.8.1-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/tmp/apalache/src/tla
#
# APALACHE version 0.8.1-SNAPSHOT build v0.7.2-117-g9e40275
#
# 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=/home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla, init=, next=, inv= I@09:39:05.709
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/tmp/apalache/mod-distribution/target/apalache-pkg-0.8.1-SNAPSHOT-full.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
PASS #0: SanyParser                                               I@09:39:06.223
Parsing file /home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla
Parsing file /tmp/Naturals.tla
PASS #1: ConfigurationPass                                        I@09:39:06.881
  > EWD840.cfg: Loading TLC configuration                         I@09:39:06.884
  > Using the init predicate Init from the TLC config             I@09:39:06.970
  > Using the next predicate Next from the TLC config             I@09:39:06.970
  > EWD840.cfg: found INVARIANTS: Inv                             I@09:39:06.970
  > Set the initialization predicate to Init                      I@09:39:06.974
  > Set the transition predicate to Next                          I@09:39:06.974
  > Set an invariant to Inv                                       I@09:39:06.975
  > Replaced CONSTANT N with 8                                    I@09:39:06.977
PASS #2: UnrollPass                                               I@09:39:07.039
  > Unroller                                                      I@09:39:07.089
PASS #3: PrimingPass                                              I@09:39:07.120
  > Introducing InitPrimed for Init'                              I@09:39:07.124
PASS #4: CoverAnalysisPass                                        I@09:39:07.151
PASS #5: InlinePass                                               I@09:39:07.151
  > InlinerOfUserOper                                             I@09:39:07.157
  > LetInExpander                                                 I@09:39:07.195
  > InlinerOfUserOper                                             I@09:39:07.204
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Inv, Next I@09:39:07.210
PASS #6: VCGen                                                    I@09:39:07.226
  > Producing verification conditions from the invariant Inv      I@09:39:07.227
  > VCGen produced 1 verification condition(s)                    I@09:39:07.229
PASS #7: PreprocessingPass                                        I@09:39:07.265
  > Before preprocessing: unique renaming                         I@09:39:07.265
 > Applying standard transformations:                             I@09:39:07.275
  > Desugarer                                                     I@09:39:07.277
  > UniqueRenamer                                                 I@09:39:07.319
  > Normalizer                                                    I@09:39:07.356
  > Keramelizer                                                   I@09:39:07.378
  > After preprocessing: UniqueRenamer                            I@09:39:07.416
PASS #8: TransitionFinderPass                                     I@09:39:07.461
  > Found 1 initializing transitions                              I@09:39:07.543
  > Found 4 transitions                                           I@09:39:07.579
  > No constant initializer                                       I@09:39:07.579
  > Applying unique renaming                                      I@09:39:07.581
PASS #9: OptimizationPass                                         I@09:39:07.605
 > Applying optimizations:                                        I@09:39:07.611
  > ConstSimplifier                                               I@09:39:07.612
  > ExprOptimizer                                                 I@09:39:07.625
  > ConstSimplifier                                               I@09:39:07.635
PASS #10: AnalysisPass                                            I@09:39:07.659
 > Marking skolemizable existentials and sets to be expanded...   I@09:39:07.661
  > SkolemizationMarker                                           I@09:39:07.662
  > ExpansionMarker                                               I@09:39:07.664
 > Running analyzers...                                           I@09:39:07.671
  > Introduced expression grades                                  I@09:39:07.690
  > Introduced 3 formula hints                                    I@09:39:07.691
PASS #11: BoundedChecker                                          I@09:39:07.691
No CONSTANT initializer given                                     I@09:39:07.945
Step 0, level 0: checking if 1 transition(s) are enabled and violate the invariant I@09:39:07.951
The problem occurs around the source location EWD840.tla:155:11-155:49 E@09:39:08.242
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],at.forsyte.apalache.tla.bmcmt.RewriterException: Expected a constant integer range in .., found 0..tpos)
EWD840.tla:155:11-155:49: rewriter error: Expected a constant integer range in .., found 0..tpos E@09:39:08.249
at.forsyte.apalache.tla.bmcmt.RewriterException: Expected a constant integer range in .., found 0..tpos
    at at.forsyte.apalache.tla.bmcmt.rules.IntDotDotRule.getRange(IntDotDotRule.scala:51)
    at at.forsyte.apalache.tla.bmcmt.rules.IntDotDotRule.apply(IntDotDotRule.scala:32)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:345)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:374)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:405)
    at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.expandExistsOrForall(QuantRule.scala:98)
    at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:68)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:345)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:374)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:405)
    at at.forsyte.apalache.tla.bmcmt.rules.LabelRule.apply(LabelRule.scala:23)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:345)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:374)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:405)
    at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg$1(AndRule.scala:72)
    at at.forsyte.apalache.tla.bmcmt.rules.AndRule.$anonfun$apply$2(AndRule.scala:76)
    at scala.collection.immutable.List.map(List.scala:297)
    at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:76)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:345)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:374)
    at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:405)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.checkOneInvariant(ModelChecker.scala:495)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.$anonfun$checkAllInvariants$3(ModelChecker.scala:480)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.$anonfun$checkAllInvariants$3$adapted(ModelChecker.scala:465)
    at scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:924)
    at scala.collection.immutable.List.foreach(List.scala:431)
    at scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:923)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.checkAllInvariants(ModelChecker.scala:465)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.applyTransition(ModelChecker.scala:402)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.filterEnabled$1(ModelChecker.scala:229)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.findEnabledOrBugs(ModelChecker.scala:238)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.applySearchStrategy(ModelChecker.scala:196)
    at at.forsyte.apalache.tla.bmcmt.ModelChecker.run(ModelChecker.scala:114)
    at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:81)
    at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:23)
    at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:38)
    at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:172)
    at at.forsyte.apalache.tla.Tool$.$anonfun$run$2(Tool.scala:94)
    at at.forsyte.apalache.tla.Tool$.$anonfun$run$2$adapted(Tool.scala:94)
    at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:234)
    at at.forsyte.apalache.tla.Tool$.run(Tool.scala:94)
    at at.forsyte.apalache.tla.Tool$.main(Tool.scala:46)
    at at.forsyte.apalache.tla.Tool.main(Tool.scala)
It took me 0 days  0 hours  0 min  2 sec                          I@09:39:08.250
Total time: 2.545 sec                                             I@09:39:08.251
EXITCODE: ERROR (99)

FWIW: For N=8, TLC finishes in 40s whereas Apalache finishes in 175s (ignoring Inv).

markus@avocado:/tmp/apalache(unstable)$ bin/apalache-mc check --length=24 /home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla 
# Tool home: /tmp/apalache
# Package:   /tmp/apalache/mod-distribution/target/apalache-pkg-0.8.1-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/tmp/apalache/src/tla
#
# APALACHE version 0.8.1-SNAPSHOT build v0.7.2-117-g9e40275
#
# 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=/home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla, init=, next=, inv= I@09:39:18.326
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/tmp/apalache/mod-distribution/target/apalache-pkg-0.8.1-SNAPSHOT-full.jar) to method java.lang.ClassLoader.defineClass(java.lang.String,byte[],int,int,java.security.ProtectionDomain)
WARNING: Please consider reporting this to the maintainers of com.google.inject.internal.cglib.core.$ReflectUtils$1
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release
PASS #0: SanyParser                                               I@09:39:18.954
Parsing file /home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla
Parsing file /tmp/Naturals.tla
PASS #1: ConfigurationPass                                        I@09:39:19.647
  > EWD840.cfg: Loading TLC configuration                         I@09:39:19.650
  > Using the init predicate Init from the TLC config             I@09:39:19.747
  > Using the next predicate Next from the TLC config             I@09:39:19.748
  > Set the initialization predicate to Init                      I@09:39:19.752
  > Set the transition predicate to Next                          I@09:39:19.752
  > Replaced CONSTANT N with 8                                    I@09:39:19.754
PASS #2: UnrollPass                                               I@09:39:19.812
  > Unroller                                                      I@09:39:19.870
PASS #3: PrimingPass                                              I@09:39:19.903
  > Introducing InitPrimed for Init'                              I@09:39:19.910
PASS #4: CoverAnalysisPass                                        I@09:39:19.941
PASS #5: InlinePass                                               I@09:39:19.942
  > InlinerOfUserOper                                             I@09:39:19.952
  > LetInExpander                                                 I@09:39:19.992
  > InlinerOfUserOper                                             I@09:39:20.000
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@09:39:20.005
PASS #6: VCGen                                                    I@09:39:20.019
  > No invariant given. Only deadlocks will be checked            I@09:39:20.020
PASS #7: PreprocessingPass                                        I@09:39:20.030
  > Before preprocessing: unique renaming                         I@09:39:20.031
 > Applying standard transformations:                             I@09:39:20.043
  > Desugarer                                                     I@09:39:20.044
  > UniqueRenamer                                                 I@09:39:20.063
  > Normalizer                                                    I@09:39:20.088
  > Keramelizer                                                   I@09:39:20.104
  > After preprocessing: UniqueRenamer                            I@09:39:20.124
PASS #8: TransitionFinderPass                                     I@09:39:20.144
  > Found 1 initializing transitions                              I@09:39:20.184
  > Found 4 transitions                                           I@09:39:20.212
  > No constant initializer                                       I@09:39:20.213
  > Applying unique renaming                                      I@09:39:20.214
PASS #9: OptimizationPass                                         I@09:39:20.235
 > Applying optimizations:                                        I@09:39:20.239
  > ConstSimplifier                                               I@09:39:20.240
  > ExprOptimizer                                                 I@09:39:20.246
  > ConstSimplifier                                               I@09:39:20.253
PASS #10: AnalysisPass                                            I@09:39:20.268
 > Marking skolemizable existentials and sets to be expanded...   I@09:39:20.270
  > SkolemizationMarker                                           I@09:39:20.271
  > ExpansionMarker                                               I@09:39:20.273
 > Running analyzers...                                           I@09:39:20.278
  > Introduced expression grades                                  I@09:39:20.296
  > Introduced 2 formula hints                                    I@09:39:20.296
PASS #11: BoundedChecker                                          I@09:39:20.296
No CONSTANT initializer given                                     I@09:39:20.514
Step 0, level 0: checking if 1 transition(s) are enabled and violate the invariant I@09:39:20.518
Step 0, level 1: collecting 1 enabled transition(s)               I@09:39:20.710
Step 1, level 1: checking if 4 transition(s) are enabled and violate the invariant I@09:39:20.764
Step 1, level 2: collecting 4 enabled transition(s)               I@09:39:21.062
Step 2, level 2: checking if 4 transition(s) are enabled and violate the invariant I@09:39:21.245
Step 2, level 3: collecting 4 enabled transition(s)               I@09:39:21.403
Step 3, level 3: checking if 4 transition(s) are enabled and violate the invariant I@09:39:21.517
Step 3, level 4: collecting 4 enabled transition(s)               I@09:39:21.664
Step 4, level 4: checking if 4 transition(s) are enabled and violate the invariant I@09:39:21.800
Step 4, level 5: collecting 4 enabled transition(s)               I@09:39:21.957
Step 5, level 5: checking if 4 transition(s) are enabled and violate the invariant I@09:39:22.051
Step 5, level 6: collecting 4 enabled transition(s)               I@09:39:22.211
Step 6, level 6: checking if 4 transition(s) are enabled and violate the invariant I@09:39:22.281
Step 6, level 7: collecting 4 enabled transition(s)               I@09:39:22.501
Step 7, level 7: checking if 4 transition(s) are enabled and violate the invariant I@09:39:22.567
Step 7, level 8: collecting 4 enabled transition(s)               I@09:39:22.883
Step 8, level 8: checking if 4 transition(s) are enabled and violate the invariant I@09:39:22.943
Step 8, level 9: collecting 4 enabled transition(s)               I@09:39:23.235
Step 9, level 9: checking if 4 transition(s) are enabled and violate the invariant I@09:39:23.291
Step 9, level 10: collecting 4 enabled transition(s)              I@09:39:23.544
Step 10, level 10: checking if 4 transition(s) are enabled and violate the invariant I@09:39:23.587
Step 10, level 11: collecting 4 enabled transition(s)             I@09:39:24.335
Step 11, level 11: checking if 4 transition(s) are enabled and violate the invariant I@09:39:24.377
Step 11, level 12: collecting 4 enabled transition(s)             I@09:39:25.103
Step 12, level 12: checking if 4 transition(s) are enabled and violate the invariant I@09:39:25.140
Step 12, level 13: collecting 4 enabled transition(s)             I@09:39:25.503
Step 13, level 13: checking if 4 transition(s) are enabled and violate the invariant I@09:39:25.549
Step 13, level 14: collecting 4 enabled transition(s)             I@09:39:26.475
Step 14, level 14: checking if 4 transition(s) are enabled and violate the invariant I@09:39:26.513
Step 14, level 15: collecting 4 enabled transition(s)             I@09:39:30.102
Step 15, level 15: checking if 4 transition(s) are enabled and violate the invariant I@09:39:30.129
Step 15, level 16: collecting 4 enabled transition(s)             I@09:39:33.116
Step 16, level 16: checking if 4 transition(s) are enabled and violate the invariant I@09:39:33.143
Step 16, level 17: collecting 4 enabled transition(s)             I@09:39:40.097
Step 17, level 17: checking if 4 transition(s) are enabled and violate the invariant I@09:39:40.137
Step 17, level 18: collecting 4 enabled transition(s)             I@09:39:45.853
Step 18, level 18: checking if 4 transition(s) are enabled and violate the invariant I@09:39:45.884
Step 18, level 19: collecting 4 enabled transition(s)             I@09:39:59.863
Step 19, level 19: checking if 4 transition(s) are enabled and violate the invariant I@09:39:59.921
Step 19, level 20: collecting 4 enabled transition(s)             I@09:40:15.842
Step 20, level 20: checking if 4 transition(s) are enabled and violate the invariant I@09:40:15.876
Step 20, level 21: collecting 4 enabled transition(s)             I@09:40:39.821
Step 21, level 21: checking if 4 transition(s) are enabled and violate the invariant I@09:40:39.860
Step 21, level 22: collecting 4 enabled transition(s)             I@09:40:53.695
Step 22, level 22: checking if 4 transition(s) are enabled and violate the invariant I@09:40:53.735
Step 22, level 23: collecting 4 enabled transition(s)             I@09:41:21.245
Step 23, level 23: checking if 4 transition(s) are enabled and violate the invariant I@09:41:21.320
Step 23, level 24: collecting 4 enabled transition(s)             I@09:41:44.612
Step 24, level 24: checking if 4 transition(s) are enabled and violate the invariant I@09:41:44.643
Step 24, level 25: collecting 4 enabled transition(s)             I@09:42:13.275
The outcome is: NoError                                           I@09:42:13.351
PASS #12: Terminal                                                I@09:42:13.352
Checker reports no error up to computation length 24              I@09:42:13.352
It took me 0 days  0 hours  2 min 55 sec                          I@09:42:13.352
Total time: 175.29 sec                                            I@09:42:13.352
EXITCODE: OK
markus@avocado:/tmp/apalache(unstable)$ /opt/toolbox/tla2tools.jar -deadlock /home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840
TLC2 Version 2.15 of Day Month 20?? (rev: 70a5e5d)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 110 and seed 929847063396399017 with 1 worker on 4 cores with 5952MB heap and 64MB offheap memory [pid: 690992] (Linux 5.4.0-58-generic amd64, Ubuntu 11.0.9.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/examples/specifications/ewd840/EWD840.tla
Parsing file /tmp/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module EWD840
Starting... (2021-01-11 09:37:31)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Computed 256 initial states...
Computed 512 initial states...
Computed 1024 initial states...
Computed 2048 initial states...
Computed 4096 initial states...
Computed 8192 initial states...
Computed 16384 initial states...
Computed 32768 initial states...
Computed 65536 initial states...
Computed 131072 initial states...
Computed 262144 initial states...
Finished computing initial states: 524288 distinct states generated at 2021-01-11 09:37:33.
Progress(2) at 2021-01-11 09:37:36: 1,879,569 states generated (1,879,569 s/min), 528,256 distinct states found (528,256 ds/min), 464,915 states left on queue.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 1.1E-6
  based on the actual fingerprints:  val = 3.1E-12
26990854 states generated, 786942 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 24.
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 17 and the 95th percentile is 2).
Finished in 40s at (2021-01-11 09:38:10)
konnov commented 3 years ago

Expected a constant integer range in .., found 0..tpos

This is a very well-known limitation of our translator to SMT. We will add another pass that detects expressions like this one and guides the user about workarounds.