ℹ [2/18] Replayed Confirmation
info: lean/./././Confirmation.lean:195:0: 'Confirmation.authorized_target_is_bound' depends on axioms: [propext]
info: lean/./././Confirmation.lean:196:0: 'Confirmation.confirm_refines_step' does not depend on any axioms
info: lean/./././Confirmation.lean:197:0: 'Confirmation.reachable_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: lean/./././Confirmation.lean:198:0: 'Confirmation.at_most_one_write' depends on axioms: [propext, Classical.choice, Quot.sound]
info: lean/./././Confirmation.lean:199:0: 'Confirmation.burn_blocks_future_reserve' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [4/18] Replayed Client.Requests
info: lean/./././Client/Requests.lean:38:0: 'Client.Requests.semaphore_bound' depends on axioms: [propext, Quot.sound]
info: lean/./././Client/Requests.lean:39:0: 'Client.Requests.retry_variant_decreases' depends on axioms: [propext, Quot.sound]
ℹ [5/18] Replayed Client.Lifecycle
info: lean/./././Client/Lifecycle.lean:40:0: 'Client.Lifecycle.selected_owner_is_running' depends on axioms: [propext, Quot.sound]
ℹ [6/18] Replayed Client.Pagination
info: lean/./././Client/Pagination.lean:54:0: 'Client.Pagination.no_duplicate_page' depends on axioms: [propext]
info: lean/./././Client/Pagination.lean:55:0: 'Client.Pagination.budget_conserved' depends on axioms: [propext, Quot.sound]
info: lean/./././Client/Pagination.lean:56:0: 'Client.Pagination.follows_server_successor' depends on axioms: [propext]
ℹ [9/18] Replayed Grading.Retry
info: lean/./././Grading/Retry.lean:74:0: 'Grading.Retry.at_most_one_write' depends on axioms: [propext, Quot.sound]
info: lean/./././Grading/Retry.lean:75:0: 'Grading.Retry.reads_at_most_four_attempts' depends on axioms: [propext, Quot.sound]
ℹ [10/18] Replayed Grading.Scheduler
info: lean/./././Grading/Scheduler.lean:86:0: 'Grading.Scheduler.reachable_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: lean/./././Grading/Scheduler.lean:87:0: 'Grading.Scheduler.no_duplicate_dispatch' depends on axioms: [propext, Classical.choice, Quot.sound]
info: lean/./././Grading/Scheduler.lean:88:0: 'Grading.Scheduler.in_flight_cap' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [13/18] Replayed TypeScriptPagination
info: lean/./././TypeScriptPagination.lean:69:0: 'TypeScriptPagination.admitted_commit_refines_step' depends on axioms: [propext, Quot.sound]
info: lean/./././TypeScriptPagination.lean:70:0: 'TypeScriptPagination.other_caller_unchanged' depends on axioms: [propext]
info: lean/./././TypeScriptPagination.lean:71:0: 'TypeScriptPagination.total_request_bound' depends on axioms: [propext, Quot.sound]
ℹ [15/18] Replayed StudentConfirmation
info: lean/./././StudentConfirmation.lean:112:0: 'StudentConfirmation.reachable_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
info: lean/./././StudentConfirmation.lean:113:0: 'StudentConfirmation.authorized_payload_bound' depends on axioms: [propext]
info: lean/./././StudentConfirmation.lean:114:0: 'StudentConfirmation.expired_denied' depends on axioms: [propext, Quot.sound]
ℹ [17/18] Replayed ConfirmedWorkflow
info: lean/./././ConfirmedWorkflow.lean:116:0: 'ConfirmedWorkflow.plan_is_bound' depends on axioms: [propext]
info: lean/./././ConfirmedWorkflow.lean:117:0: 'ConfirmedWorkflow.only_confirmed_targets' depends on axioms: [propext]
info: lean/./././ConfirmedWorkflow.lean:118:0: 'ConfirmedWorkflow.bounded_dispatch' depends on axioms: [propext, Quot.sound]
info: lean/./././ConfirmedWorkflow.lean:119:0: 'ConfirmedWorkflow.no_false_unsent' depends on axioms: [propext]
Build completed successfully.
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 95 and seed 908349686476342339 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 16] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/Confirmation.tla
Parsing file /tmp/tlc-265339313696602514/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-265339313696602514/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-265339313696602514/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Confirmation
Linting of module Confirmation
Starting... (2026-09-23 21:07:48)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:48.
Error: Invariant NoBurnReplay is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ replay = FALSE
/\ burned = FALSE
/\ held = FALSE
/\ burnedEver = FALSE
/\ pc = (a :> "idle" @@ b :> "idle" @@ c :> "idle")
/\ writes = 0

