[BUG] java.lang.AssertionError at forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming #528

vitorenesduarte · 2021-02-01T13:40:18Z

To Reproduce

git clone https://github.com/informalsystems/ibc-rs
cd ibc-rs/
git checkout ilina/ics03_tla_bugfix
cd docs/spec/tla/fungible-token-transfer
apalache-mc check --inv=TypeOK IBCTokenTransfer_apalache.tla

Log files

output:

# APALACHE version 0.8.1 build v0.7.2-159-ga0e64fc
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
#
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Checker options: filename=IBCTokenTransfer_apalache.tla, init=, next=, inv=TypeOK I@14:25:27.279
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/home/vitor.enes/bin/apalache-pkg-0.8.1-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@14:25:27.500
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/IBCTokenTransfer_apalache.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/IBCTokenTransfer.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Sequences.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla
Parsing file /tmp/Naturals.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/Chain.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/Bank.tla
WORKAROUND #130: labelling operator Sum as recursive, though SANY did not tell us so. W@14:25:28.019
PASS #1: ConfigurationPass                                        I@14:25:28.369
  > IBCTokenTransfer_apalache.cfg: Loading TLC configuration      I@14:25:28.371
  > No TLC configuration found. Skipping.                         I@14:25:28.376
  > Command line option --init is not set. Using Init             I@14:25:28.376
  > Command line option --next is not set. Using Next             I@14:25:28.376
  > Set the initialization predicate to Init                      I@14:25:28.376
  > Set the transition predicate to Next                          I@14:25:28.377
  > Set an invariant to TypeOK                                    I@14:25:28.377
PASS #2: UnrollPass                                               I@14:25:28.469
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],java.lang.AssertionError: assertion failed)
Unhandled exception                                               E@14:25:28.510
java.lang.AssertionError: assertion failed
	at scala.Predef$.assert(Predef.scala:208)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:184)
	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.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:200)
	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.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:200)
	at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.apply(IncrementalRenaming.scala:245)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$applyToDecl$1(IncrementalRenaming.scala:246)
	at at.forsyte.apalache.tla.lir.transformations.impl.Lift$.$anonfun$exToDecl$1(Lift.scala:8)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:285)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.generic.TraversableForwarder.foreach(TraversableForwarder.scala:38)
	at scala.collection.generic.TraversableForwarder.foreach$(TraversableForwarder.scala:38)
	at scala.collection.mutable.ListBuffer.foreach(ListBuffer.scala:47)
	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.lir.transformations.impl.Lift$.$anonfun$declToDecls$1(Lift.scala:13)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.syncAndNormalizeDs(IncrementalRenaming.scala:373)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$renameInModule$1(IncrementalRenaming.scala:134)
	at at.forsyte.apalache.tla.pp.passes.UnrollPassImpl.execute(UnrollPassImpl.scala:58)
	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@14:25:28.510
Total time: 1.232 sec                                             I@14:25:28.510
EXITCODE: ERROR (99)

detailed.log

14:25:27.279 [main] INFO  a.f.a.t.Tool$ - Checker options: filename=IBCTokenTransfer_apalache.tla, init=, next=, inv=TypeOK
14:25:27.500 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
14:25:28.019 [main] WARN  a.f.a.t.i.ModuleTranslator - WORKAROUND #130: labelling operator Sum as recursive, though SANY did not tell us so.
14:25:28.368 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
14:25:28.369 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: ConfigurationPass
14:25:28.371 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > IBCTokenTransfer_apalache.cfg: Loading TLC configuration
14:25:28.376 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > No TLC configuration found. Skipping.
14:25:28.376 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --init is not set. Using Init
14:25:28.376 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --next is not set. Using Next
14:25:28.376 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
14:25:28.377 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
14:25:28.377 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to TypeOK
14:25:28.469 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: ConfigurationPass [OK]
14:25:28.469 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: UnrollPass
14:25:28.510 [main] ERROR a.f.a.t.Tool$ - Unhandled exception
java.lang.AssertionError: assertion failed
	at scala.Predef$.assert(Predef.scala:208)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:184)
	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.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:200)
	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.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:200)
	at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$track$1(TrackerWithListeners.scala:15)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.apply(IncrementalRenaming.scala:245)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$applyToDecl$1(IncrementalRenaming.scala:246)
	at at.forsyte.apalache.tla.lir.transformations.impl.Lift$.$anonfun$exToDecl$1(Lift.scala:8)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:285)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at scala.collection.generic.TraversableForwarder.foreach(TraversableForwarder.scala:38)
	at scala.collection.generic.TraversableForwarder.foreach$(TraversableForwarder.scala:38)
	at scala.collection.mutable.ListBuffer.foreach(ListBuffer.scala:47)
	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.lir.transformations.impl.Lift$.$anonfun$declToDecls$1(Lift.scala:13)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.syncAndNormalizeDs(IncrementalRenaming.scala:373)
	at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$renameInModule$1(IncrementalRenaming.scala:134)
	at at.forsyte.apalache.tla.pp.passes.UnrollPassImpl.execute(UnrollPassImpl.scala:58)
	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)
