@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.20 of Day Month 20??
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 8 and seed 4274897399077996598 with 4 workers on 8 cores with 1193MB heap and 2683MB offheap memory [pid: 16852] (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\AddSeq.toolbox\Model_1\MC.tla
Parsing file C:\lamport\books\fred\book-specs\AddSeq.toolbox\Model_1\AddSeq.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:\lamport\books\fred\book-specs\AddSeq.toolbox\Model_1\Add.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 Add
Semantic processing of module AddSeq
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2024-10-15 15:48:10)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 4 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 8 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 16 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 32 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 64 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 128 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 256 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 512 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 1024 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2048 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 4096 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 8192 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 16384 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 32768 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 65536 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 131072 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 262144 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 524288 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 1048576 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1232100 distinct states generated at 2024-10-15 15:48:18.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(2) at 2024-10-15 15:48:21: 1,672,500 states generated (1,672,500 s/min), 1,386,956 distinct states found (1,386,956 ds/min), 946,544 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@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 = 10.0E-8
  based on the actual fingerprints:  val = 1.1E-8
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2024-10-15 15:48:29
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 58, col 1 to line 58, col 4 of module AddSeq>: 1232100:1232100
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 59, col 18 to line 59, col 25 of module AddSeq: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 6, col 1 to line 6, col 35 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 6, col 7 to line 6, col 35 of module MC: 1:1116
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||line 6, col 8 to line 6, col 21 of module MC: 3:5432
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 6, col 9 to line 6, col 12 of module MC: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 6, col 17 to line 6, col 20 of module MC: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 6, col 31 to line 6, col 34 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 60, col 18 to line 60, col 25 of module AddSeq: 1110
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 6, col 1 to line 6, col 35 of module MC: 1110
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 6, col 7 to line 6, col 35 of module MC: 1110:1238760
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||line 6, col 8 to line 6, col 21 of module MC: 3330:6029520
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 6, col 9 to line 6, col 12 of module MC: 3330
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 6, col 17 to line 6, col 20 of module MC: 3330
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 6, col 31 to line 6, col 34 of module MC: 1110
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 61, col 12 to line 61, col 22 of module AddSeq: 1232100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 63, col 12 to line 63, col 19 of module AddSeq: 1232100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Next line 65, col 1 to line 65, col 4 of module AddSeq>: 263285:1493276
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 65, col 12 to line 65, col 19 of module AddSeq: 2988661
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 65, col 12 to line 65, col 13 of module AddSeq: 1495385
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 66, col 15 to line 66, col 53 of module AddSeq: 1493276
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 66, col 16 to line 66, col 24 of module AddSeq: 1493276
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 66, col 31 to line 66, col 52 of module AddSeq: 7296
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 66, col 31 to line 66, col 39 of module AddSeq: 7296
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 66, col 44 to line 66, col 52 of module AddSeq: 3216
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 68, col 28 to line 68, col 57 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 68, col 35 to line 68, col 57 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 68, col 42 to line 68, col 44 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 68, col 47 to line 68, col 56 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 68, col 47 to line 68, col 51 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 67, col 36 to line 67, col 64 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 67, col 36 to line 67, col 56 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 67, col 36 to line 67, col 44 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 67, col 36 to line 67, col 41 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 13 to line 37, col 46 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 37, col 16 to line 37, col 26 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 37, col 33 to line 37, col 37 of module AddSeq: 5187
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 37, col 44 to line 37, col 46 of module AddSeq: 1485980
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 67, col 40 to line 67, col 40 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 67, col 48 to line 67, col 56 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 67, col 48 to line 67, col 53 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 13 to line 37, col 46 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 37, col 16 to line 37, col 26 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 37, col 33 to line 37, col 37 of module AddSeq: 5187
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 37, col 44 to line 37, col 46 of module AddSeq: 1485980
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 67, col 52 to line 67, col 52 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 67, col 60 to line 67, col 64 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 69, col 28 to line 69, col 51 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 69, col 38 to line 69, col 50 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 69, col 38 to line 69, col 42 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 67, col 36 to line 67, col 64 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 67, col 36 to line 67, col 56 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 67, col 36 to line 67, col 44 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 67, col 36 to line 67, col 41 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 37, col 13 to line 37, col 46 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 16 to line 37, col 26 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 33 to line 37, col 37 of module AddSeq: 5187
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 44 to line 37, col 46 of module AddSeq: 1485980
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 67, col 40 to line 67, col 40 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 67, col 48 to line 67, col 56 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 67, col 48 to line 67, col 53 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 37, col 13 to line 37, col 46 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 16 to line 37, col 26 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 33 to line 37, col 37 of module AddSeq: 5187
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||||line 37, col 44 to line 37, col 46 of module AddSeq: 1485980
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 67, col 52 to line 67, col 52 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 67, col 60 to line 67, col 64 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 70, col 23 to line 70, col 39 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 70, col 28 to line 70, col 39 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 70, col 33 to line 70, col 38 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 37, col 13 to line 37, col 46 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 37, col 16 to line 37, col 26 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 37, col 33 to line 37, col 37 of module AddSeq: 5187
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 37, col 44 to line 37, col 46 of module AddSeq: 1485980
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 70, col 37 to line 70, col 37 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 71, col 23 to line 71, col 39 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 71, col 28 to line 71, col 39 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 71, col 33 to line 71, col 38 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 37, col 13 to line 37, col 46 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 37, col 16 to line 37, col 26 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 37, col 33 to line 37, col 37 of module AddSeq: 5187
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 37, col 44 to line 37, col 46 of module AddSeq: 1485980
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 71, col 37 to line 71, col 37 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 72, col 23 to line 72, col 31 of module AddSeq: 1491167
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 73, col 23 to line 73, col 32 of module AddSeq: 2109
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 74, col 23 to line 74, col 34 of module AddSeq: 2109
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 75, col 23 to line 75, col 47 of module AddSeq: 2109
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(6) at 2024-10-15 15:48:29: 2,725,376 states generated (8,146,393 s/min), 1,495,385 distinct states found (4,469,840 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
2725376 states generated, 1495385 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 6.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 1 and the 95th percentile is 1).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 20137ms at (2024-10-15 15:48:29)
@!@!@ENDMSG 2186 @!@!@