State 2: <Check(a) line 9, col 13 to line 11, col 69 of module Confirmation>
/\ replay = FALSE
/\ burned = FALSE
/\ held = FALSE
/\ burnedEver = FALSE
/\ pc = (a :> "checked" @@ b :> "idle" @@ c :> "idle")
/\ writes = 0

State 3: <Reserve(a) line 12, col 15 to line 15, col 57 of module Confirmation>
/\ replay = FALSE
/\ burned = FALSE
/\ held = TRUE
/\ burnedEver = FALSE
/\ pc = (a :> "inflight" @@ b :> "idle" @@ c :> "idle")
/\ writes = 0

State 4: <Mismatch(b) line 19, col 16 to line 21, col 50 of module Confirmation>
/\ replay = FALSE
/\ burned = FALSE
/\ held = TRUE
/\ burnedEver = TRUE
/\ pc = (a :> "inflight" @@ b :> "idle" @@ c :> "idle")
/\ writes = 0

State 5: <Release(a) line 22, col 15 to line 25, col 65 of module Confirmation>
/\ replay = FALSE
/\ burned = FALSE
/\ held = FALSE
/\ burnedEver = TRUE
/\ pc = (a :> "idle" @@ b :> "idle" @@ c :> "idle")
/\ writes = 0

State 6: <Check(a) line 9, col 13 to line 11, col 69 of module Confirmation>
/\ replay = FALSE
/\ burned = FALSE
/\ held = FALSE
/\ burnedEver = TRUE
/\ pc = (a :> "checked" @@ b :> "idle" @@ c :> "idle")
/\ writes = 0

State 7: <Reserve(a) line 12, col 15 to line 15, col 57 of module Confirmation>
/\ replay = TRUE
/\ burned = FALSE
/\ held = TRUE
/\ burnedEver = TRUE
/\ pc = (a :> "inflight" @@ b :> "idle" @@ c :> "idle")
/\ writes = 0

173 states generated, 62 distinct states found, 11 states left on queue.
The depth of the complete state graph search is 7.
Finished in 00s at (2026-09-23 21:07:48)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 68 and seed 5658098193668490464 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 39] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/Confirmation.tla
Parsing file /tmp/tlc-13730460973805297882/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-13730460973805297882/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-13730460973805297882/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Confirmation
Linting of module Confirmation
Starting... (2026-09-23 21:07:49)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:49.
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.9E-16
184 states generated, 57 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 6.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 4).
Finished in 00s at (2026-09-23 21:07:49)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 79 and seed -561468569698858463 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 62] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/Clock.tla
Parsing file /tmp/tlc-1205272180499642283/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module Clock
Linting of module Clock
Starting... (2026-09-23 21:07:50)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:50.
Error: Invariant NoDoubleRedeem is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ now = 0
/\ spent = FALSE
/\ redemptions = 0
/\ expiredSuccess = FALSE

State 2: <Reserve(0) line 16, col 5 to line 22, col 65 of module Clock>
/\ now = 0
/\ spent = TRUE
/\ redemptions = 1
/\ expiredSuccess = FALSE

State 3: <Reserve(2) line 16, col 5 to line 22, col 65 of module Clock>
/\ now = 2
/\ spent = TRUE
/\ redemptions = 2
/\ expiredSuccess = TRUE

18 states generated, 8 distinct states found, 3 states left on queue.
The depth of the complete state graph search is 3.
Finished in 00s at (2026-09-23 21:07:50)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 67 and seed -2966808475509414708 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 84] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/Clock.tla
Parsing file /tmp/tlc-7215658437360945378/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module Clock
Linting of module Clock
Starting... (2026-09-23 21:07:50)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:50.
Error: Invariant NoDoubleRedeem is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ now = 0
/\ spent = FALSE
/\ redemptions = 0
/\ expiredSuccess = FALSE

State 2: <Reserve(0) line 16, col 5 to line 22, col 65 of module Clock>
/\ now = 0
/\ spent = TRUE
/\ redemptions = 1
/\ expiredSuccess = FALSE

State 3: <Observe(2) line 10, col 17 to line 13, col 60 of module Clock>
/\ now = 2
/\ spent = FALSE
/\ redemptions = 1
/\ expiredSuccess = FALSE

