== TLC [standard]: OnlineScanner.tla ==
TLC2 Version 2.20 of Day Month 20?? (rev: bb62e53)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 48 and seed 8358357651215939041 with 1 worker on 8 cores with 4096MB heap and 64MB offheap memory [pid: 263301] (Linux 7.0.7-arch1-1 amd64, Arch Linux 26.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/OnlineScanner.tla
Parsing file /tmp/tlc-6405879849068740006/Integers.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-6405879849068740006/Sequences.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-6405879849068740006/FiniteSets.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-6405879849068740006/TLC.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-6405879849068740006/_TLCTrace.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-6405879849068740006/Naturals.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-6405879849068740006/TLCExt.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module OnlineScanner
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module OnlineScanner
Starting... (2026-05-27 11:38:18)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-05-27 11:38:18.
Progress(4) at 2026-05-27 11:38:18: 23 states generated, 15 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 15 total distinct states at (2026-05-27 11:38:18)
Finished checking temporal properties in 00s at 2026-05-27 11:38:18
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 = 6.5E-18
23 states generated, 15 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
Finished in 00s at (2026-05-27 11:38:18)
Command being timed: "java -Xmx4G -jar /home/dylon/.tla/tla2tools.jar -config /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/OnlineScanner.cfg /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/OnlineScanner.tla"
User time (seconds): 0.99
System time (seconds): 0.09
Percent of CPU this job got: 147%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.73
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 112188
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 23992
Voluntary context switches: 3980
Involuntary context switches: 74
Swaps: 0
File system inputs: 8
File system outputs: 16
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 0
== TLC [standard]: PriorityQuery.tla ==
TLC2 Version 2.20 of Day Month 20?? (rev: bb62e53)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 110 and seed 6418855591153873661 with 1 worker on 8 cores with 4096MB heap and 64MB offheap memory [pid: 263354] (Linux 7.0.7-arch1-1 amd64, Arch Linux 26.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/PriorityQuery.tla
Parsing file /tmp/tlc-14140402307673395203/Integers.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-14140402307673395203/Sequences.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-14140402307673395203/FiniteSets.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-14140402307673395203/TLC.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-14140402307673395203/_TLCTrace.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-14140402307673395203/Naturals.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-14140402307673395203/TLCExt.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module PriorityQuery
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module PriorityQuery
Starting... (2026-05-27 11:38:19)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-05-27 11:38:19.
Progress(2) at 2026-05-27 11:38:19: 4 states generated, 2 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 2 total distinct states at (2026-05-27 11:38:19)
Finished checking temporal properties in 00s at 2026-05-27 11:38:19
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.2E-19
4 states generated, 2 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 2.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 00s at (2026-05-27 11:38:19)
Command being timed: "java -Xmx4G -jar /home/dylon/.tla/tla2tools.jar -config /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/PriorityQuery.cfg /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/PriorityQuery.tla"
User time (seconds): 1.00
System time (seconds): 0.07
Percent of CPU this job got: 144%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.74
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 115196
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 1
Minor (reclaiming a frame) page faults: 24542
Voluntary context switches: 3817
Involuntary context switches: 97
Swaps: 0
File system inputs: 240
File system outputs: 16
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 0
== TLC [standard]: ProductAutomaton.tla ==
TLC2 Version 2.20 of Day Month 20?? (rev: bb62e53)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 23 and seed -47771783433409907 with 1 worker on 8 cores with 4096MB heap and 64MB offheap memory [pid: 263410] (Linux 7.0.7-arch1-1 amd64, Arch Linux 26.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/ProductAutomaton.tla
Parsing file /tmp/tlc-6166969321333387586/Integers.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-6166969321333387586/Sequences.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-6166969321333387586/FiniteSets.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-6166969321333387586/TLC.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-6166969321333387586/_TLCTrace.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-6166969321333387586/Naturals.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-6166969321333387586/TLCExt.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module ProductAutomaton
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module ProductAutomaton
Starting... (2026-05-27 11:38:20)
Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-05-27 11:38:20.
Progress(3) at 2026-05-27 11:38:20: 9 states generated, 3 distinct states found, 0 states left on queue.
Checking 2 branches of temporal properties for the complete state space with 6 total distinct states at (2026-05-27 11:38:20)
Finished checking temporal properties in 00s at 2026-05-27 11:38:20
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 = 9.8E-19
9 states generated, 3 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
Finished in 00s at (2026-05-27 11:38:20)
Command being timed: "java -Xmx4G -jar /home/dylon/.tla/tla2tools.jar -config /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/ProductAutomaton.cfg /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/ProductAutomaton.tla"
User time (seconds): 0.93
System time (seconds): 0.10
Percent of CPU this job got: 141%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.73
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 110024
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 0
Minor (reclaiming a frame) page faults: 23297
Voluntary context switches: 3260
Involuntary context switches: 54
Swaps: 0
File system inputs: 8
File system outputs: 32
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 0
== TLC [light]: Subsumption.tla ==
TLC2 Version 2.20 of Day Month 20?? (rev: bb62e53)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 38 and seed 6149964340344732322 with 1 worker on 4 cores with 2048MB heap and 64MB offheap memory [pid: 263464] (Linux 7.0.7-arch1-1 amd64, Arch Linux 26.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/Subsumption.tla
Parsing file /tmp/tlc-10027168621281595145/Integers.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-10027168621281595145/FiniteSets.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-10027168621281595145/TLC.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-10027168621281595145/_TLCTrace.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-10027168621281595145/Naturals.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-10027168621281595145/Sequences.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-10027168621281595145/TLCExt.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module Subsumption
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module Subsumption
Starting... (2026-05-27 11:38:20)
Warning: The invariant Irreflexive is a constant-level formula (i.e., it contains no variables, primes, or temporal operators) and evaluates to TRUE. To assert constant-level formulas in your spec, use ASSUME ConstInv. If you optionally want to give the assumption a name, write ASSUME YourAssumption == ConstInv instead. See
https://explain.tlapl.us/assumptions-and-invariants for additional details.
Warning: The invariant Asymmetric is a constant-level formula (i.e., it contains no variables, primes, or temporal operators) and evaluates to TRUE. To assert constant-level formulas in your spec, use ASSUME ConstInv. If you optionally want to give the assumption a name, write ASSUME YourAssumption == ConstInv instead. See
https://explain.tlapl.us/assumptions-and-invariants for additional details.
Warning: The invariant Transitive is a constant-level formula (i.e., it contains no variables, primes, or temporal operators) and evaluates to TRUE. To assert constant-level formulas in your spec, use ASSUME ConstInv. If you optionally want to give the assumption a name, write ASSUME YourAssumption == ConstInv instead. See
https://explain.tlapl.us/assumptions-and-invariants for additional details.
Warning: The invariant CompletionPreservationInv is a constant-level formula (i.e., it contains no variables, primes, or temporal operators) and evaluates to TRUE. To assert constant-level formulas in your spec, use ASSUME ConstInv. If you optionally want to give the assumption a name, write ASSUME YourAssumption == ConstInv instead. See
https://explain.tlapl.us/assumptions-and-invariants for additional details.
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-05-27 11:38:21.
Progress(7) at 2026-05-27 11:38:21: 321 states generated, 64 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 64 total distinct states at (2026-05-27 11:38:21)
Finished checking temporal properties in 00s at 2026-05-27 11:38:21
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
321 states generated, 64 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 7.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 6 and the 95th percentile is 4).
Finished in 01s at (2026-05-27 11:38:21)
Command being timed: "java -Xmx2G -jar /home/dylon/.tla/tla2tools.jar -config /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/Subsumption.cfg /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/Subsumption.tla"
User time (seconds): 2.68
System time (seconds): 0.19
Percent of CPU this job got: 162%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:01.77
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 348668
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 1
Minor (reclaiming a frame) page faults: 83157
Voluntary context switches: 3374
Involuntary context switches: 94
Swaps: 0
File system inputs: 96
File system outputs: 16
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 0
== TLC [standard]: ValueYieldingQuery.tla ==
TLC2 Version 2.20 of Day Month 20?? (rev: bb62e53)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 73 and seed 5122789457347802393 with 1 worker on 8 cores with 4096MB heap and 64MB offheap memory [pid: 263526] (Linux 7.0.7-arch1-1 amd64, Arch Linux 26.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/ValueYieldingQuery.tla
Parsing file /tmp/tlc-14328063582077007608/Integers.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-14328063582077007608/FiniteSets.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-14328063582077007608/TLC.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-14328063582077007608/_TLCTrace.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-14328063582077007608/Naturals.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-14328063582077007608/Sequences.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-14328063582077007608/TLCExt.tla (jar:file:/home/dylon/.tla/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module ValueYieldingQuery
Linting of module TLCExt
Linting of module _TLCTrace
Linting of module ValueYieldingQuery
Starting... (2026-05-27 11:38:22)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-05-27 11:38:22.
Progress(8) at 2026-05-27 11:38:22: 65 states generated, 31 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 31 total distinct states at (2026-05-27 11:38:22)
Finished checking temporal properties in 00s at 2026-05-27 11:38:22
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 = 5.7E-17
65 states generated, 31 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 8.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 3 and the 95th percentile is 3).
Finished in 00s at (2026-05-27 11:38:22)
Command being timed: "java -Xmx4G -jar /home/dylon/.tla/tla2tools.jar -config /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/ValueYieldingQuery.cfg /home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/docs/verification/tla/ValueYieldingQuery.tla"
User time (seconds): 0.93
System time (seconds): 0.09
Percent of CPU this job got: 142%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.72
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 110428
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 1
Minor (reclaiming a frame) page faults: 23214
Voluntary context switches: 3925
Involuntary context switches: 75
Swaps: 0
File system inputs: 0
File system outputs: 16
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 4096
Exit status: 0