@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.20 of Day Month 20??
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 15 and seed 7738505963619240447 with 4 workers on 8 cores with 1193MB heap and 2683MB offheap memory [pid: 27136] (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\OneBit.toolbox\InductiveInv\MC.tla
Parsing file C:\lamport\books\fred\book-specs\OneBit.toolbox\InductiveInv\OneBit.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\Naturals.tla
Parsing file C:\cygwin\usr\local\lib\tlaps\TLAPS.tla
Parsing file C:\lamport\books\fred\book-specs\OneBit.toolbox\InductiveInv\LockMutex.tla
Parsing file C:\Users\lamport\tlaplus-master\git\tlaplus\tlatools\org.lamport.tlatools\class\tla2sany\StandardModules\Sequences.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 TLAPS
Semantic processing of module LockMutex
Semantic processing of module OneBit
Semantic processing of module Sequences
Semantic processing of module FiniteSets
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:35:07)
@!@!@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 2190:0 @!@!@
Finished computing initial states: 95 distinct states generated at 2024-10-20 16:35:09.
@!@!@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 = 8.9E-16
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2024-10-20 16:35:09
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<InvUM line 113, col 1 to line 113, col 5 of module OneBit>: 95:196
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 97, col 20 to line 97, col 37 of module OneBit: 1:8
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 97, col 21 to line 97, col 25 of module OneBit: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 97, col 30 to line 97, col 36 of module OneBit: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 98, col 14 to line 98, col 78 of module OneBit: 95
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 98, col 21 to line 98, col 78 of module OneBit: 4:392
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 98, col 22 to line 98, col 26 of module OneBit: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 98, col 31 to line 98, col 77 of module OneBit: 4:260
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 99, col 14 to line 99, col 38 of module OneBit: 196
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 114, col 13 to line 115, col 67 of module OneBit: 140
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 114, col 31 to line 115, col 67 of module OneBit: 250
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 114, col 34 to line 114, col 64 of module OneBit: 250
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 114, col 35 to line 114, col 55 of module OneBit: 250
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 114, col 61 to line 114, col 64 of module OneBit: 86
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 115, col 34 to line 115, col 67 of module OneBit: 207
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 115, col 35 to line 115, col 46 of module OneBit: 207
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 115, col 53 to line 115, col 66 of module OneBit: 21
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 114, col 22 to line 114, col 27 of module OneBit: 140:390
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Ncs line 43, col 1 to line 43, col 6 of module OneBit>: 0:40
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 43, col 14 to line 43, col 26 of module OneBit: 230
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 43, col 14 to line 43, col 18 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 44, col 14 to line 44, col 17 of module OneBit: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 45, col 14 to line 45, col 44 of module OneBit: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 46, col 14 to line 46, col 19 of module OneBit: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Wait line 48, col 1 to line 48, col 7 of module OneBit>: 0:40
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 48, col 15 to line 48, col 28 of module OneBit: 230
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 48, col 15 to line 48, col 19 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 49, col 15 to line 49, col 41 of module OneBit: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 50, col 15 to line 50, col 43 of module OneBit: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<W2 line 52, col 1 to line 52, col 5 of module OneBit>: 0:13
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 52, col 13 to line 52, col 24 of module OneBit: 203
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 52, col 13 to line 52, col 17 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 53, col 17 to line 53, col 19 of module OneBit: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 54, col 24 to line 54, col 28 of module OneBit: 17
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 54, col 25 to line 54, col 28 of module OneBit: 12
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 55, col 24 to line 55, col 52 of module OneBit: 5
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 56, col 27 to line 56, col 30 of module OneBit: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 57, col 32 to line 57, col 63 of module OneBit: 5
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 58, col 32 to line 58, col 63 of module OneBit: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 59, col 13 to line 59, col 18 of module OneBit: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<W3 line 61, col 1 to line 61, col 5 of module OneBit>: 0:16
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 61, col 13 to line 61, col 24 of module OneBit: 206
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 61, col 13 to line 61, col 17 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 62, col 13 to line 62, col 40 of module OneBit: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 63, col 13 to line 63, col 41 of module OneBit: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<W4 line 65, col 1 to line 65, col 5 of module OneBit>: 0:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 65, col 13 to line 65, col 24 of module OneBit: 196
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 65, col 13 to line 65, col 17 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 66, col 13 to line 66, col 18 of module OneBit: 22
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 66, col 15 to line 66, col 18 of module OneBit: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 67, col 13 to line 67, col 43 of module OneBit: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 68, col 13 to line 68, col 18 of module OneBit: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Cs line 70, col 1 to line 70, col 5 of module OneBit>: 0:18
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 70, col 13 to line 70, col 24 of module OneBit: 208
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 70, col 13 to line 70, col 17 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 71, col 13 to line 71, col 43 of module OneBit: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 72, col 13 to line 72, col 18 of module OneBit: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Exit line 74, col 1 to line 74, col 7 of module OneBit>: 0:40
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 74, col 15 to line 74, col 28 of module OneBit: 230
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 74, col 15 to line 74, col 19 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 75, col 15 to line 75, col 42 of module OneBit: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 76, col 15 to line 76, col 44 of module OneBit: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<InvUM line 113, col 1 to line 113, col 5 of module OneBit>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 113, col 10 to line 115, col 67 of module OneBit: 95
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 113, col 13 to line 113, col 18 of module OneBit: 95
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 114, col 13 to line 115, col 67 of module OneBit: 95
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 114, col 31 to line 115, col 67 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 114, col 34 to line 114, col 64 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 114, col 35 to line 114, col 55 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 114, col 61 to line 114, col 64 of module OneBit: 38
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 115, col 34 to line 115, col 67 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 115, col 35 to line 115, col 46 of module OneBit: 190
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 115, col 53 to line 115, col 66 of module OneBit: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 114, col 22 to line 114, col 27 of module OneBit: 95:285
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(1) at 2024-10-20 16:35:09: 268 states generated (2,285 s/min), 95 distinct states found (810 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
268 states generated, 95 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 1.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 7087ms at (2024-10-20 16:35:09)
@!@!@ENDMSG 2186 @!@!@
