step.out

@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.15 of Day Month 20?? (rev: d977051)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 12 and seed 5016491069357648850 with 1 worker on 8 cores with 3524MB heap and 64MB offheap memory [pid: 7495] (Linux 5.4.0-72-generic amd64, Ubuntu 11.0.11 x86_64, MSBDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/a/projects/tla-specs/asyncio-lock/step2.tla
Parsing file /tmp/TLC.tla (jar:file:/home/a/.vscode/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/Sequences.tla (jar:file:/home/a/.vscode/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /home/a/projects/tla-specs/asyncio-lock/step1.tla
Parsing file /tmp/Naturals.tla (jar:file:/home/a/.vscode/extensions/alygin.vscode-tlaplus-1.5.4/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/FiniteSets.tla (jar:file:/home/a/.vscode/extensions/alygin.vscode-tlaplus-1.5.4/tools/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 TLC
Semantic processing of module step1
Semantic processing of module step2
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2021-05-12 12:57:00)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 2 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1 distinct state generated at 2021-05-12 12:57:00.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(7) at 2021-05-12 12:57:00: 208 states generated, 116 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 2 branches of temporal properties for the complete state space with 232 total distinct states at (2021-05-12 12:57:00)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2116:1 @!@!@
Temporal properties were violated.

@!@!@ENDMSG 2116 @!@!@
@!@!@STARTMSG 2264:1 @!@!@
The following behavior constitutes a counter-example:

@!@!@ENDMSG 2264 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ waiters = <<>>
/\ lockState = unlocked
/\ taskStates = (Task1 :> running @@ Task2 :> running @@ Task3 :> running)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <s1!Acquire line 19, col 1 to line 19, col 20 of module step2>
/\ waiters = <<>>
/\ lockState = locked
/\ taskStates = (Task1 :> acquired @@ Task2 :> running @@ Task3 :> running)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <s1!Acquire line 19, col 1 to line 19, col 20 of module step2>
/\ waiters = <<Task3>>
/\ lockState = locked
/\ taskStates = (Task1 :> acquired @@ Task2 :> running @@ Task3 :> waiting)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <Cancel line 25, col 3 to line 27, col 37 of module step2>
/\ waiters = <<Task3>>
/\ lockState = locked
/\ taskStates = (Task1 :> acquired @@ Task2 :> running @@ Task3 :> canceled)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
5: <s1!Release line 19, col 1 to line 19, col 20 of module step2>
/\ waiters = <<Task3>>
/\ lockState = unlocked
/\ taskStates = (Task1 :> done @@ Task2 :> running @@ Task3 :> canceled)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
6: <s1!Acquire line 19, col 1 to line 19, col 20 of module step2>
/\ waiters = <<Task3, Task2>>
/\ lockState = unlocked
/\ taskStates = (Task1 :> done @@ Task2 :> waiting @@ Task3 :> canceled)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2218:4 @!@!@
7: Stuttering
@!@!@ENDMSG 2218 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2021-05-12 12:57:00
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2021-05-12 12:57:00
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<s1!Init line 19, col 1 to line 19, col 2 of module step2>: 2:2
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 22, col 3 to line 24, col 19 of module step1: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<s1!Acquire line 19, col 1 to line 19, col 2 of module step2>: 39:59
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 29, col 22 to line 29, col 44 of module step1: 1275
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 29, col 22 to line 29, col 34 of module step1: 1098
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 29, col 39 to line 29, col 44 of module step1: 1098
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 29, col 15 to line 29, col 19 of module step1: 393
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 30, col 6 to line 30, col 31 of module step1: 371
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 30, col 6 to line 30, col 21 of module step1: 312
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 30, col 25 to line 30, col 31 of module step1: 312
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 31, col 9 to line 31, col 46 of module step1: 59
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 31, col 9 to line 31, col 22 of module step1: 59
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 31, col 27 to line 31, col 46 of module step1: 39
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 32, col 10 to line 32, col 61 of module step1: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 33, col 10 to line 33, col 28 of module step1: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 34, col 10 to line 34, col 26 of module step1: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 36, col 10 to line 36, col 60 of module step1: 46
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 37, col 10 to line 37, col 41 of module step1: 46
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 38, col 10 to line 38, col 28 of module step1: 46
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Cancel line 23, col 1 to line 23, col 12 of module step2>: 32:49
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 25, col 6 to line 25, col 31 of module step2: 443
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 25, col 6 to line 25, col 21 of module step2: 394
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 25, col 25 to line 25, col 31 of module step2: 394
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 26, col 6 to line 26, col 57 of module step2: 49
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 27, col 6 to line 27, col 37 of module step2: 49
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<TypeInvariant line 44, col 1 to line 44, col 13 of module step2>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 44, col 18 to line 44, col 33 of module step2: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 96, col 3 to line 98, col 37 of module step1: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 96, col 6 to line 97, col 76 of module step1: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 97, col 7 to line 97, col 76 of module step1: 348
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 96, col 15 to line 96, col 19 of module step1: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 98, col 6 to line 98, col 37 of module step1: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<NotMoreThanOneAcquired line 45, col 1 to line 45, col 22 of module step2>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 45, col 27 to line 45, col 51 of module step2: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 3092
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 1161
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 1441
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 9278
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 16999
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 2150
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 3098
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 2123
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 558
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 1365
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 1737
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 19, col 1 to line 19, col 20 of module step2: 2644
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 102, col 3 to line 103, col 59 of module step1: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 102, col 20 to line 103, col 59 of module step1: 348
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 103, col 5 to line 103, col 59 of module step1: 696
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 103, col 5 to line 103, col 29 of module step1: 696
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||||line 103, col 34 to line 103, col 59 of module step1: 120
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |||line 102, col 30 to line 102, col 41 of module step1: 348
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  ||line 102, col 13 to line 102, col 17 of module step1: 116
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(7) at 2021-05-12 12:57:00: 208 states generated (10,823 s/min), 116 distinct states found (6,036 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
208 states generated, 116 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 7.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1163ms at (2021-05-12 12:57:00)
@!@!@ENDMSG 2186 @!@!@