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] java.lang.UnsupportedOperationException: empty.reduceLeft #475

Closed
lemmy opened this issue Jan 22, 2021 · 2 comments
Closed

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

lemmy opened this issue Jan 22, 2021 · 2 comments
Assignees
@konnov
Labels
bug Fprepro Feature: TLA+ preprocessor
Milestone
January iteration...

Comments

@lemmy
Copy link
Contributor

lemmy commented Jan 22, 2021 

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
========
@lemmy lemmy added the bug label Jan 22, 2021
@konnov
Copy link
Collaborator

konnov commented Jan 22, 2021

Wow. We definitely did not account for that:

   UNCHANGED <<>>

We definitely should use fold though.

@konnov konnov self-assigned this Jan 22, 2021
@konnov konnov added this to the January iteration milestone Jan 22, 2021
@konnov konnov added the Fprepro Feature: TLA+ preprocessor label Jan 23, 2021
konnov added a commit that referenced this issue Jan 23, 2021
@konnov
close #471 and close #475
bc75aa4
@konnov konnov mentioned this issue Jan 23, 2021
Merged
3 tasks
@konnov
Copy link
Collaborator

konnov commented Jan 25, 2021

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

@konnov konnov closed this as completed Jan 25, 2021
@apalache-bot apalache-bot mentioned this issue Jan 25, 2021
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@konnov konnov

Labels
bug Fprepro Feature: TLA+ preprocessor
Projects
None yet
Milestone
January iteration 2021
Development

No branches or pull requests
2 participants
@lemmy @konnov