State 4: <Observe(0) line 10, col 17 to line 13, col 60 of module Clock>
/\ now = 0
/\ spent = FALSE
/\ redemptions = 1
/\ expiredSuccess = FALSE

State 5: <Reserve(0) line 16, col 5 to line 22, col 65 of module Clock>
/\ now = 0
/\ spent = TRUE
/\ redemptions = 2
/\ expiredSuccess = FALSE

40 states generated, 9 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 5.
Finished in 00s at (2026-09-23 21:07:50)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 57 and seed -3884263685608812037 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 107] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/Clock.tla
Parsing file /tmp/tlc-3799170918690796750/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module Clock
Linting of module Clock
Starting... (2026-09-23 21:07:51)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:51.
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.8E-18
33 states generated, 6 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 3 and the 95th percentile is 3).
Finished in 00s at (2026-09-23 21:07:51)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 57 and seed 7761560567956706513 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 130] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientRequests.tla
Parsing file /tmp/tlc-12187374685138860295/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-12187374685138860295/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-12187374685138860295/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module ClientRequests
Linting of module ClientRequests
Starting... (2026-09-23 21:07:52)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:52.
Error: Invariant OwnedClientClosed is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ attempts = (a :> 0 @@ b :> 0 @@ c :> 0)
/\ closed = (a :> FALSE @@ b :> FALSE @@ c :> FALSE)
/\ pc = (a :> "queued" @@ b :> "queued" @@ c :> "queued")

State 2: <Cancel(a) line 24, col 14 to line 27, col 34 of module ClientRequests>
/\ attempts = (a :> 0 @@ b :> 0 @@ c :> 0)
/\ closed = (a :> FALSE @@ b :> FALSE @@ c :> FALSE)
/\ pc = (a :> "done" @@ b :> "queued" @@ c :> "queued")

3 states generated, 3 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 2.
Finished in 00s at (2026-09-23 21:07:52)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 90 and seed -2320745698609409990 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 153] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientRequests.tla
Parsing file /tmp/tlc-841136873574133236/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-841136873574133236/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-841136873574133236/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module ClientRequests
Linting of module ClientRequests
Starting... (2026-09-23 21:07:53)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:53.
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.2E-13
7321 states generated, 2232 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 28.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 6 and the 95th percentile is 2).
Finished in 00s at (2026-09-23 21:07:53)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 55 and seed 7281963685688429461 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 178] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientCleanup.tla
Parsing file /tmp/tlc-10382912113488416929/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ClientCleanup
Linting of module ClientCleanup
Starting... (2026-09-23 21:07:54)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:54.
Error: Invariant ReplacementPreserved is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ replaced = FALSE
/\ phase = "idle"
/\ cache = 1

State 2: <Start line 7, col 10 to line 9, col 30 of module ClientCleanup>
/\ replaced = FALSE
/\ phase = "waiting"
/\ cache = 1

State 3: <Replace line 10, col 12 to line 11, col 63 of module ClientCleanup>
/\ replaced = TRUE
/\ phase = "waiting"
/\ cache = 2

State 4: <Finish line 12, col 11 to line 14, col 31 of module ClientCleanup>
/\ replaced = TRUE
/\ phase = "done"
/\ cache = 0

5 states generated, 5 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 4.
Finished in 00s at (2026-09-23 21:07:54)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 46 and seed -6719539345160680505 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 201] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientCleanup.tla
Parsing file /tmp/tlc-6820512406173430268/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ClientCleanup
Linting of module ClientCleanup
Starting... (2026-09-23 21:07:54)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:55.
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 = 0.0
5 states generated, 5 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-09-23 21:07:55)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 72 and seed 4304624363157646706 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 224] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientDispatch.tla
Parsing file /tmp/tlc-2670074449493775469/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ClientDispatch
Linting of module ClientDispatch
Starting... (2026-09-23 21:07:55)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:55.
Error: Invariant DispatchOpen is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ bad = FALSE
/\ closed = {}
/\ dispatched = FALSE
/\ cache = 1
/\ cleaned = FALSE

State 2: <Cleanup line 9, col 12 to line 11, col 43 of module ClientDispatch>
/\ bad = FALSE
/\ closed = {1}
/\ dispatched = FALSE
/\ cache = 0
/\ cleaned = TRUE

