search

apalache-mc / apalache

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

[BUG] java.lang.UnsupportedOperationException: empty.reduceLeft #475

Closed lemmy closed 3 years ago

lemmy commented 3 years ago 
markus@avocado:~/Desktop/ewd998$ apalache check EWD998Chan
# Tool home: /home/markus/src/TLA/_community/apalache
# Package:   /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.8.2-SNAPSHOT-full.jar
# JVM args: -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla
#
# APALACHE version 0.8.2-SNAPSHOT build v0.7.2-163-gde4505d
#
# 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=EWD998Chan, init=, next=, inv=          I@11:15:52.937
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.8.2-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@11:15:53.480
Parsing file /home/markus/Desktop/ewd998/EWD998Chan.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.tla
PASS #1: ConfigurationPass                                        I@11:15:54.201
  > EWD998Chan: Loading TLC configuration                         I@11:15:54.204
  > No TLC configuration found. Skipping.                         I@11:15:54.215
  > Command line option --init is not set. Using Init             I@11:15:54.216
  > Command line option --next is not set. Using Next             I@11:15:54.216
  > Set the initialization predicate to Init                      I@11:15:54.216
  > Set the transition predicate to Next                          I@11:15:54.217
PASS #2: UnrollPass                                               I@11:15:54.298
  > Unroller                                                      I@11:15:54.376
PASS #3: PrimingPass                                              I@11:15:54.427
  > Introducing InitPrimed for Init'                              I@11:15:54.433
PASS #4: CoverAnalysisPass                                        I@11:15:54.499
PASS #5: InlinePass                                               I@11:15:54.506
  > InlinerOfUserOper                                             I@11:15:54.515
  > LetInExpander                                                 I@11:15:54.568
  > InlinerOfUserOper                                             I@11:15:54.583
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next I@11:15:54.591
PASS #6: VCGen                                                    I@11:15:54.630
  > No invariant given. Only deadlocks will be checked            I@11:15:54.631
PASS #7: PreprocessingPass                                        I@11:15:54.647
  > Before preprocessing: unique renaming                         I@11:15:54.647
 > Applying standard transformations:                             I@11:15:54.660
  > Desugarer                                                     I@11:15:54.663
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],java.lang.UnsupportedOperationException: empty.reduceLeft)
Unhandled exception                                               E@11:15:54.702
java.lang.UnsupportedOperationException: empty.reduceLeft
    at scala.collection.TraversableOnce.reduceLeft(TraversableOnce.scala:212)
    at scala.collection.TraversableOnce.reduceLeft$(TraversableOnce.scala:210)
    at scala.collection.mutable.ArrayBuffer.scala$collection$IndexedSeqOptimized$$super$reduceLeft(ArrayBuffer.scala:49)
    at scala.collection.IndexedSeqOptimized.reduceLeft(IndexedSeqOptimized.scala:77)
    at scala.collection.IndexedSeqOptimized.reduceLeft$(IndexedSeqOptimized.scala:76)
    at scala.collection.mutable.ArrayBuffer.reduceLeft(ArrayBuffer.scala:49)
    at scala.collection.TraversableOnce.reduce(TraversableOnce.scala:242)
    at scala.collection.TraversableOnce.reduce$(TraversableOnce.scala:242)
    at scala.collection.AbstractTraversable.reduce(Traversable.scala:108)
    at at.forsyte.apalache.tla.pp.Desugarer.flattenTuples(Desugarer.scala:86)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$flattenTuples$1(Desugarer.scala:86)
    at scala.collection.immutable.List.map(List.scala:293)
    at at.forsyte.apalache.tla.pp.Desugarer.flattenTuples(Desugarer.scala:86)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$1(Desugarer.scala:48)
    at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
    at scala.collection.immutable.List.map(List.scala:297)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$1(Desugarer.scala:78)
    at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$3(Desugarer.scala:81)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:285)
    at scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:62)
    at scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:55)
    at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:49)
    at scala.collection.TraversableLike.map(TraversableLike.scala:285)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:278)
    at scala.collection.AbstractTraversable.map(Traversable.scala:108)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$1(Desugarer.scala:81)
    at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
    at scala.collection.immutable.List.map(List.scala:297)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$1(Desugarer.scala:78)
    at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
    at scala.collection.immutable.List.map(List.scala:293)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$1(Desugarer.scala:78)
    at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
    at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:285)
    at scala.collection.mutable.ResizableArray.foreach(ResizableArray.scala:62)
    at scala.collection.mutable.ResizableArray.foreach$(ResizableArray.scala:55)
    at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:49)
    at scala.collection.TraversableLike.map(TraversableLike.scala:285)
    at scala.collection.TraversableLike.map$(TraversableLike.scala:278)
    at scala.collection.AbstractTraversable.map(Traversable.scala:108)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$1(Desugarer.scala:78)
    at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
    at scala.collection.immutable.List.map(List.scala:297)
    at at.forsyte.apalache.tla.pp.Desugarer.$anonfun$transform$1(Desugarer.scala:78)
    at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
    at at.forsyte.apalache.tla.pp.Desugarer.apply(Desugarer.scala:26)
    at at.forsyte.apalache.tla.pp.Desugarer.apply(Desugarer.scala:22)
    at at.forsyte.apalache.tla.lir.transformations.standard.ModuleByExTransformer.$anonfun$apply$1(ModuleByExTransformer.scala:15)
    at scala.collection.immutable.List.map(List.scala:297)
    at at.forsyte.apalache.tla.lir.transformations.standard.ModuleByExTransformer.apply(ModuleByExTransformer.scala:23)
    at at.forsyte.apalache.tla.lir.transformations.standard.ModuleByExTransformer.apply(ModuleByExTransformer.scala:11)
    at at.forsyte.apalache.tla.pp.passes.PreproPassImpl.$anonfun$execute$1(PreproPassImpl.scala:66)
    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.pp.passes.PreproPassImpl.execute(PreproPassImpl.scala:63)
    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  1 sec                          I@11:15:54.705
Total time: 1.771 sec                                             I@11:15:54.707
EXITCODE: ERROR (99)
----------------------------- MODULE EWD998Chan -----------------------------
EXTENDS Integers, Sequences, FiniteSets

RemoveAt(s, i) == 
  SubSeq(s, 1, i-1) \o SubSeq(s, i+1, Len(s))

\* CONSTANT N
\* ASSUME NAssumption == N \in Nat \ {0} \* At least one node.

N == 3

\* igor: this is the apalache idiom to deal with dynamic ranges
rng(a, b) == { i \in 0..N: a <= i /\ i <= b }

sum(a, b) == a + b

\* old apalache type annotations, will change soon
a <: b == a
\* a type specification for the recursive function reduced
reducedT == [Int -> Int]

Reduce(op(_,_), fun, from, to, base) == 
  (**************************************************************************)
  (* Reduce the elements in the range from..to of the function's co-domain. *)
  (**************************************************************************)
  LET reduced[i \in rng(from, to)] ==
          IF i = from THEN op(base, fun[i])
          ELSE op((reduced <: reducedT)[i - 1], fun[i])
  IN reduced[to]

Node == 0 .. N-1
Color == {"white", "black"}

VARIABLES 
 active,
 color,
 counter,
 inbox

vars == <<active, color, counter, inbox>>

TokenMsg == [type : {"tok"}, q : Int, color : Color]
BasicMsg == [type : {"pl"}]
Message == TokenMsg \cup BasicMsg

TypeOK ==
  /\ counter \in [Node -> Int]
  /\ active \in [Node -> BOOLEAN]
  /\ color \in [Node -> Color]
  /\ inbox \in [Node -> Seq(Message)]
  \* There is always exactly one token (singleton-type).
  /\ \E i \in Node : \E j \in 1..Len(inbox[i]): inbox[i][j].type = "tok"
  /\ \A i,j \in Node : \A k \in 1 .. Len(inbox[i]) : \A l \in 1 .. Len(inbox[j]) :
        inbox[i][k].type = "tok" /\ inbox[j][l].type = "tok"
        => i = j /\ k = l

------------------------------------------------------------------------------

Init ==
  (* Rule 0 *)
  /\ counter = [i \in Node |-> 0] \* c properly initialized
  /\ inbox = [i \in Node |-> IF i = 0 
                             THEN << [type |-> "tok", q |-> 0, color |-> "black" ] >> 
                             ELSE <<>>] \* with empty channels.
  (* EWD840 *) 
  /\ active \in [Node -> BOOLEAN]
  /\ color \in [Node -> Color]

InitiateProbe ==
  (* Rule 1 *)
  /\ \E j \in 1..Len(inbox[0]):
      \* Token is at node 0.
      /\ inbox[0][j].type = "tok"
      /\ \* Previous round inconsistent, if:
         \/ inbox[0][j].color = "black"
         \/ color[0] = "black"
         \* Implicit stated in EWD998 as c0 + q > 0 means that termination has not 
         \* been achieved: Initiate a probe if the token's color is white but the
         \* number of in-flight messages is not zero.
         \/ counter[0] + inbox[0][j].q # 0
      /\ inbox' = [inbox EXCEPT ![N-1] = Append(@, 
           [type |-> "tok", q |-> 0,
             (* Rule 6 *)
             color |-> "white"]), 
             ![0] = RemoveAt(@, j) ] \* consume token message from inbox[0]. 
  (* Rule 6 *)
  /\ color' = [ color EXCEPT ![0] = "white" ]
  \* The state of the nodes remains unchanged by token-related actions.
  /\ UNCHANGED <<active, counter>>                            

