[BUG] RewriterException: Expected a constant integer range in .., found 1..N)

[lemmy]

-------------------------- MODULE AsyncGameOfLife --------------------------
(***********************************************************************)
(* Evolution in Asynchronous Cellular Automata                         *)
(* by Chrystopher L. Nehaniv.                                          *)
(* https://uhra.herts.ac.uk/bitstream/handle/2299/7041/102007.pdf      *)
(***********************************************************************)
EXTENDS Integers,
        FiniteSets

CONSTANT N
ASSUME N \in Nat

R == 
  {0,1,2}

Pos ==
  {<<x, y>> : x, y \in 1..N}

nbhd(v) ==
  LET moore == {x \in {-1, 0, 1} \X {-1, 0, 1} : x /= <<0, 0>>}
      points == {<<v[1] + x, v[2] + y>> : <<x, y>> \in moore}
  IN { p \in points : /\ p[1] # 0 /\ p[2] # 0
                      /\ p[1]<= N /\ p[2]<= N }

VARIABLES grid
vars == <<grid>>

TypeOK == 
  grid \in [Pos -> (BOOLEAN \X BOOLEAN \X R)]

Init == 
  grid \in [Pos -> (BOOLEAN \X BOOLEAN \X R)]

delta(b, liveNbgrs) ==
  IF \/  (b /\ Cardinality(liveNbgrs) \in {2, 3})
     \/ (~b /\ Cardinality(liveNbgrs) = 3)
  THEN TRUE
  ELSE FALSE

ready(r, Neighbors) == 
  \A w \in Neighbors: grid[w][3] # (r + 2) % 3

qPP(qw, qwP, rw) == 
  CASE rw = 0 -> qw \* w in a state of form (q_w,qP_w,0)
    [] rw = 1 -> qwP \* w in a state of form (q_w,qP_w,1)
    [] OTHER -> FALSE \* Undefined

deltaP(v, q, qP, r, Neighbors) ==
  \/ /\ r = 0
     /\ ready(0, Neighbors) 
     /\ grid' = [ grid EXCEPT ![v] = <<delta(q, 
                  {w \in Neighbors: qPP(grid[w][1], grid[w][2], grid[w][3])}),
                  q, 1>> ]
  \/ /\ r = 0
     /\ ~ ready(0, Neighbors) 
     /\ grid' = [ grid EXCEPT ![v] = <<q, qP, 0>> ]
  \/ /\ r \in {1,2}
     /\ ready(r, Neighbors)
     /\ grid' = [ grid EXCEPT ![v] = <<q, qP, (r + 1) % 3>> ]
  \/ /\ r \in {1,2}
     /\ ~ ready(r, Neighbors)
     /\ UNCHANGED grid

Next ==
  \E v \in Pos: /\ deltaP(v, grid[v][1], grid[v][2], grid[v][3], nbhd(v))

Spec == Init /\ [][Next]_vars
-------------------------------------------------------
\* Tests based on Still lifes

\* https://en.wikipedia.org/wiki/File:Game_of_life_block_with_border.svg
BlockN == 
  N = 4
  
Block ==
  [pos \in Pos |-> IF pos \in {<<2,2>>,<<2,3>>,<<3,2>>,<<3,3>>}
                   THEN <<TRUE, TRUE, 0>>
                   ELSE <<FALSE, FALSE, 0>>]

BlockInit ==
    /\ grid = Block  
==========

markus@avocado:~/src/TLA/_community/apalache(unstable)$ bin/apalache-mc check --init=BlockInit --cinit=BlockN AsyncGameOfLife.tla 
# Tool home: /home/markus/src/TLA/_community/apalache
# Package:   /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.7.0-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -Djava.library.path=/home/markus/src/TLA/_community/apalache/3rdparty/lib
#
# APALACHE version 0.7.0-SNAPSHOT build v0.6.0-125-g1918dfc
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/konnov/apalache/issues]

Checker options: filename=AsyncGameOfLife.tla, init=BlockInit, next=, inv= I@16:18:23.960
PASS #0: SanyParser                                               I@16:18:24.304
Parsing file /home/markus/src/TLA/_community/apalache/AsyncGameOfLife.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
PASS #1: ConfigurationPass                                        I@16:18:24.815
  > Loading TLC configuration from AsyncGameOfLife.cfg            I@16:18:24.816
  > No TLC configuration found; skipping                          I@16:18:24.821
PASS #2: UnrollPass                                               I@16:18:24.890
  > Unroller                                                      I@16:18:24.894
PASS #3: InlinePass                                               I@16:18:24.945
  > InlinerOfUserOper                                             I@16:18:24.947
  > LetInExpander                                                 I@16:18:24.996
PASS #4: PrimingPass                                              I@16:18:25.061
  > Introducing BlockNPrimed for BlockN'                          I@16:18:25.065
  > Introducing BlockInitPrimed for BlockInit'                    I@16:18:25.070
PASS #5: VCGen                                                    I@16:18:25.138
  > No invariant given. Only deadlocks will be checked            I@16:18:25.139
PASS #6: PreprocessingPass                                        I@16:18:25.181
  > Before preprocessing: unique renaming                         I@16:18:25.181
 > Applying standard transformations:                             I@16:18:25.192
  > Desugarer                                                     I@16:18:25.193
  > UniqueRenamer                                                 I@16:18:25.243
  > Normalizer                                                    I@16:18:25.346
  > Keramelizer                                                   I@16:18:25.353
  > After preprocessing: UniqueRenamer                            I@16:18:25.411
PASS #7: TransitionFinderPass                                     I@16:18:25.520
  > Found 1 initializing transitions                              I@16:18:25.631
  > Found 4 transitions                                           I@16:18:25.681
  > Found constant initializer BlockN                             I@16:18:25.681
  > Applying unique renaming                                      I@16:18:25.683