State 3: <Dispatch line 12, col 13 to line 16, col 44 of module ClientDispatch>
/\ bad = TRUE
/\ closed = {1}
/\ dispatched = TRUE
/\ cache = 0
/\ cleaned = TRUE

4 states generated, 4 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 3.
Finished in 00s at (2026-09-23 21:07:55)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 49 and seed -2573945647817554766 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 247] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientDispatch.tla
Parsing file /tmp/tlc-8395930858213803215/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ClientDispatch
Linting of module ClientDispatch
Starting... (2026-09-23 21:07:56)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:56.
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 = 0.0
5 states generated, 5 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 2 and the 95th percentile is 2).
Finished in 00s at (2026-09-23 21:07:56)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 61 and seed 1112200349618116012 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 270] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientPagination.tla
Parsing file /tmp/tlc-9945918797016436138/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-9945918797016436138/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-9945918797016436138/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module ClientPagination
Linting of module ClientPagination
Starting... (2026-09-23 21:07:57)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:58.
Error: Invariant NoSkippedSuccessor is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ phase = (a :> "active" @@ b :> "active")
/\ pages = (a :> <<>> @@ b :> <<>>)
/\ cursor = (a :> 1 @@ b :> 1)

State 2: <Fetch(a) line 11, col 13 to line 18, col 99 of module ClientPagination>
/\ phase = (a :> "done" @@ b :> "active")
/\ pages = (a :> <<1>> @@ b :> <<>>)
/\ cursor = (a :> 2 @@ b :> 1)

2 states generated, 2 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 2.
Finished in 01s at (2026-09-23 21:07:58)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 109 and seed -528722482061416948 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 293] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientPagination.tla
Parsing file /tmp/tlc-17466955285634565881/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-17466955285634565881/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-17466955285634565881/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module ClientPagination
Linting of module ClientPagination
Starting... (2026-09-23 21:07:58)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:07:59.
Progress(5) at 2026-09-23 21:07:59: 13 states generated, 9 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 9 total distinct states at (2026-09-23 21:07:59)
Finished checking temporal properties in 00s at 2026-09-23 21:07:59
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.0E-18
13 states generated, 9 distinct states found, 0 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 0, the maximum 2 and the 95th percentile is 2).
Finished in 01s at (2026-09-23 21:07:59)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 114 and seed -2091859048535471020 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 318] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientPagination.tla
Parsing file /tmp/tlc-7911291833206474056/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-7911291833206474056/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-7911291833206474056/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module ClientPagination
Linting of module ClientPagination
Starting... (2026-09-23 21:08:00)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:00.
Progress(5) at 2026-09-23 21:08:00: 13 states generated, 9 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 9 total distinct states at (2026-09-23 21:08:00)
Finished checking temporal properties in 00s at 2026-09-23 21:08:00
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.0E-18
13 states generated, 9 distinct states found, 0 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 0, the maximum 2 and the 95th percentile is 2).
Finished in 00s at (2026-09-23 21:08:00)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 77 and seed 5530705150061531361 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 342] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientPageBudget.tla
Parsing file /tmp/tlc-17216974188708119325/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ClientPageBudget
Linting of module ClientPageBudget
Starting... (2026-09-23 21:08:00)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:01.
Progress(2) at 2026-09-23 21:08:01: 3 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-09-23 21:08:01)
Error: Temporal property Termination was violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
/\ done = FALSE
/\ remaining = 3
/\ tick = FALSE

State 2: <More line 9, col 9 to line 11, col 43 of module ClientPageBudget>
/\ done = FALSE
/\ remaining = 3
/\ tick = TRUE

Back to state 1: <More line 9, col 9 to line 11, col 43 of module ClientPageBudget>

Finished checking temporal properties in 00s at 2026-09-23 21:08:01
3 states generated, 2 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 2.
Finished in 00s at (2026-09-23 21:08:01)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 4 and seed -526424261289600808 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 367] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ClientPageBudget.tla
Parsing file /tmp/tlc-10939749482731886227/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ClientPageBudget
Linting of module ClientPageBudget
Starting... (2026-09-23 21:08:01)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:01.
Progress(4) at 2026-09-23 21:08:01: 4 states generated, 4 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 4 total distinct states at (2026-09-23 21:08:01)
Finished checking temporal properties in 00s at 2026-09-23 21:08:02
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 = 0.0
4 states generated, 4 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 1 and the 95th percentile is 1).
Finished in 00s at (2026-09-23 21:08:02)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 95 and seed -5205774327372303816 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 391] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingRedirect.tla
Parsing file /tmp/tlc-13945383419364685402/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module GradingRedirect
Linting of module GradingRedirect
Starting... (2026-09-23 21:08:02)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:02.
Error: Invariant OneWrite is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ pc = "send"
/\ commits = 0

