@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.20 of Day Month 20??
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 98 and seed -7318712818714006935 with 4 workers on 8 cores with 1193MB heap and 2683MB offheap memory [pid: 12456] (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\ICen1.toolbox\ICen1_p_implies_ICen2\MC.tla
Parsing file C:\lamport\books\fred\book-specs\ICen1.toolbox\ICen1_p_implies_ICen2\ICen1.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\ICen1.toolbox\ICen1_p_implies_ICen2\ICen2.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 ICen2
Semantic processing of module ICen1
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-16 15:16:51)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 1 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@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 2190:0 @!@!@
Finished computing initial states: 20 distinct states generated at 2024-10-16 15:16:52.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(3) at 2024-10-16 15:16:52: 520 states generated, 220 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking temporal properties for the complete state space with 220 total distinct states at (2024-10-16 15:16:52)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2024-10-16 15:16:52
@!@!@ENDMSG 2267 @!@!@
@!@!@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 = 3.6E-15
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2024-10-16 15:16:52
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init_p line 82, col 1 to line 82, col 6 of module ICen1>: 20:20
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 35, col 14 to line 35, col 25 of module ICen1: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 36, col 14 to line 36, col 23 of module ICen1: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  line 37, col 23 to line 37, col 34 of module ICen1: 1:20
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 37, col 23 to line 37, col 25 of module ICen1: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 11, col 1 to line 11, col 20 of module MC: 1:6
@!@!@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 11, col 18 to line 11, col 19 of module MC: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |line 37, col 30 to line 37, col 34 of module ICen1: 1:16
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 82, col 20 to line 82, col 26 of module ICen1: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 82, col 25 to line 82, col 26 of module ICen1: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Input_p line 84, col 1 to line 84, col 7 of module ICen1>: 100:200
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 39, col 14 to line 39, col 25 of module ICen1: 240
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 39, col 14 to line 39, col 16 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 39, col 20 to line 39, col 25 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 39, col 32 to line 39, col 41 of module ICen1: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 39, col 32 to line 39, col 33 of module ICen1: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 39, col 37 to line 39, col 41 of module ICen1: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 40, col 13 to line 40, col 24 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 40, col 22 to line 40, col 24 of module ICen1: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  ||line 11, col 1 to line 11, col 20 of module MC: 20:120
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 2 to line 11, col 3 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 6 to line 11, col 7 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 10 to line 11, col 11 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 14 to line 11, col 15 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 11, col 18 to line 11, col 19 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 41, col 13 to line 41, col 26 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 42, col 13 to line 42, col 24 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 84, col 35 to line 84, col 40 of module ICen1: 200
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 84, col 30 to line 84, col 31 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Ack_p line 86, col 1 to line 86, col 5 of module ICen1>: 0:100
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 51, col 14 to line 51, col 24 of module ICen1: 320
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 51, col 14 to line 51, col 16 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 51, col 22 to line 51, col 24 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 51, col 31 to line 51, col 40 of module ICen1: 300
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 51, col 31 to line 51, col 32 of module ICen1: 200
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 51, col 36 to line 51, col 40 of module ICen1: 200
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 52, col 13 to line 52, col 25 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 53, col 13 to line 53, col 40 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 86, col 18 to line 86, col 21 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<DispOrNot_p line 94, col 1 to line 94, col 11 of module ICen1>: 100:200
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 88, col 15 to line 88, col 24 of module ICen1: 320
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 88, col 15 to line 88, col 16 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 88, col 20 to line 88, col 24 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 89, col 23 to line 89, col 31 of module ICen1: 150
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 89, col 23 to line 89, col 23 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 89, col 38 to line 89, col 65 of module ICen1: 50
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 90, col 23 to line 90, col 30 of module ICen1: 150
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 90, col 23 to line 90, col 23 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 90, col 37 to line 90, col 48 of module ICen1: 50
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 91, col 19 to line 91, col 29 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 92, col 19 to line 92, col 31 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 94, col 21 to line 94, col 21 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 94, col 28 to line 94, col 35 of module ICen1: 200
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 94, col 34 to line 94, col 35 of module ICen1: 100
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<TypeOK_p line 80, col 1 to line 80, col 8 of module ICen1>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 80, col 13 to line 80, col 31 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 80, col 13 to line 80, col 18 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 31, col 11 to line 33, col 28 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 31, col 14 to line 31, col 38 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 31, col 14 to line 31, col 16 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 31, col 22 to line 31, col 38 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||||line 31, col 22 to line 31, col 24 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
  |||||line 31, col 31 to line 31, col 38 of module ICen1: 220:440
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||||line 31, col 32 to line 31, col 37 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 32, col 14 to line 32, col 34 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 33, col 14 to line 33, col 28 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 80, col 24 to line 80, col 30 of module ICen1: 220
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2778:0 @!@!@
<constr_172908461028131000 line 15, col 1 to line 15, col 25 of module MC>: 520:520
@!@!@ENDMSG 2778 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 16, col 1 to line 16, col 9 of module MC: 520
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(3) at 2024-10-16 15:16:52: 520 states generated (14,593 s/min), 220 distinct states found (6,173 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
520 states generated, 220 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 3.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 9 and the 95th percentile is 5).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 2153ms at (2024-10-16 15:16:52)
@!@!@ENDMSG 2186 @!@!@