PassToken(i) ==
  (* Rule 2 *)
  /\ ~ active[i] \* If machine i is active, keep the token.
  /\ \E j \in 1..Len(inbox[i]) : 
          /\ inbox[i][j].type = "tok"
          \* the machine nr.i+1 transmits the token to machine nr.i under q := q + c[i+1]
          /\ LET tkn == inbox[i][j]
             IN  inbox' = [inbox EXCEPT ![i-1] = 
                                       Append(@, [tkn EXCEPT !.q = tkn.q + counter[i],
                                                             !.color = IF color[i] = "black"
                                                                       THEN "black"
                                                                       ELSE tkn.color]),
                                    ![i] = RemoveAt(@, j) ] \* pass on the token.
  (* Rule 7 *)
  /\ color' = [ color EXCEPT ![i] = "white" ]
  \* The state of the nodes remains unchanged by token-related actions.
  /\ UNCHANGED <<active, counter>>                            

System == \/ InitiateProbe
          \/ \E i \in Node \ {0} : PassToken(i)

-----------------------------------------------------------------------------

SendMsg(i) ==
  \* Only allowed to send msgs if node i is active.
  /\ active[i]
  (* Rule 0 *)
  /\ counter' = [counter EXCEPT ![i] = @ + 1]
  \* Non-deterministically choose a receiver node.
  /\ \E j \in Node \ {i} :
          \* Send a message (not the token) to j.
          /\ inbox' = [inbox EXCEPT ![j] = Append(@, [type |-> "pl" ] ) ]
          \* Note that we don't blacken node i as in EWD840 if node i
          \* sends a message to node j with j > i
  /\ UNCHANGED <<active, color>>                            

RecvMsg(i) ==
  (* Rule 0 *)
  /\ counter' = [counter EXCEPT ![i] = @ - 1]
  (* Rule 3 *)
  /\ color' = [ color EXCEPT ![i] = "black" ]
  \* Receipt of a message activates i.
  /\ active' = [ active EXCEPT ![i] = TRUE ]
  \* Consume a message (not the token!).
  /\ \E j \in 1..Len(inbox[i]) : 
          /\ inbox[i][j].type = "pl"
          /\ inbox' = [inbox EXCEPT ![i] = RemoveAt(@, j) ]
  /\ UNCHANGED <<>>                           

Deactivate(i) ==
  /\ active[i]
  /\ active' = [active EXCEPT ![i] = FALSE]
  /\ UNCHANGED <<color, inbox, counter>>

Environment == \E i \in Node : SendMsg(i) \/ RecvMsg(i) \/ Deactivate(i)

-----------------------------------------------------------------------------

Next ==
  System \/ Environment
========
konnov commented 3 years ago

Wow. We definitely did not account for that:

   UNCHANGED <<>>

We definitely should use fold though.

konnov commented 3 years ago

We have fixed that in #483. The upcoming release will contain the fix (today).