State 2: <Apply line 7, col 10 to line 7, col 69 of module GradingRedirect>
/\ pc = "response"
/\ commits = 1

State 3: <Redirect line 10, col 13 to line 12, col 32 of module GradingRedirect>
/\ pc = "send"
/\ commits = 1

State 4: <Apply line 7, col 10 to line 7, col 69 of module GradingRedirect>
/\ pc = "response"
/\ commits = 2

4 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
Finished in 00s at (2026-09-23 21:08:02)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 31 and seed -6945146467784932666 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 414] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingRedirect.tla
Parsing file /tmp/tlc-11870253184409491175/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module GradingRedirect
Linting of module GradingRedirect
Starting... (2026-09-23 21:08:03)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:03.
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 = 0.0
3 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-09-23 21:08:03)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 29 and seed -7571777521119163269 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 436] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingStride.tla
Parsing file /tmp/tlc-97417128806281000/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module GradingStride
Linting of module GradingStride
Starting... (2026-09-23 21:08:03)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:03.
Error: Invariant CapRespected is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ rejected = FALSE
/\ offset2 = 0
/\ active = 0

State 2: <Admit line 9, col 10 to line 12, col 30 of module GradingStride>
/\ rejected = FALSE
/\ offset2 = 3
/\ active = 1

State 3: <Finish line 13, col 11 to line 13, col 73 of module GradingStride>
/\ rejected = FALSE
/\ offset2 = 3
/\ active = 0

State 4: <Admit line 9, col 10 to line 12, col 30 of module GradingStride>
/\ rejected = FALSE
/\ offset2 = 6
/\ active = 2

4 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
Finished in 00s at (2026-09-23 21:08:03)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 32 and seed 7731526606091145251 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 459] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingStride.tla
Parsing file /tmp/tlc-477949275020733861/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module GradingStride
Linting of module GradingStride
Starting... (2026-09-23 21:08:04)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:04.
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 = 0.0
1 states generated, 1 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
Finished in 00s at (2026-09-23 21:08:04)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 11 and seed -2641722433995361003 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 482] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingRetry.tla
Parsing file /tmp/tlc-6565928996582560266/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module GradingRetry
Linting of module GradingRetry
Starting... (2026-09-23 21:08:04)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:05.
Error: Invariant OneWrite is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ attempts = 0
/\ pc = "ready"
/\ commits = 0

State 2: <Dispatch line 7, col 13 to line 10, col 32 of module GradingRetry>
/\ attempts = 1
/\ pc = "remote"
/\ commits = 0

State 3: <Remote line 12, col 11 to line 15, col 31 of module GradingRetry>
/\ attempts = 1
/\ pc = "response"
/\ commits = 1

State 4: <Response line 16, col 13 to line 19, col 46 of module GradingRetry>
/\ attempts = 1
/\ pc = "backoff"
/\ commits = 1

State 5: <Wake line 20, col 9 to line 21, col 42 of module GradingRetry>
/\ attempts = 1
/\ pc = "ready"
/\ commits = 1

State 6: <Dispatch line 7, col 13 to line 10, col 32 of module GradingRetry>
/\ attempts = 2
/\ pc = "remote"
/\ commits = 1

State 7: <Remote line 12, col 11 to line 15, col 31 of module GradingRetry>
/\ attempts = 2
/\ pc = "response"
/\ commits = 2