14:25:28.510 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  1 sec
14:25:28.510 [main] INFO  a.f.a.t.Tool$ - Total time: 1.232 sec

Desktop (please complete the following information):

Debian GNU/Linux 10
openjdk 11.0.9.1 2020-11-04
APALACHE version 0.8.1 build v0.7.2-159-ga0e64fc

The text was updated successfully, but these errors were encountered:

konnov · 2021-02-01T15:14:43Z

I think it has been fixed recently. Can you try it in 0.9.0?

vitorenesduarte · 2021-02-01T15:38:02Z

I'm getting the same error:

# APALACHE version 0.9.0 build 5fce1e5
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
# 
# Usage statistics is OFF. We care about your privacy.
# If you want to help our project, consider enabling statistics with config --enable-stats=true.

Checker options: filename=IBCTokenTransfer_apalache.tla, init=, next=, inv=TypeOK I@16:35:35.933
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by com.google.inject.internal.cglib.core.$ReflectUtils$1 (file:/home/vitor.enes/bin/apalache-pkg-0.9.0-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
Tuning:                                                           I@16:35:36.149
PASS #0: SanyParser                                               I@16:35:36.149
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/IBCTokenTransfer_apalache.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/IBCTokenTransfer.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Sequences.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/IBCTokenTransferDefinitions.tla
Parsing file /tmp/Naturals.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/Chain.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/ICS04PacketHandlers.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/ICS20FungibleTokenTransferHandlers.tla
Parsing file /home/vitor.enes/ibc-rs/docs/spec/tla/fungible-token-transfer/Bank.tla
WORKAROUND #130: labelling operator Sum as recursive, though SANY did not tell us so. W@16:35:36.617
PASS #1: ConfigurationPass                                        I@16:35:36.936
  > IBCTokenTransfer_apalache.cfg: Loading TLC configuration      I@16:35:36.938
  > No TLC configuration found. Skipping.                         I@16:35:36.942
  > Command line option --init is not set. Using Init             I@16:35:36.942
  > Command line option --next is not set. Using Next             I@16:35:36.942
  > Set the initialization predicate to Init                      I@16:35:36.942
  > Set the transition predicate to Next                          I@16:35:36.943
  > Set an invariant to TypeOK                                    I@16:35:36.943
PASS #2: UnrollPass                                               I@16:35:37.043
(Please report an issue at: [https://github.com/informalsystems/apalache/issues],java.lang.AssertionError: assertion failed)
Unhandled exception                                               E@16:35:37.087
java.lang.AssertionError: assertion failed
        at scala.Predef$.assert(Predef.scala:208)
        at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:183)
        at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$trackEx$1(TrackerWithListeners.scala:17)
        at scala.collection.immutable.List.map(List.scala:297)
        at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:199)
        at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$trackEx$1(TrackerWithListeners.scala:17)
        at scala.collection.immutable.List.map(List.scala:297)
        at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$rename$1(IncrementalRenaming.scala:199)
        at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$trackEx$1(TrackerWithListeners.scala:17)
        at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.apply(IncrementalRenaming.scala:248)
        at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.apply(IncrementalRenaming.scala:123)
        at at.forsyte.apalache.tla.lir.transformations.TransformationTracker.$anonfun$fromExToDeclTransformation$1(TransformationTracker.scala:70)
        at at.forsyte.apalache.tla.lir.transformations.impl.TrackerWithListeners.$anonfun$trackDecl$1(TrackerWithListeners.scala:33)
        at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$syncAndNormalizeDs$1(IncrementalRenaming.scala:380)
        at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:285)
        at scala.collection.immutable.List.foreach(List.scala:431)
        at scala.collection.generic.TraversableForwarder.foreach(TraversableForwarder.scala:38)
        at scala.collection.generic.TraversableForwarder.foreach$(TraversableForwarder.scala:38)
        at scala.collection.mutable.ListBuffer.foreach(ListBuffer.scala:47)
        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.lir.transformations.standard.IncrementalRenaming.syncAndNormalizeDs(IncrementalRenaming.scala:380)
        at at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming.$anonfun$renameInModule$1(IncrementalRenaming.scala:133)
        at at.forsyte.apalache.tla.pp.passes.UnrollPassImpl.execute(UnrollPassImpl.scala:58)
        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:173)
        at at.forsyte.apalache.tla.Tool$.$anonfun$run$2(Tool.scala:95)
        at at.forsyte.apalache.tla.Tool$.$anonfun$run$2$adapted(Tool.scala:95)
        at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:257)
        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  1 sec                          I@16:35:37.087
