Skip to content

Instantly share code, notes, and snippets.

@japgolly

japgolly/as.log Secret

Created December 14, 2020 23:15
Show Gist options
  • Save japgolly/19ee59f884bc13cefa9401b1f57c49cc to your computer and use it in GitHub Desktop.
Save japgolly/19ee59f884bc13cefa9401b1f57c49cc to your computer and use it in GitHub Desktop.
Download ZIP
TLA+ trace example
Raw
as.log
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2020-12-14 22:38:46.
Progress(22) at 2020-12-14 22:38:49: 213,160 states generated (213,160 s/min), 99,208 distinct states found (99,208 ds/min), 51,365 states left on queue.
Progress(27) at 2020-12-14 22:39:49: 11,009,928 states generated (10,796,768 s/min), 4,280,792 distinct states found (4,181,584 ds/min), 1,881,953 states left on queue.
Progress(29) at 2020-12-14 22:40:49: 21,888,016 states generated (10,878,088 s/min), 8,328,728 distinct states found (4,047,936 ds/min), 3,585,584 states left on queue.
Progress(29) at 2020-12-14 22:41:49: 32,750,079 states generated (10,862,063 s/min), 12,261,135 distinct states found (3,932,407 ds/min), 5,163,965 states left on queue.
Progress(30) at 2020-12-14 22:42:49: 43,598,635 states generated (10,848,556 s/min), 16,135,153 distinct states found (3,874,018 ds/min), 6,697,840 states left on queue.
Progress(30) at 2020-12-14 22:43:49: 54,558,881 states generated (10,960,246 s/min), 19,987,081 distinct states found (3,851,928 ds/min), 8,151,782 states left on queue.
Progress(31) at 2020-12-14 22:44:49: 65,304,590 states generated (10,745,709 s/min), 23,766,553 distinct states found (3,779,472 ds/min), 9,619,573 states left on queue.
Progress(31) at 2020-12-14 22:45:49: 76,186,218 states generated (10,881,628 s/min), 27,566,838 distinct states found (3,800,285 ds/min), 11,050,013 states left on queue.
Progress(31) at 2020-12-14 22:46:49: 87,051,255 states generated (10,865,037 s/min), 31,351,168 distinct states found (3,784,330 ds/min), 12,415,439 states left on queue.
Progress(31) at 2020-12-14 22:47:49: 97,724,474 states generated (10,673,219 s/min), 34,931,451 distinct states found (3,580,283 ds/min), 13,705,096 states left on queue.
Progress(32) at 2020-12-14 22:48:49: 108,679,169 states generated (10,954,695 s/min), 38,871,362 distinct states found (3,939,911 ds/min), 15,261,895 states left on queue.
Progress(32) at 2020-12-14 22:49:49: 119,494,268 states generated (10,815,099 s/min), 42,644,083 distinct states found (3,772,721 ds/min), 16,739,237 states left on queue.
Progress(32) at 2020-12-14 22:50:49: 130,695,518 states generated (11,201,250 s/min), 46,453,713 distinct states found (3,809,630 ds/min), 18,111,874 states left on queue.
Progress(32) at 2020-12-14 22:51:49: 141,400,710 states generated (10,705,192 s/min), 50,154,674 distinct states found (3,700,961 ds/min), 19,390,667 states left on queue.
Progress(32) at 2020-12-14 22:52:49: 152,355,500 states generated (10,954,790 s/min), 53,912,226 distinct states found (3,757,552 ds/min), 20,784,583 states left on queue.
Progress(32) at 2020-12-14 22:53:49: 163,220,218 states generated (10,864,718 s/min), 57,520,382 distinct states found (3,608,156 ds/min), 21,972,771 states left on queue.
Progress(33) at 2020-12-14 22:54:49: 174,406,295 states generated (11,186,077 s/min), 61,408,313 distinct states found (3,887,931 ds/min), 23,381,134 states left on queue.
Progress(33) at 2020-12-14 22:55:49: 185,226,842 states generated (10,820,547 s/min), 65,219,500 distinct states found (3,811,187 ds/min), 24,860,761 states left on queue.
Progress(33) at 2020-12-14 22:56:49: 195,974,297 states generated (10,747,455 s/min), 68,898,176 distinct states found (3,678,676 ds/min), 26,329,491 states left on queue.
Progress(33) at 2020-12-14 22:57:49: 206,955,412 states generated (10,981,115 s/min), 72,604,632 distinct states found (3,706,456 ds/min), 27,629,603 states left on queue.
Progress(33) at 2020-12-14 22:58:49: 218,089,896 states generated (11,134,484 s/min), 76,432,621 distinct states found (3,827,989 ds/min), 28,969,519 states left on queue.
Progress(33) at 2020-12-14 22:59:49: 228,808,326 states generated (10,718,430 s/min), 80,099,717 distinct states found (3,667,096 ds/min), 30,234,710 states left on queue.
Progress(33) at 2020-12-14 23:00:49: 239,785,580 states generated (10,977,254 s/min), 83,847,589 distinct states found (3,747,872 ds/min), 31,607,816 states left on queue.
Progress(33) at 2020-12-14 23:01:49: 250,468,274 states generated (10,682,694 s/min), 87,293,897 distinct states found (3,446,308 ds/min), 32,652,719 states left on queue.
Progress(33) at 2020-12-14 23:02:49: 261,560,592 states generated (11,092,318 s/min), 90,997,621 distinct states found (3,703,724 ds/min), 33,920,014 states left on queue.
Progress(34) at 2020-12-14 23:03:49: 272,546,526 states generated (10,985,934 s/min), 94,780,548 distinct states found (3,782,927 ds/min), 35,236,971 states left on queue.
Progress(34) at 2020-12-14 23:04:49: 283,510,811 states generated (10,964,285 s/min), 98,601,604 distinct states found (3,821,056 ds/min), 36,584,323 states left on queue.
Progress(34) at 2020-12-14 23:05:49: 294,122,285 states generated (10,611,474 s/min), 102,165,646 distinct states found (3,564,042 ds/min), 37,962,365 states left on queue.
Progress(34) at 2020-12-14 23:06:49: 304,531,016 states generated (10,408,731 s/min), 105,792,964 distinct states found (3,627,318 ds/min), 39,296,771 states left on queue.
Progress(34) at 2020-12-14 23:07:49: 315,317,899 states generated (10,786,883 s/min), 109,285,925 distinct states found (3,492,961 ds/min), 40,549,372 states left on queue.
Checkpointing of run states/20-12-14-22-38-45
Checkpointing completed at (2020-12-14 23:08:49)
Progress(34) at 2020-12-14 23:08:49: 326,339,425 states generated (11,021,526 s/min), 112,912,035 distinct states found (3,626,110 ds/min), 41,661,933 states left on queue.
Progress(34) at 2020-12-14 23:09:49: 337,262,116 states generated (10,922,691 s/min), 116,569,718 distinct states found (3,657,683 ds/min), 42,977,953 states left on queue.
Progress(34) at 2020-12-14 23:10:49: 348,669,868 states generated (11,407,752 s/min), 120,435,215 distinct states found (3,865,497 ds/min), 44,278,778 states left on queue.
Progress(34) at 2020-12-14 23:11:49: 359,688,806 states generated (11,018,938 s/min), 124,280,220 distinct states found (3,845,005 ds/min), 45,645,038 states left on queue.
Progress(34) at 2020-12-14 23:12:49: 370,116,520 states generated (10,427,714 s/min), 127,853,639 distinct states found (3,573,419 ds/min), 46,983,080 states left on queue.
Progress(34) at 2020-12-14 23:13:49: 381,035,409 states generated (10,918,889 s/min), 131,517,181 distinct states found (3,663,542 ds/min), 48,177,995 states left on queue.
Progress(34) at 2020-12-14 23:14:49: 391,923,111 states generated (10,887,702 s/min), 135,023,976 distinct states found (3,506,795 ds/min), 49,277,158 states left on queue.
Progress(34) at 2020-12-14 23:15:49: 402,358,641 states generated (10,435,530 s/min), 138,445,468 distinct states found (3,421,492 ds/min), 50,386,261 states left on queue.
Progress(34) at 2020-12-14 23:16:49: 413,688,830 states generated (11,330,189 s/min), 142,244,569 distinct states found (3,799,101 ds/min), 51,694,603 states left on queue.
Progress(34) at 2020-12-14 23:17:49: 424,417,746 states generated (10,728,916 s/min), 145,866,729 distinct states found (3,622,160 ds/min), 52,876,062 states left on queue.
Progress(35) at 2020-12-14 23:18:49: 435,378,868 states generated (10,961,122 s/min), 149,630,120 distinct states found (3,763,391 ds/min), 54,091,782 states left on queue.
Progress(35) at 2020-12-14 23:19:49: 446,455,418 states generated (11,076,550 s/min), 153,315,985 distinct states found (3,685,865 ds/min), 55,267,474 states left on queue.
Progress(35) at 2020-12-14 23:20:49: 456,349,591 states generated (9,894,173 s/min), 156,820,058 distinct states found (3,504,073 ds/min), 56,751,357 states left on queue.
Progress(35) at 2020-12-14 23:21:49: 467,153,108 states generated (10,803,517 s/min), 160,333,059 distinct states found (3,513,001 ds/min), 57,903,324 states left on queue.
Progress(35) at 2020-12-14 23:22:49: 477,878,675 states generated (10,725,567 s/min), 164,125,326 distinct states found (3,792,267 ds/min), 59,401,090 states left on queue.
Progress(35) at 2020-12-14 23:23:49: 488,159,372 states generated (10,280,697 s/min), 167,475,857 distinct states found (3,350,531 ds/min), 60,551,409 states left on queue.
"Error: Drafts are not eventually-consistent"
[ AB |-> {},
AW |-> {w1},
AT |-> {t1, t2},
Stores |->
{ {},
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] } } ]
Error: Invariant StableInvariants is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ target = [drafts |-> {}, pending |-> {}, returning |-> {}]
/\ workers = (w1 :> [status |-> "-"] @@ w2 :> [status |-> "-"])
/\ tabs = (t1 :> [status |-> "-"] @@ t2 :> [status |-> "-"])
/\ remote = [drafts |-> {}, ord |-> 0]
/\ browsers = (b1 :> << >> @@ b2 :> << >>)
/\ network = <<>>
State 2: <TabNew line 879, col 5 to line 897, col 10 of module drafts>
/\ workers = ( w1 :>
[ drafts |-> {},
time |-> 1,
status |-> "live",
sync |->
[Remote |-> [tombstones |-> {}, sync |-> FALSE, syncing |-> FALSE]],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ tabs = ( t1 :>
[ drafts |-> {},
worker |-> w1,
status |-> "loading",
awaiting |-> {"Remote"} ] @@
t2 :> [status |-> "-"] )
State 3: <TabLoad line 855, col 5 to line 875, col 74 of module drafts>
/\ tabs = ( t1 :> [drafts |-> {}, worker |-> w1, status |-> "loading", awaiting |-> {}] @@
t2 :> [status |-> "-"] )
State 4: <TabNew line 879, col 5 to line 897, col 10 of module drafts>
/\ tabs = ( t1 :> [drafts |-> {}, worker |-> w1, status |-> "loading", awaiting |-> {}] @@
t2 :>
[ drafts |-> {},
worker |-> w1,
status |-> "loading",
awaiting |-> {"Remote"} ] )
State 5: <TabLoad line 855, col 5 to line 875, col 74 of module drafts>
/\ tabs = ( t1 :> [drafts |-> {}, worker |-> w1, status |-> "loading", awaiting |-> {}] @@
t2 :> [drafts |-> {}, worker |-> w1, status |-> "loading", awaiting |-> {}] )
State 6: <TabStart line 909, col 7 to line 922, col 58 of module drafts>
/\ tabs = ( t1 :>
[worker |-> w1, editCount |-> 0, status |-> "clean", tombstones |-> {}] @@
t2 :> [drafts |-> {}, worker |-> w1, status |-> "loading", awaiting |-> {}] )
State 7: <TabStart line 909, col 7 to line 922, col 58 of module drafts>
/\ tabs = ( t1 :>
[worker |-> w1, editCount |-> 0, status |-> "clean", tombstones |-> {}] @@
t2 :>
[worker |-> w1, editCount |-> 0, status |-> "clean", tombstones |-> {}] )
State 8: <UserEditClean line 1041, col 7 to line 1045, col 59 of module drafts>
/\ target = [ drafts |-> {},
pending |-> {[tombstone |-> FALSE, editCount |-> 1, tab |-> t1]},
returning |-> {} ]
/\ tabs = ( t1 :>
[ drafts |-> {},
worker |-> w1,
editCount |-> 1,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> TRUE,
editSent |-> FALSE,
aborted |-> FALSE ] @@
t2 :>
[worker |-> w1, editCount |-> 0, status |-> "clean", tombstones |-> {}] )
State 9: <UserAbort line 994, col 7 to line 1031, col 63 of module drafts>
/\ target = [ drafts |-> {},
pending |-> {[tombstone |-> TRUE, editCount |-> 1, tab |-> t1]},
returning |-> {} ]
/\ tabs = ( t1 :>
[ drafts |-> {},
worker |-> w1,
editCount |-> 2,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> TRUE,
editSent |-> FALSE,
aborted |-> TRUE ] @@
t2 :>
[worker |-> w1, editCount |-> 0, status |-> "clean", tombstones |-> {}] )
State 10: <TabSendChangesToWorker line 957, col 7 to line 971, col 58 of module drafts>
/\ tabs = ( t1 :>
[ drafts |-> {},
worker |-> w1,
editCount |-> 2,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> TRUE,
aborted |-> TRUE ] @@
t2 :>
[worker |-> w1, editCount |-> 0, status |-> "clean", tombstones |-> {}] )
/\ network = << [ drafts |-> {},
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |->
[ isEmpty |-> FALSE,
get |-> [prov |-> (w1 :> 0 @@ w2 :> 0), editCount |-> 2] ] ] >>
State 11: <WorkerRecvChanges line 1074, col 5 to line 1102, col 88 of module drafts>
/\ target = [ drafts |-> {},
pending |-> {},
returning |->
{ [ editCount |-> 2,
draft |->
[ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ],
tab |-> t1 ] } ]
/\ workers = ( w1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
time |-> 2,
status |-> "live",
sync |->
[Remote |-> [tombstones |-> {}, sync |-> TRUE, syncing |-> FALSE]],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:W->T",
from |-> w1,
to |-> t2,
edit |-> [isEmpty |-> TRUE] ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:W->T",
from |-> w1,
to |-> t1,
edit |->
[ isEmpty |-> FALSE,
get |->
[ editCount |-> 2,
draft |->
[ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] ] ] ] >>
State 12: <TabRecvDraftsFromWorker line 831, col 5 to line 851, col 52 of module drafts>
/\ tabs = ( t1 :>
[ drafts |-> {},
worker |-> w1,
editCount |-> 2,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> TRUE,
aborted |-> TRUE ] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:W->T",
from |-> w1,
to |-> t1,
edit |->
[ isEmpty |-> FALSE,
get |->
[ editCount |-> 2,
draft |->
[ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] ] ] ] >>
State 13: <TabRecvDraftsFromWorker line 831, col 5 to line 851, col 52 of module drafts>
/\ target = [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
pending |-> {},
returning |-> {} ]
/\ tabs = ( t1 :>
[ worker |-> w1,
editCount |-> 2,
status |-> "clean",
tombstones |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] } ] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ network = <<>>
State 14: <TabSendTombstonesToWorker line 977, col 7 to line 987, col 58 of module drafts>
/\ tabs = ( t1 :>
[worker |-> w1, editCount |-> 2, status |-> "clean", tombstones |-> {}] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ] >>
State 15: <WorkerSendRemoteStoreCmd line 1147, col 7 to line 1157, col 55 of module drafts>
/\ workers = ( w1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
time |-> 2,
status |-> "live",
sync |->
[Remote |-> [tombstones |-> {}, sync |-> FALSE, syncing |-> TRUE]],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "rcmd:T->R",
from |-> w1,
to |-> t2 ] >>
State 16: <TabRecvRemoteStoreCmd line 929, col 5 to line 951, col 66 of module drafts>
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:T->R",
from |-> t2,
to |-> "Remote" ] >>
State 17: <RemoteRecvDrafts line 783, col 5 to line 804, col 58 of module drafts>
/\ remote = [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
ord |-> 0 ]
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ],
[type |-> "ack:R->T", from |-> "Remote", to |-> t2],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ] >>
State 18: <WorkerRecvChanges line 1074, col 5 to line 1102, col 88 of module drafts>
/\ workers = ( w1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
time |-> 2,
status |-> "live",
sync |->
[Remote |-> [tombstones |-> {}, sync |-> TRUE, syncing |-> TRUE]],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ network = << [type |-> "ack:R->T", from |-> "Remote", to |-> t2],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:W->T",
from |-> w1,
to |-> t2,
edit |-> [isEmpty |-> TRUE] ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:W->T",
from |-> w1,
to |-> t1,
edit |-> [isEmpty |-> TRUE] ] >>
State 19: <TabRecvDraftsFromWorker line 831, col 5 to line 851, col 52 of module drafts>
/\ tabs = ( t1 :>
[worker |-> w1, editCount |-> 2, status |-> "clean", tombstones |-> {}] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ network = << [type |-> "ack:R->T", from |-> "Remote", to |-> t2],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:W->T",
from |-> w1,
to |-> t1,
edit |-> [isEmpty |-> TRUE] ] >>
State 20: <TabRecvDraftsFromWorker line 831, col 5 to line 851, col 52 of module drafts>
/\ tabs = ( t1 :>
[ worker |-> w1,
editCount |-> 2,
status |-> "clean",
tombstones |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] } ] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ network = << [type |-> "ack:R->T", from |-> "Remote", to |-> t2],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ] >>
State 21: <TabRecvRemoteAck line 1162, col 5 to line 1173, col 66 of module drafts>
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[type |-> "ack:T->W", from |-> t2, to |-> w1, rejected |-> FALSE] >>
State 22: <TabSendTombstonesToWorker line 977, col 7 to line 987, col 58 of module drafts>
/\ tabs = ( t1 :>
[worker |-> w1, editCount |-> 2, status |-> "clean", tombstones |-> {}] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[type |-> "ack:T->W", from |-> t2, to |-> w1, rejected |-> FALSE],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ] >>
State 23: <WorkerRecvChanges line 1074, col 5 to line 1102, col 88 of module drafts>
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[type |-> "ack:T->W", from |-> t2, to |-> w1, rejected |-> FALSE] >>
State 24: <WorkerRecvRemoteAck line 1178, col 5 to line 1191, col 57 of module drafts>
/\ workers = ( w1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
time |-> 2,
status |-> "live",
sync |->
[Remote |-> [tombstones |-> {}, sync |-> TRUE, syncing |-> FALSE]],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ] >>
State 25: <WorkerSendRemoteStoreCmd line 1147, col 7 to line 1157, col 55 of module drafts>
/\ workers = ( w1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
time |-> 2,
status |-> "live",
sync |->
[ Remote |->
[ tombstones |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
sync |-> FALSE,
syncing |-> TRUE ] ],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "rcmd:T->R",
from |-> w1,
to |-> t1 ] >>
State 26: <TabRecvRemoteStoreCmd line 929, col 5 to line 951, col 66 of module drafts>
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->R",
from |-> t1,
to |-> "Remote" ] >>
State 27: <RemoteRecvDrafts line 783, col 5 to line 804, col 58 of module drafts>
/\ remote = [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
ord |-> 0 ]
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t1 ],
[type |-> "ack:R->T", from |-> "Remote", to |-> t1],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t2 ] >>
State 28: <TabRecvDraftsFromRemote line 809, col 5 to line 826, col 60 of module drafts>
/\ tabs = ( t1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
worker |-> w1,
editCount |-> 2,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ network = << [type |-> "ack:R->T", from |-> "Remote", to |-> t1],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:R->T",
from |-> "Remote",
to |-> t2 ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ] >>
State 29: <TabRecvDraftsFromRemote line 809, col 5 to line 826, col 60 of module drafts>
/\ network = << [type |-> "ack:R->T", from |-> "Remote", to |-> t1],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t2,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ] >>
State 30: <TabRecvRemoteAck line 1162, col 5 to line 1173, col 66 of module drafts>
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
type |-> "sync:T->W",
from |-> t1,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ],
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t2,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ],
[type |-> "ack:T->W", from |-> t1, to |-> w1, rejected |-> FALSE] >>
State 31: <WorkerRecvChanges line 1074, col 5 to line 1102, col 88 of module drafts>
/\ workers = ( w1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
time |-> 2,
status |-> "live",
sync |->
[ Remote |->
[ tombstones |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
sync |-> TRUE,
syncing |-> TRUE ] ],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ network = << [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
type |-> "sync:T->W",
from |-> t2,
to |-> w1,
edit |-> [isEmpty |-> TRUE] ],
[type |-> "ack:T->W", from |-> t1, to |-> w1, rejected |-> FALSE] >>
State 32: <WorkerRecvChanges line 1074, col 5 to line 1102, col 88 of module drafts>
/\ network = <<[type |-> "ack:T->W", from |-> t1, to |-> w1, rejected |-> FALSE]>>
State 33: <WorkerRecvRemoteAck line 1178, col 5 to line 1191, col 57 of module drafts>
/\ workers = ( w1 :>
[ drafts |-> {},
time |-> 2,
status |-> "live",
sync |->
[Remote |-> [tombstones |-> {}, sync |-> TRUE, syncing |-> FALSE]],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ network = <<>>
State 34: <WorkerSendRemoteStoreCmd line 1147, col 7 to line 1157, col 55 of module drafts>
/\ target = [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
pending |-> {},
returning |-> {} ]
/\ workers = ( w1 :>
[ drafts |-> {},
time |-> 2,
status |-> "live",
sync |->
[Remote |-> [tombstones |-> {}, sync |-> FALSE, syncing |-> FALSE]],
browser |-> b1 ] @@
w2 :> [status |-> "-"] )
/\ tabs = ( t1 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> FALSE ] },
worker |-> w1,
editCount |-> 2,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] @@
t2 :>
[ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
worker |-> w1,
editCount |-> 0,
status |-> "dirty",
editDraft |-> [isEmpty |-> TRUE],
editUnsent |-> FALSE,
editSent |-> FALSE,
aborted |-> FALSE ] )
/\ remote = [ drafts |->
{ [ worker |-> w1,
time |-> 1,
prov |-> (w1 :> 0 @@ w2 :> 0),
tombstone |-> TRUE ] },
ord |-> 0 ]
/\ browsers = (b1 :> << >> @@ b2 :> << >>)
/\ network = <<>>
491225770 states generated, 168321093 distinct states found, 60801274 states left on queue.
The depth of the complete state graph search is 35.
Finished in 45min 21s at (2020-12-14 23:24:06)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment