@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.20 of Day Month 20??
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 130 and seed 8675143452668328597 with 4 workers on 8 cores with 1193MB heap and 2683MB offheap memory [pid: 568] (Windows 10 10.0 amd64, Oracle Corporation 11.0.2 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file C:\lamport\books\fred\book-specs\IFifo.toolbox\check TypeOK\MC.tla
Parsing file C:\lamport\books\fred\book-specs\IFifo.toolbox\check TypeOK\IFifo.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\TLC.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Integers.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Sequences.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Naturals.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module IFifo
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2024-10-19 11:37:45)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 4 distinct states generated at 2024-10-19 11:37:46.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2193:0 @!@!@
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.5E-11
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2024-10-19 11:37:46
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 63, col 1 to line 63, col 4 of module IFifo>: 4:4
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 63, col 18 to line 63, col 40 of module IFifo: 1:2
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 63, col 25 to line 63, col 30 of module IFifo: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 21, col 1 to line 21, col 8 of module MC: 1:3
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 21, col 2 to line 21, col 3 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 21, col 6 to line 21, col 7 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 64, col 20 to line 64, col 35 of module IFifo: 1:8
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 64, col 21 to line 64, col 26 of module IFifo: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 64, col 31 to line 64, col 34 of module IFifo: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 31, col 1 to line 31, col 8 of module MC: 1:10
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 31, col 2 to line 31, col 3 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 31, col 6 to line 31, col 7 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 65, col 12 to line 65, col 24 of module IFifo: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 66, col 23 to line 66, col 45 of module IFifo: 4:8
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 66, col 30 to line 66, col 35 of module IFifo: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 21, col 1 to line 21, col 8 of module MC: 4:12
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 21, col 2 to line 21, col 3 of module MC: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 21, col 6 to line 21, col 7 of module MC: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 67, col 12 to line 67, col 25 of module IFifo: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<BeginEnq line 69, col 1 to line 69, col 11 of module IFifo>: 1923:7500
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 69, col 19 to line 69, col 31 of module IFifo: 21784
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 69, col 19 to line 69, col 24 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 69, col 28 to line 69, col 31 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 70, col 35 to line 70, col 62 of module IFifo: 7500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 70, col 28 to line 70, col 31 of module IFifo: 3750
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 31, col 1 to line 31, col 8 of module MC: 3750:11250
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 31, col 2 to line 31, col 3 of module MC: 3750
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 31, col 6 to line 31, col 7 of module MC: 3750
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 71, col 19 to line 71, col 59 of module IFifo: 7500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 72, col 19 to line 72, col 52 of module IFifo: 7500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<DoEnq line 74, col 1 to line 74, col 8 of module IFifo>: 1371:7500
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 74, col 16 to line 74, col 33 of module IFifo: 25534
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 74, col 16 to line 74, col 26 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 74, col 30 to line 74, col 33 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 75, col 16 to line 75, col 45 of module IFifo: 7500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 76, col 17 to line 76, col 57 of module IFifo: 7500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 77, col 16 to line 77, col 47 of module IFifo: 7500
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<EndEnq line 79, col 1 to line 79, col 9 of module IFifo>: 1169:6784
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 79, col 17 to line 79, col 29 of module IFifo: 24818
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 79, col 17 to line 79, col 22 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 79, col 26 to line 79, col 29 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 80, col 17 to line 80, col 34 of module IFifo: 21068
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 80, col 17 to line 80, col 27 of module IFifo: 14284
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 80, col 31 to line 80, col 34 of module IFifo: 14284
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 81, col 17 to line 81, col 48 of module IFifo: 6784
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 82, col 17 to line 82, col 60 of module IFifo: 6784
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<BeginDeq line 84, col 1 to line 84, col 11 of module IFifo>: 2198:7212
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 84, col 19 to line 84, col 31 of module IFifo: 25246
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 84, col 19 to line 84, col 24 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 84, col 28 to line 84, col 31 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 85, col 19 to line 85, col 50 of module IFifo: 7212
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 86, col 19 to line 86, col 62 of module IFifo: 7212
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 87, col 19 to line 87, col 52 of module IFifo: 7212
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<DoDeq line 89, col 1 to line 89, col 8 of module IFifo>: 1985:3360
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 89, col 16 to line 89, col 28 of module IFifo: 21394
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 89, col 16 to line 89, col 21 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 89, col 25 to line 89, col 28 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 90, col 16 to line 90, col 35 of module IFifo: 14182
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 90, col 16 to line 90, col 26 of module IFifo: 10822
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 90, col 30 to line 90, col 35 of module IFifo: 10822
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 91, col 16 to line 91, col 28 of module IFifo: 6970
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 91, col 16 to line 91, col 20 of module IFifo: 3610
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 91, col 24 to line 91, col 28 of module IFifo: 3610
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 92, col 16 to line 92, col 64 of module IFifo: 3360
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 93, col 16 to line 93, col 35 of module IFifo: 3360
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 94, col 16 to line 94, col 47 of module IFifo: 3360
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<EndDeq line 96, col 1 to line 96, col 9 of module IFifo>: 367:7212
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 96, col 17 to line 96, col 29 of module IFifo: 25246
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 96, col 17 to line 96, col 22 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 96, col 26 to line 96, col 29 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 97, col 17 to line 97, col 36 of module IFifo: 18034
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 97, col 17 to line 97, col 27 of module IFifo: 10822
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 97, col 31 to line 97, col 36 of module IFifo: 10822
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 98, col 17 to line 98, col 54 of module IFifo: 7212
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 99, col 17 to line 99, col 60 of module IFifo: 7212
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<TypeOK line 57, col 1 to line 57, col 6 of module IFifo>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 57, col 11 to line 61, col 56 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 57, col 14 to line 57, col 49 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 57, col 14 to line 57, col 16 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 57, col 22 to line 57, col 49 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 57, col 23 to line 57, col 28 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 57, col 33 to line 57, col 48 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 57, col 33 to line 57, col 36 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||line 57, col 43 to line 57, col 48 of module IFifo: 13017:26034
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 57, col 44 to line 57, col 47 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 58, col 14 to line 58, col 49 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 58, col 14 to line 58, col 16 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 58, col 22 to line 58, col 49 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 58, col 23 to line 58, col 28 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 58, col 33 to line 58, col 48 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 58, col 33 to line 58, col 36 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||line 58, col 43 to line 58, col 48 of module IFifo: 13017:26034
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 58, col 44 to line 58, col 47 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 59, col 14 to line 59, col 32 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 60, col 14 to line 60, col 50 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 61, col 14 to line 61, col 56 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 61, col 14 to line 61, col 21 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 61, col 27 to line 61, col 56 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 61, col 28 to line 61, col 33 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 61, col 38 to line 61, col 55 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 61, col 38 to line 61, col 41 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||line 61, col 48 to line 61, col 55 of module IFifo: 13017:26034
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 61, col 49 to line 61, col 54 of module IFifo: 13017
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2778:0 @!@!@
<constr_172933066381575000 line 35, col 1 to line 35, col 25 of module MC>: 35572:39572
@!@!@ENDMSG 2778 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 36, col 1 to line 36, col 14 of module MC: 39572
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(26) at 2024-10-19 11:37:46: 39,572 states generated (931,471 s/min), 9,017 distinct states found (212,247 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
39572 states generated, 9017 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 26.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 6 and the 95th percentile is 3).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 2562ms at (2024-10-19 11:37:46)
@!@!@ENDMSG 2186 @!@!@