16 states generated, 15 distinct states found, 2 states left on queue.
The depth of the complete state graph search is 7.
Finished in 00s at (2026-09-23 21:08:05)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 103 and seed -8973719576772183263 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 506] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingRetry.tla
Parsing file /tmp/tlc-589821527344938506/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module GradingRetry
Linting of module GradingRetry
Starting... (2026-09-23 21:08:05)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:05.
Progress(4) at 2026-09-23 21:08:05: 6 states generated, 6 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 6 total distinct states at (2026-09-23 21:08:05)
Finished checking temporal properties in 00s at 2026-09-23 21:08:05
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 = 0.0
6 states generated, 6 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-09-23 21:08:05)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 72 and seed 5548155320597895752 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 529] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingRetry.tla
Parsing file /tmp/tlc-9751835107463054746/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module GradingRetry
Linting of module GradingRetry
Starting... (2026-09-23 21:08:06)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:06.
Progress(16) at 2026-09-23 21:08:06: 19 states generated, 19 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 19 total distinct states at (2026-09-23 21:08:06)
Finished checking temporal properties in 00s at 2026-09-23 21:08:06
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 = 0.0
19 states generated, 19 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 16.
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-09-23 21:08:06)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 57 and seed 6146416832848033900 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 554] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingBatch.tla
Parsing file /tmp/tlc-16065957631282132758/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-16065957631282132758/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-16065957631282132758/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module GradingBatch
Linting of module GradingBatch
Starting... (2026-09-23 21:08:07)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:07.
Error: Invariant NoDoubleGrade is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ rejected = FALSE
/\ target = <<1, 1>>
/\ waiting = FALSE
/\ pc = <<"queued", "queued">>
/\ sleeps = 0
/\ writes = <<0>>
/\ offset = 1

State 2: <Admit line 42, col 10 to line 42, col 63 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 1>>
/\ waiting = FALSE
/\ pc = <<"callback", "callback">>
/\ sleeps = 0
/\ writes = <<0>>
/\ offset = 3

State 3: <Callback(1) line 20, col 16 to line 23, col 73 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 1>>
/\ waiting = FALSE
/\ pc = <<"request", "callback">>
/\ sleeps = 0
/\ writes = <<0>>
/\ offset = 3

State 4: <Send(1) line 24, col 12 to line 27, col 69 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 1>>
/\ waiting = FALSE
/\ pc = <<"remote", "callback">>
/\ sleeps = 0
/\ writes = <<1>>
/\ offset = 3

State 5: <Callback(2) line 20, col 16 to line 23, col 73 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 1>>
/\ waiting = FALSE
/\ pc = <<"remote", "request">>
/\ sleeps = 0
/\ writes = <<1>>
/\ offset = 3

State 6: <Send(2) line 24, col 12 to line 27, col 69 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 1>>
/\ waiting = FALSE
/\ pc = <<"remote", "remote">>
/\ sleeps = 0
/\ writes = <<2>>
/\ offset = 3

30 states generated, 21 distinct states found, 6 states left on queue.
The depth of the complete state graph search is 6.
Finished in 00s at (2026-09-23 21:08:07)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 79 and seed -2348676993345800151 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 578] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingBatch.tla
Parsing file /tmp/tlc-5870251720376600890/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-5870251720376600890/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-5870251720376600890/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module GradingBatch
Linting of module GradingBatch
Starting... (2026-09-23 21:08:08)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:08.
Progress(1) at 2026-09-23 21:08:08: 1 states generated, 1 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 1 total distinct states at (2026-09-23 21:08:08)
Finished checking temporal properties in 00s at 2026-09-23 21:08:08
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 = 0.0
1 states generated, 1 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
The average outdegree of the complete state graph is 0 (minimum is 0, the maximum 0 and the 95th percentile is 0).
Finished in 00s at (2026-09-23 21:08:08)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 89 and seed 1038797388582610193 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 602] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingBatch.tla
Parsing file /tmp/tlc-10396738557012227983/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-10396738557012227983/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-10396738557012227983/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module GradingBatch
Linting of module GradingBatch
Starting... (2026-09-23 21:08:10)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:10.
Progress(17) at 2026-09-23 21:08:11: 214 states generated, 134 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 134 total distinct states at (2026-09-23 21:08:11)
Finished checking temporal properties in 00s at 2026-09-23 21:08:11
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.8E-16
214 states generated, 134 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 17.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3).
Finished in 01s at (2026-09-23 21:08:11)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 58 and seed 8898027218743914849 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 629] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingBatch.tla
Parsing file /tmp/tlc-10511438742205912301/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-10511438742205912301/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-10511438742205912301/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module GradingBatch
Linting of module GradingBatch
Starting... (2026-09-23 21:08:12)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:12.
Error: Invariant NoDoubleGrade is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"queued", "queued", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<0, 0, 0, 0>>
/\ offset = 1

State 2: <Admit line 42, col 10 to line 42, col 63 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"callback", "callback", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<0, 0, 0, 0>>
/\ offset = 3

State 3: <Callback(1) line 20, col 16 to line 23, col 73 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"request", "callback", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<0, 0, 0, 0>>
/\ offset = 3

