@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.20 of Day Month 20??
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 82 and seed -9137419877566919682 with 4 workers on 8 cores with 1193MB heap and 2683MB offheap memory [pid: 29980] (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\Increment.toolbox\Model_1\MC.tla
Parsing file C:\lamport\books\fred\book-specs\Increment.toolbox\Model_1\Increment.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:\cygwin\usr\local\lib\tlaps\FiniteSets.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\TLAPS.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\FiniteSetTheorems.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\Functions.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\WellFoundedInduction.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\NaturalsInduction.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Sequences.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 TLAPS
Semantic processing of module Functions
Semantic processing of module NaturalsInduction
Semantic processing of module WellFoundedInduction
Semantic processing of module FiniteSetTheorems
Semantic processing of module Increment
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2024-10-20 16:37:39)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1 distinct state generated at 2024-10-20 16:37:40.
@!@!@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 = 2.1E-14
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2024-10-20 16:37:40
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 20, col 1 to line 20, col 4 of module Increment>: 1:1
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 21, col 16 to line 21, col 34 of module Increment: 1:4
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 21, col 23 to line 21, col 27 of module Increment: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 11, col 1 to line 11, col 16 of module MC: 1:5
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 2 to line 11, col 3 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 6 to line 11, col 7 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 10 to line 11, col 11 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 14 to line 11, col 15 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 22, col 12 to line 22, col 37 of module Increment: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 22, col 17 to line 22, col 37 of module Increment: 1:4
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 22, col 24 to line 22, col 28 of module Increment: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||line 11, col 1 to line 11, col 16 of module MC: 1:5
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 2 to line 11, col 3 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 6 to line 11, col 7 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 10 to line 11, col 11 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 14 to line 11, col 15 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<aStep line 24, col 1 to line 24, col 8 of module Increment>: 242:336
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 24, col 16 to line 24, col 26 of module Increment: 3356
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 24, col 16 to line 24, col 20 of module Increment: 3020
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 25, col 16 to line 25, col 21 of module Increment: 336
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 26, col 16 to line 26, col 39 of module Increment: 336
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 27, col 16 to line 27, col 43 of module Increment: 336
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<bStep line 29, col 1 to line 29, col 8 of module Increment>: 512:820
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 29, col 16 to line 29, col 26 of module Increment: 3840
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 29, col 16 to line 29, col 20 of module Increment: 3020
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 30, col 16 to line 30, col 28 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 31, col 16 to line 31, col 21 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 32, col 16 to line 32, col 46 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Stutter line 36, col 1 to line 36, col 7 of module Increment>: 0:109
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 36, col 31 to line 36, col 44 of module Increment: 2123
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 36, col 31 to line 36, col 35 of module Increment: 1687
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 36, col 24 to line 36, col 28 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 11, col 1 to line 11, col 16 of module MC: 755:3775
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 2 to line 11, col 3 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 6 to line 11, col 7 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 10 to line 11, col 11 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 11, col 14 to line 11, col 15 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 37, col 15 to line 37, col 36 of module Increment: 109
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<Inv line 71, col 1 to line 71, col 3 of module Increment>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 71, col 8 to line 73, col 25 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 71, col 11 to line 71, col 16 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 72, col 11 to line 72, col 64 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 72, col 28 to line 72, col 64 of module Increment: 3020
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 72, col 29 to line 72, col 39 of module Increment: 3020
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 72, col 46 to line 72, col 63 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 72, col 46 to line 72, col 49 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 72, col 54 to line 72, col 63 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 69, col 15 to line 69, col 57 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 69, col 27 to line 69, col 56 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 69, col 42 to line 69, col 55 of module Increment: 3280
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 69, col 34 to line 69, col 38 of module Increment: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||||||line 11, col 1 to line 11, col 16 of module MC: 820:4100
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 2 to line 11, col 3 of module MC: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 6 to line 11, col 7 of module MC: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 10 to line 11, col 11 of module MC: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||||line 11, col 14 to line 11, col 15 of module MC: 820
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 72, col 20 to line 72, col 24 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||line 11, col 1 to line 11, col 16 of module MC: 755:3775
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 2 to line 11, col 3 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 6 to line 11, col 7 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 10 to line 11, col 11 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 11, col 14 to line 11, col 15 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 73, col 11 to line 73, col 25 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 73, col 11 to line 73, col 11 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 73, col 16 to line 73, col 25 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 69, col 15 to line 69, col 57 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 69, col 27 to line 69, col 56 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 69, col 42 to line 69, col 55 of module Increment: 3020
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 69, col 34 to line 69, col 38 of module Increment: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||||||line 11, col 1 to line 11, col 16 of module MC: 755:3775
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 2 to line 11, col 3 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 6 to line 11, col 7 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 10 to line 11, col 11 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||||line 11, col 14 to line 11, col 15 of module MC: 755
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(9) at 2024-10-20 16:37:40: 1,266 states generated (30,262 s/min), 755 distinct states found (18,047 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
1266 states generated, 755 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 9.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 2522ms at (2024-10-20 16:37:40)
@!@!@ENDMSG 2186 @!@!@