PASS #8: OptimizationPass                                         I@16:18:25.716
 > Applying optimizations:                                        I@16:18:25.728
  > ConstSimplifier                                               I@16:18:25.729
  > ExprOptimizer                                                 I@16:18:25.738
  > ConstSimplifier                                               I@16:18:25.770
PASS #9: AnalysisPass                                             I@16:18:25.802
 > Marking skolemizable existentials and sets to be expanded...   I@16:18:25.805
  > SkolemizationMarker                                           I@16:18:25.807
  > ExpansionMarker                                               I@16:18:25.810
 > Running analyzers...                                           I@16:18:25.828
  > Introduced expression grades                                  I@16:18:25.850
  > Introduced 1 formula hints                                    I@16:18:25.850
PASS #10: BoundedChecker                                          I@16:18:25.850
Initializing CONSTANTS with the provided operator                 I@16:18:25.942
Step 0, level 0: checking if 1 transition(s) are enabled and violate the invariant I@16:18:25.969
The problem occurs around the source location AsyncGameOfLife.tla:17:24-17:27 E@16:18:25.999
(Please report an issue at: [https://github.com/konnov/apalache/issues],at.forsyte.apalache.tla.bmcmt.RewriterException: Expected a constant integer range in .., found 1..N)
AsyncGameOfLife.tla:17:24-17:27: rewriter error: Expected a constant integer range in .., found 1..N E@16:18:26.008
at.forsyte.apalache.tla.bmcmt.RewriterException: Expected a constant integer range in .., found 1..N
	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:324)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:353)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:379)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.eachExpr$1(SymbStateRewriterImpl.scala:396)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.$anonfun$rewriteSeqUntilDone$1(SymbStateRewriterImpl.scala:402)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.AbstractIterator.foreach(Iterator.scala:932)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:54)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
	at scala.collection.AbstractTraversable.map(Traversable.scala:104)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteSeqUntilDone(SymbStateRewriterImpl.scala:402)
	at at.forsyte.apalache.tla.bmcmt.rules.aux.MapBase.rewriteSetMapManyArgs(MapBase.scala:29)
	at at.forsyte.apalache.tla.bmcmt.rules.SetMapRule.apply(SetMapRule.scala:28)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:324)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:353)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:379)
	at at.forsyte.apalache.tla.bmcmt.rules.FunCtorRule.rewriteFunCtor(FunCtorRule.scala:38)
	at at.forsyte.apalache.tla.bmcmt.rules.FunCtorRule.apply(FunCtorRule.scala:28)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:324)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:353)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:379)
	at at.forsyte.apalache.tla.bmcmt.rules.AssignmentRule.apply(AssignmentRule.scala:43)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:324)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:353)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:379)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg$1(AndRule.scala:73)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.$anonfun$apply$2(AndRule.scala:77)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:234)
	at scala.collection.immutable.List.foreach(List.scala:378)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:234)
	at scala.collection.immutable.List.map(List.scala:284)
	at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:77)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:324)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive$1(SymbStateRewriterImpl.scala:353)
	at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:379)
	at at.forsyte.apalache.tla.bmcmt.ModelChecker.applyTransition(ModelChecker.scala:357)
	at at.forsyte.apalache.tla.bmcmt.ModelChecker.filterEnabled$1(ModelChecker.scala:221)
	at at.forsyte.apalache.tla.bmcmt.ModelChecker.findEnabledOrBugs(ModelChecker.scala:230)
	at at.forsyte.apalache.tla.bmcmt.ModelChecker.applySearchStrategy(ModelChecker.scala:188)
	at at.forsyte.apalache.tla.bmcmt.ModelChecker.run(ModelChecker.scala:106)
	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:146)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$2(Tool.scala:81)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$2$adapted(Tool.scala:81)
	at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:195)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:81)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:42)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)
It took me 0 days  0 hours  0 min  2 sec                          I@16:18:26.012
Total time: 2.121 sec                                             I@16:18:26.013
EXITCODE: ERROR (99)

[lemmy]

Ditching cinit and rewriting CONSTANT N to N == 4 works fine.

[konnov]

Well, the problem with a..b is that unless apalache computed bounds on a and b, the set a..b is unbounded. In practice, when you fix the parameters, the bounds are easy to find. But that message is annoying :-)

[lemmy]

@konnov It seems I don't understand the semantics of ConstInit. I assumed that Initializing CONSTANTS with the provided operator in Apalache's output prior to the exception says that CONSTANT N has been fixed to the value defined by BlockN making it - from that point - equivalent to specifying N==4.

[konnov]

They are not equivalent. We treat ConstInit as a constraint on the constant, it can be e.g. N \in 2..10. When one writes N == 4, the tool propagates the constant. Technically, we could propagate the constants from ConstInit too, but why would you write ConstInit with fixed constants?

[lemmy]

CONSTANT N has to be initialized in a config (MC.cfg), but configs are a clutch. It's much more convenient to have no MC.cfg and define (several) ConstInit in MC.tla.

[konnov]

It would be good to have a more aggressive constant propagation in Apalache. One day maybe.

[konnov]

As for MC.cfg, I started to define MC.tla with an INSTANCE inside. It looks better than having two config files, and there are no obvious downsides.

[konnov]

It is not really a bug, as Apalache behaves as intended here (modulo that we could propagate constants from ConstInit better). But this is a usability issue, as the exception is thrown from the guts of the translator to SMT. We should introduce an intermediate pass that checks for known limitations and explains the user what to do.

[konnov]

@shonfeder, that is an interesting issue to start with