TLC2 Version 2.19 of 08 August 2024 (rev: 5a47802)
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 26 and seed -7103193436448417687 with 1 worker on 8 cores with 4002MB heap and 64MB offheap memory [pid: 480577] (Linux 6.12.94+ amd64, Eclipse Adoptium 21.0.13 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/tla-tutorial/Login.tla
Parsing file /tmp/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module Login
Starting... (2026-10-30 11:04:41)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-10-30 11:04:41.
Error: Invariant AtMostOneSession is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 0
/\ pc = [t1 |-> "start", t2 |-> "start"]

State 2: <Check line 13, col 13 to line 16, col 33 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 0
/\ pc = [t1 |-> "checked", t2 |-> "start"]

State 3: <Check line 13, col 13 to line 16, col 33 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 0
/\ pc = [t1 |-> "checked", t2 |-> "checked"]

State 4: <Create line 18, col 14 to line 21, col 30 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 1
/\ pc = [t1 |-> "done", t2 |-> "checked"]

State 5: <Create line 18, col 14 to line 21, col 30 of module Login>
/\ seen = [t1 |-> 0, t2 |-> 0]
/\ sessions = 2
/\ pc = [t1 |-> "done", t2 |-> "done"]

13 states generated, 12 distinct states found, 3 states left on queue.
The depth of the complete state graph search is 5.
The average outdegree of the complete state graph is 1 (minimum is 1, the maximum 2 and the 95th percentile is 2).
Finished in 00s at (2026-10-30 11:04:41)