Total time: 1.155 sec                                             I@16:35:37.087
EXITCODE: ERROR (99)

The IBCTokenTransfer_apalache.tla has been removed from that branch, so here it is:

--------------------- MODULE IBCTokenTransfer_apalache ---------------------

 VARIABLES chainAstore, \* store of ChainA
           chainBstore, \* store of ChainB
           packetDatagramsChainA, \* set of packet datagrams incoming to ChainA
           packetDatagramsChainB, \* set of packet datagrams incoming to ChainB
           packetLog, \* packet log
           appPacketSeqChainA, \* packet sequence number from the application on ChainA
           appPacketSeqChainB, \* packet sequence number from the application on ChainB
           accounts, \* a map from chainIDs and denominations to account balances
           escrowAccounts \* a map from channelIDs and denominations to escrow account balances

 INSTANCE IBCTokenTransfer WITH
     MaxHeight <- 2, 
     MaxPacketSeq <- 1, 
     MaxBalance <- 1,
     NativeDenominationChainA <- "atom", 
     NativeDenominationChainB <- "eth" 

 =============================================================================

konnov · 2021-02-01T15:44:59Z

@Kukovec can you have a look?

vitorenesduarte · 2021-02-01T15:45:26Z

Actually that file is not needed. It should be enough to run apalache-mc check IBCTokenTransfer.tla.

konnov · 2021-02-01T15:46:57Z

Still, it should not throw an exception

Kukovec · 2021-02-01T16:01:39Z

One question, I can't see a ics03_tla_bugfix branch in the repo, can you advise?

vitorenesduarte · 2021-02-01T16:10:56Z

Sorry, it should be ilina/ics03_tla_bugfix. I've updated the instructions in the top comment.

Kukovec · 2021-02-01T16:23:15Z

In any case, I found the cause. The syntax

[<<x,y>> \in S |-> e]

(e.g. in Init) should have been caught and replaced by Desugarer, since this is pattern-matching on domain elements. This was supposedly addressed by #483, but apparently not completely.

konnov · 2021-02-01T16:34:58Z

Actually, the bug is triggered before Desugarer is called.

konnov · 2021-02-01T16:44:13Z

The problem is that Unroller is called before Desugarer. So we have to promote Desugarer to work before Unroller.

konnov · 2021-02-01T16:51:14Z

We have to solve #531 and this hopefully will allow us to get rid of this bug.

konnov · 2021-02-02T19:15:39Z

Fixed in #536

vitorenesduarte added the bug label Feb 1, 2021

konnov assigned Kukovec Feb 1, 2021

konnov added this to the February iteration milestone Feb 1, 2021

konnov added the high prio label Feb 1, 2021

konnov mentioned this issue Feb 1, 2021

[FEATURE] Promote Desugarer to be the first preprocessing pass #531

Closed

konnov mentioned this issue Feb 2, 2021

Promote Desugarer to be the first pass #536

Merged

4 tasks

konnov closed this as completed Feb 2, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[BUG] java.lang.AssertionError at forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming #528

[BUG] java.lang.AssertionError at forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming #528

vitorenesduarte commented Feb 1, 2021 •

edited

Loading

konnov commented Feb 1, 2021

vitorenesduarte commented Feb 1, 2021

konnov commented Feb 1, 2021

vitorenesduarte commented Feb 1, 2021

konnov commented Feb 1, 2021

Kukovec commented Feb 1, 2021

vitorenesduarte commented Feb 1, 2021

Kukovec commented Feb 1, 2021

konnov commented Feb 1, 2021

konnov commented Feb 1, 2021

konnov commented Feb 1, 2021

konnov commented Feb 2, 2021

[BUG] java.lang.AssertionError at forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming #528

[BUG] java.lang.AssertionError at forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming #528

Comments

vitorenesduarte commented Feb 1, 2021 • edited Loading

konnov commented Feb 1, 2021

vitorenesduarte commented Feb 1, 2021

konnov commented Feb 1, 2021

vitorenesduarte commented Feb 1, 2021

konnov commented Feb 1, 2021

Kukovec commented Feb 1, 2021

vitorenesduarte commented Feb 1, 2021

Kukovec commented Feb 1, 2021

konnov commented Feb 1, 2021

konnov commented Feb 1, 2021

konnov commented Feb 1, 2021

konnov commented Feb 2, 2021

vitorenesduarte commented Feb 1, 2021 •

edited

Loading