State 4: <Send(1) line 24, col 12 to line 27, col 69 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"remote", "callback", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<1, 0, 0, 0>>
/\ offset = 3

State 5: <Callback(2) line 20, col 16 to line 23, col 73 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 1, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"remote", "request", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<1, 0, 0, 0>>
/\ offset = 3

State 6: <Send(2) line 24, col 12 to line 27, col 69 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 1, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"remote", "remote", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<2, 0, 0, 0>>
/\ offset = 3

31 states generated, 22 distinct states found, 7 states left on queue.
The depth of the complete state graph search is 6.
Finished in 00s at (2026-09-23 21:08:12)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 6 and seed -5018886247320574679 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 652] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingBatch.tla
Parsing file /tmp/tlc-7635755483922831508/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-7635755483922831508/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-7635755483922831508/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module GradingBatch
Linting of module GradingBatch
Starting... (2026-09-23 21:08:13)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:13.
Progress(17) at 2026-09-23 21:08:13: 214 states generated, 134 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 134 total distinct states at (2026-09-23 21:08:13)
Finished checking temporal properties in 00s at 2026-09-23 21:08:13
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.8E-16
214 states generated, 134 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 17.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3).
Finished in 00s at (2026-09-23 21:08:13)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 88 and seed 2615298258726515973 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 678] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingBatch.tla
Parsing file /tmp/tlc-18215280896287951897/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-18215280896287951897/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-18215280896287951897/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module GradingBatch
Linting of module GradingBatch
Starting... (2026-09-23 21:08:14)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:14.
Error: Invariant ZeroDelay is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"queued", "queued", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<0, 0, 0, 0>>
/\ offset = 1

State 2: <Admit line 42, col 10 to line 42, col 63 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"callback", "callback", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<0, 0, 0, 0>>
/\ offset = 3

State 3: <Callback(1) line 20, col 16 to line 23, col 73 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"done", "callback", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<0, 0, 0, 0>>
/\ offset = 3

State 4: <Callback(2) line 20, col 16 to line 23, col 73 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = FALSE
/\ pc = <<"done", "done", "queued", "queued">>
/\ sleeps = 0
/\ writes = <<0, 0, 0, 0>>
/\ offset = 3

State 5: <BatchSettled line 32, col 17 to line 37, col 69 of module GradingBatch>
/\ rejected = FALSE
/\ target = <<1, 2, 3, 4>>
/\ waiting = TRUE
/\ pc = <<"done", "done", "queued", "queued">>
/\ sleeps = 1
/\ writes = <<0, 0, 0, 0>>
/\ offset = 3

24 states generated, 18 distinct states found, 6 states left on queue.
The depth of the complete state graph search is 5.
Finished in 01s at (2026-09-23 21:08:14)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 122 and seed -5391946698261472748 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 702] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/GradingBatch.tla
Parsing file /tmp/tlc-9838891342821573382/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-9838891342821573382/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-9838891342821573382/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module GradingBatch
Linting of module GradingBatch
Starting... (2026-09-23 21:08:15)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:16.
Progress(17) at 2026-09-23 21:08:16: 214 states generated, 134 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 134 total distinct states at (2026-09-23 21:08:16)
Finished checking temporal properties in 00s at 2026-09-23 21:08:16
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.8E-16
214 states generated, 134 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 17.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3).
Finished in 01s at (2026-09-23 21:08:16)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 103 and seed 4657571144097831773 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 727] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/TypeScriptConfig.tla
Parsing file /tmp/tlc-15574185181396186905/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module TypeScriptConfig
Linting of module TypeScriptConfig
Starting... (2026-09-23 21:08:16)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:16.
Error: Invariant CredentialBound is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ changed = FALSE
/\ page = 0
/\ sentWith = 1
/\ globalConfig = 1
/\ saved = 1

State 2: <Fetch line 12, col 10 to line 15, col 54 of module TypeScriptConfig>
/\ changed = FALSE
/\ page = 1
/\ sentWith = 1
/\ globalConfig = 1
/\ saved = 1

State 3: <Reinitialize line 9, col 17 to line 11, col 54 of module TypeScriptConfig>
/\ changed = TRUE
/\ page = 1
/\ sentWith = 1
/\ globalConfig = 2
/\ saved = 1

State 4: <Fetch line 12, col 10 to line 15, col 54 of module TypeScriptConfig>
/\ changed = TRUE
/\ page = 2
/\ sentWith = 2
/\ globalConfig = 2
/\ saved = 1

5 states generated, 5 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 4.
Finished in 00s at (2026-09-23 21:08:17)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 79 and seed 1902245323302550692 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 749] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/TypeScriptConfig.tla
Parsing file /tmp/tlc-15090732430383241750/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module TypeScriptConfig
Linting of module TypeScriptConfig
Starting... (2026-09-23 21:08:17)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:17.
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 = 0.0
5 states generated, 5 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-09-23 21:08:17)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 81 and seed -2376777262976548195 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 773] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/StudentClaims.tla
Parsing file /tmp/tlc-17980835605056752476/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-17980835605056752476/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-17980835605056752476/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module StudentClaims
Linting of module StudentClaims
Starting... (2026-09-23 21:08:18)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:18.
Error: Invariant OneActive is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ now = 0
/\ phase = <<"idle", "idle">>
/\ claimed = FALSE
/\ deadline = 1

State 2: <Confirm(1) line 11, col 15 to line 15, col 30 of module StudentClaims>
/\ now = 0
/\ phase = <<"active", "idle">>
/\ claimed = TRUE
/\ deadline = 1

State 3: <Clock line 16, col 10 to line 17, col 50 of module StudentClaims>
/\ now = 2
/\ phase = <<"active", "idle">>
/\ claimed = TRUE
/\ deadline = 1

State 4: <Purge line 18, col 10 to line 21, col 46 of module StudentClaims>
/\ now = 2
/\ phase = <<"active", "idle">>
/\ claimed = FALSE
/\ deadline = 1

State 5: <Confirm(2) line 11, col 15 to line 15, col 30 of module StudentClaims>
/\ now = 2
/\ phase = <<"active", "active">>
/\ claimed = TRUE
/\ deadline = 3

33 states generated, 27 distinct states found, 9 states left on queue.
The depth of the complete state graph search is 5.
Finished in 00s at (2026-09-23 21:08:18)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 102 and seed 3154313840727011774 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 796] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/StudentClaims.tla
Parsing file /tmp/tlc-1532258381502515868/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-1532258381502515868/FiniteSets.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-1532258381502515868/Sequences.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module StudentClaims
Linting of module StudentClaims
Starting... (2026-09-23 21:08:19)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08: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.9E-17
49 states generated, 32 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 6.
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-09-23 21:08:19)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 93 and seed -3514967153362782622 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 819] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ReminderReceipt.tla
Parsing file /tmp/tlc-5845953884226193408/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ReminderReceipt
Linting of module ReminderReceipt
Starting... (2026-09-23 21:08:20)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08:20.
Error: Invariant NoFalseUnsent is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ done = FALSE
/\ applied = FALSE
/\ started = FALSE
/\ spent = FALSE
/\ reportsNoSend = FALSE

State 2: <Send line 8, col 9 to line 10, col 53 of module ReminderReceipt>
/\ done = FALSE
/\ applied = FALSE
/\ started = TRUE
/\ spent = TRUE
/\ reportsNoSend = FALSE

State 3: <Apply line 12, col 10 to line 13, col 61 of module ReminderReceipt>
/\ done = FALSE
/\ applied = TRUE
/\ started = TRUE
/\ spent = TRUE
/\ reportsNoSend = FALSE

State 4: <Exception line 14, col 14 to line 16, col 53 of module ReminderReceipt>
/\ done = TRUE
/\ applied = TRUE
/\ started = TRUE
/\ spent = TRUE
/\ reportsNoSend = TRUE

6 states generated, 6 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 4.
Finished in 00s at (2026-09-23 21:08:20)
TLC2 Version 2026.09.22.222048 (rev: 35d40c9)
Running breadth-first search Model-Checking with fp 61 and seed -3082560085646162180 with 1 worker on 8 cores with 4551MB heap and 64MB offheap memory [pid: 841] (Linux 6.18.44 amd64, Ubuntu 17.0.20 64bit, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspace/scratch/5655cab44c80/canvas-mcp-confirmation-workflows/verify/tla/ReminderReceipt.tla
Parsing file /tmp/tlc-1167161254898079402/Naturals.tla (jar:file:/workspace/scratch/5655cab44c80/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Semantic processing of module Naturals
Semantic processing of module ReminderReceipt
Linting of module ReminderReceipt
Starting... (2026-09-23 21:08:21)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2026-09-23 21:08: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 = 3.3E-19
7 states generated, 6 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 01s at (2026-09-23 21:08:22)
