diff --git a/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t2_l2.cfg-2024-11-06--13-44-17.log b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t2_l2.cfg-2024-11-06--13-44-17.log new file mode 100644 index 0000000000..768722b1eb --- /dev/null +++ b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t2_l2.cfg-2024-11-06--13-44-17.log @@ -0,0 +1,63 @@ +git revision: 864f4667d +Platform: Linux neon-dev-arm64-1 6.8.0-48-generic #48-Ubuntu SMP PREEMPT_DYNAMIC Fri Sep 27 14:35:45 UTC 2024 aarch64 aarch64 aarch64 GNU/Linux +CPU Info Linux: Neoverse-N1 +CPU Cores Linux: 80 +CPU Info Mac: +CPU Cores Mac: +Spec: MCProposerAcceptorStatic.tla +Config: models/MCProposerAcceptorStatic_p2_a3_t2_l2.cfg +---- +\* A very small model just to play. +CONSTANTS +NULL = NULL +proposers = {p1, p2} +acceptors = {a1, a2, a3} +max_term = 2 +max_entries = 2 +SPECIFICATION Spec +CONSTRAINT StateConstraint +INVARIANT +TypeOk +ElectionSafety +LogIsMonotonic +LogSafety +CommittedNotTruncated +SYMMETRY ProposerAcceptorSymmetry +CHECK_DEADLOCK FALSE +ALIAS Alias + + +---- + +TLC2 Version 2.20 of Day Month 20?? (rev: f68cb71) +Running breadth-first search Model-Checking with fp 110 and seed 3949669318051689745 with 80 workers on 80 cores with 54613MB heap and 61440MB offheap memory [pid: 46037] (Linux 6.8.0-48-generic aarch64, Ubuntu 21.0.4 x86_64, OffHeapDiskFPSet, DiskStateQueue). +Parsing file /home/arseny/neon/safekeeper/spec/MCProposerAcceptorStatic.tla +Parsing file /tmp/tlc-11123278435718411444/TLC.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) +Parsing file /home/arseny/neon/safekeeper/spec/ProposerAcceptorStatic.tla +Parsing file /tmp/tlc-11123278435718411444/_TLCTrace.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla) +Parsing file /tmp/tlc-11123278435718411444/Integers.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) +Parsing file /tmp/tlc-11123278435718411444/Sequences.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) +Parsing file /tmp/tlc-11123278435718411444/FiniteSets.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) +Parsing file /tmp/tlc-11123278435718411444/Naturals.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) +Parsing file /tmp/tlc-11123278435718411444/TLCExt.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 Integers +Semantic processing of module ProposerAcceptorStatic +Semantic processing of module TLCExt +Semantic processing of module _TLCTrace +Semantic processing of module MCProposerAcceptorStatic +Starting... (2024-11-06 13:44:18) +Computing initial states... +Finished computing initial states: 1 distinct state generated at 2024-11-06 13:44:20. +Model checking completed. No error has been found. + Estimates of the probability that TLC did not check all reachable states + because two distinct states had the same fingerprint: + calculated (optimistic): val = 2.9E-9 + based on the actual fingerprints: val = 4.1E-10 +922134 states generated, 61249 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 31. +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 6 and the 95th percentile is 3). +Finished in 11s at (2024-11-06 13:44:28) diff --git a/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t3_l3.cfg-2024-11-06--13-03-51.log b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t3_l3.cfg-2024-11-06--13-03-51.log new file mode 100644 index 0000000000..46f21cee72 --- /dev/null +++ b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t3_l3.cfg-2024-11-06--13-03-51.log @@ -0,0 +1,72 @@ +git revision: 864f4667d +Platform: Linux neon-dev-arm64-1 6.8.0-48-generic #48-Ubuntu SMP PREEMPT_DYNAMIC Fri Sep 27 14:35:45 UTC 2024 aarch64 aarch64 aarch64 GNU/Linux +CPU Info Linux: Neoverse-N1 +CPU Cores Linux: 80 +CPU Info Mac: +CPU Cores Mac: +Spec: MCProposerAcceptorStatic.tla +Config: models/MCProposerAcceptorStatic_p2_a3_t3_l3.cfg +---- +CONSTANTS +NULL = NULL +proposers = {p1, p2} +acceptors = {a1, a2, a3} +max_term = 3 +max_entries = 3 +SPECIFICATION Spec +CONSTRAINT StateConstraint +INVARIANT +TypeOk +ElectionSafety +LogIsMonotonic +LogSafety +CommittedNotTruncated +SYMMETRY ProposerAcceptorSymmetry +CHECK_DEADLOCK FALSE +ALIAS Alias + +---- + +TLC2 Version 2.20 of Day Month 20?? (rev: f68cb71) +Running breadth-first search Model-Checking with fp 126 and seed 2302892334567572769 with 80 workers on 80 cores with 54613MB heap and 61440MB offheap memory [pid: 39701] (Linux 6.8.0-48-generic aarch64, Ubuntu 21.0.4 x86_64, OffHeapDiskFPSet, DiskStateQueue). +Parsing file /home/arseny/neon/safekeeper/spec/MCProposerAcceptorStatic.tla +Parsing file /tmp/tlc-15178810317173795942/TLC.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) +Parsing file /home/arseny/neon/safekeeper/spec/ProposerAcceptorStatic.tla +Parsing file /tmp/tlc-15178810317173795942/_TLCTrace.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla) +Parsing file /tmp/tlc-15178810317173795942/Integers.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) +Parsing file /tmp/tlc-15178810317173795942/Sequences.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) +Parsing file /tmp/tlc-15178810317173795942/FiniteSets.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) +Parsing file /tmp/tlc-15178810317173795942/Naturals.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) +Parsing file /tmp/tlc-15178810317173795942/TLCExt.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 Integers +Semantic processing of module ProposerAcceptorStatic +Semantic processing of module TLCExt +Semantic processing of module _TLCTrace +Semantic processing of module MCProposerAcceptorStatic +Starting... (2024-11-06 13:03:52) +Computing initial states... +Finished computing initial states: 1 distinct state generated at 2024-11-06 13:03:55. +Progress(21) at 2024-11-06 13:03:58: 846,240 states generated (846,240 s/min), 106,298 distinct states found (106,298 ds/min), 41,028 states left on queue. +Progress(28) at 2024-11-06 13:04:58: 27,538,211 states generated (26,691,971 s/min), 2,768,793 distinct states found (2,662,495 ds/min), 782,984 states left on queue. +Progress(30) at 2024-11-06 13:05:58: 54,048,763 states generated (26,510,552 s/min), 5,076,745 distinct states found (2,307,952 ds/min), 1,241,301 states left on queue. +Progress(31) at 2024-11-06 13:06:58: 80,554,724 states generated (26,505,961 s/min), 7,199,201 distinct states found (2,122,456 ds/min), 1,541,574 states left on queue. +Progress(32) at 2024-11-06 13:07:58: 106,991,261 states generated (26,436,537 s/min), 9,121,549 distinct states found (1,922,348 ds/min), 1,686,289 states left on queue. +Progress(33) at 2024-11-06 13:08:58: 133,354,665 states generated (26,363,404 s/min), 10,935,451 distinct states found (1,813,902 ds/min), 1,739,977 states left on queue. +Progress(34) at 2024-11-06 13:09:58: 159,631,385 states generated (26,276,720 s/min), 12,605,372 distinct states found (1,669,921 ds/min), 1,677,447 states left on queue. +Progress(35) at 2024-11-06 13:10:58: 185,862,196 states generated (26,230,811 s/min), 14,138,409 distinct states found (1,533,037 ds/min), 1,501,760 states left on queue. +Progress(36) at 2024-11-06 13:11:58: 212,021,688 states generated (26,159,492 s/min), 15,538,990 distinct states found (1,400,581 ds/min), 1,216,621 states left on queue. +Progress(37) at 2024-11-06 13:12:58: 238,046,160 states generated (26,024,472 s/min), 16,778,583 distinct states found (1,239,593 ds/min), 797,230 states left on queue. +Progress(39) at 2024-11-06 13:13:58: 263,931,163 states generated (25,885,003 s/min), 17,820,786 distinct states found (1,042,203 ds/min), 209,400 states left on queue. +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.5E-4 + based on the actual fingerprints: val = 7.9E-5 +270257170 states generated, 18005639 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 47. +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 7 and the 95th percentile is 3). +Finished in 10min 25s at (2024-11-06 13:14:17) diff --git a/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t4_l4.cfg-2024-11-06--14-20-25.log b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t4_l4.cfg-2024-11-06--14-20-25.log new file mode 100644 index 0000000000..c7cc853af0 --- /dev/null +++ b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a3_t4_l4.cfg-2024-11-06--14-20-25.log @@ -0,0 +1,1466 @@ +# Shows LogSafety violation when "don't commit separately entries from previous terms" check is disabled. +git revision: 4f1ee6331 +Platform: Linux neon-dev-arm64-1 6.8.0-48-generic #48-Ubuntu SMP PREEMPT_DYNAMIC Fri Sep 27 14:35:45 UTC 2024 aarch64 aarch64 aarch64 GNU/Linux +CPU Info Linux: Neoverse-N1 +CPU Cores Linux: 80 +CPU Info Mac: +CPU Cores Mac: +Spec: MCProposerAcceptorStatic.tla +Config: models/MCProposerAcceptorStatic_p2_a3_t4_l4.cfg +---- +CONSTANTS +NULL = NULL +proposers = {p1, p2} +acceptors = {a1, a2, a3} +max_term = 4 +max_entries = 4 +SPECIFICATION Spec +CONSTRAINT StateConstraint +INVARIANT +TypeOk +ElectionSafety +LogIsMonotonic +LogSafety +SYMMETRY ProposerAcceptorSymmetry +CHECK_DEADLOCK FALSE +ALIAS Alias + +---- + +TLC2 Version 2.20 of Day Month 20?? (rev: f68cb71) +Running breadth-first search Model-Checking with fp 12 and seed -5379034126224420237 with 80 workers on 80 cores with 54613MB heap and 61440MB offheap memory [pid: 52295] (Linux 6.8.0-48-generic aarch64, Ubuntu 21.0.4 x86_64, OffHeapDiskFPSet, DiskStateQueue). +Parsing file /home/arseny/neon/safekeeper/spec/MCProposerAcceptorStatic.tla +Parsing file /tmp/tlc-4533438058229992850/TLC.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) +Parsing file /home/arseny/neon/safekeeper/spec/ProposerAcceptorStatic.tla +Parsing file /tmp/tlc-4533438058229992850/_TLCTrace.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla) +Parsing file /tmp/tlc-4533438058229992850/Integers.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) +Parsing file /tmp/tlc-4533438058229992850/Sequences.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) +Parsing file /tmp/tlc-4533438058229992850/FiniteSets.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) +Parsing file /tmp/tlc-4533438058229992850/Naturals.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) +Parsing file /tmp/tlc-4533438058229992850/TLCExt.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 Integers +Semantic processing of module ProposerAcceptorStatic +Semantic processing of module TLCExt +Semantic processing of module _TLCTrace +Semantic processing of module MCProposerAcceptorStatic +Starting... (2024-11-06 14:20:26) +Computing initial states... +Finished computing initial states: 1 distinct state generated at 2024-11-06 14:20:29. +Progress(20) at 2024-11-06 14:20:32: 1,011,898 states generated (1,011,898 s/min), 140,947 distinct states found (140,947 ds/min), 60,535 states left on queue. +Progress(26) at 2024-11-06 14:21:32: 30,146,518 states generated (29,134,620 s/min), 3,742,736 distinct states found (3,601,789 ds/min), 1,438,779 states left on queue. +Progress(27) at 2024-11-06 14:22:32: 59,362,708 states generated (29,216,190 s/min), 7,210,233 distinct states found (3,467,497 ds/min), 2,708,295 states left on queue. +Progress(28) at 2024-11-06 14:23:32: 88,589,291 states generated (29,226,583 s/min), 10,552,781 distinct states found (3,342,548 ds/min), 3,874,296 states left on queue. +Progress(29) at 2024-11-06 14:24:32: 117,894,209 states generated (29,304,918 s/min), 13,932,498 distinct states found (3,379,717 ds/min), 5,069,960 states left on queue. +Progress(29) at 2024-11-06 14:25:32: 147,338,882 states generated (29,444,673 s/min), 17,180,069 distinct states found (3,247,571 ds/min), 6,146,371 states left on queue. +Progress(29) at 2024-11-06 14:26:32: 176,498,135 states generated (29,159,253 s/min), 20,547,926 distinct states found (3,367,857 ds/min), 7,338,835 states left on queue. +Progress(30) at 2024-11-06 14:27:32: 205,957,044 states generated (29,458,909 s/min), 23,661,090 distinct states found (3,113,164 ds/min), 8,293,570 states left on queue. +Progress(30) at 2024-11-06 14:28:32: 235,390,133 states generated (29,433,089 s/min), 26,892,306 distinct states found (3,231,216 ds/min), 9,369,229 states left on queue. +Progress(30) at 2024-11-06 14:29:32: 264,571,938 states generated (29,181,805 s/min), 30,176,971 distinct states found (3,284,665 ds/min), 10,493,429 states left on queue. +Progress(31) at 2024-11-06 14:30:32: 293,928,191 states generated (29,356,253 s/min), 33,296,160 distinct states found (3,119,189 ds/min), 11,463,686 states left on queue. +Progress(31) at 2024-11-06 14:31:32: 323,436,668 states generated (29,508,477 s/min), 36,347,973 distinct states found (3,051,813 ds/min), 12,365,578 states left on queue. +Progress(31) at 2024-11-06 14:32:32: 352,943,790 states generated (29,507,122 s/min), 39,465,244 distinct states found (3,117,271 ds/min), 13,349,544 states left on queue. +Progress(31) at 2024-11-06 14:33:32: 382,292,863 states generated (29,349,073 s/min), 42,654,621 distinct states found (3,189,377 ds/min), 14,384,363 states left on queue. +Progress(31) at 2024-11-06 14:34:32: 411,385,854 states generated (29,092,991 s/min), 45,941,145 distinct states found (3,286,524 ds/min), 15,509,450 states left on queue. +Progress(31) at 2024-11-06 14:35:32: 440,738,756 states generated (29,352,902 s/min), 48,984,566 distinct states found (3,043,421 ds/min), 16,419,882 states left on queue. +Progress(32) at 2024-11-06 14:36:32: 470,251,558 states generated (29,512,802 s/min), 51,925,693 distinct states found (2,941,127 ds/min), 17,211,457 states left on queue. +Progress(32) at 2024-11-06 14:37:32: 499,714,013 states generated (29,462,455 s/min), 54,955,581 distinct states found (3,029,888 ds/min), 18,114,624 states left on queue. +Progress(32) at 2024-11-06 14:38:32: 529,254,608 states generated (29,540,595 s/min), 57,938,914 distinct states found (2,983,333 ds/min), 18,996,128 states left on queue. +Progress(32) at 2024-11-06 14:39:32: 558,774,398 states generated (29,519,790 s/min), 61,072,943 distinct states found (3,134,029 ds/min), 19,975,689 states left on queue. +Progress(32) at 2024-11-06 14:40:32: 588,134,665 states generated (29,360,267 s/min), 64,148,888 distinct states found (3,075,945 ds/min), 20,922,407 states left on queue. +Progress(32) at 2024-11-06 14:41:32: 617,464,374 states generated (29,329,709 s/min), 67,306,855 distinct states found (3,157,967 ds/min), 21,928,799 states left on queue. +Progress(32) at 2024-11-06 14:42:32: 646,525,281 states generated (29,060,907 s/min), 70,425,194 distinct states found (3,118,339 ds/min), 22,895,971 states left on queue. +Progress(32) at 2024-11-06 14:43:32: 676,054,893 states generated (29,529,612 s/min), 73,351,905 distinct states found (2,926,711 ds/min), 23,703,779 states left on queue. +Progress(33) at 2024-11-06 14:44:32: 705,581,782 states generated (29,526,889 s/min), 76,200,615 distinct states found (2,848,710 ds/min), 24,414,094 states left on queue. +Progress(33) at 2024-11-06 14:45:32: 735,069,836 states generated (29,488,054 s/min), 79,168,244 distinct states found (2,967,629 ds/min), 25,255,224 states left on queue. +Progress(33) at 2024-11-06 14:46:32: 764,659,188 states generated (29,589,352 s/min), 82,024,430 distinct states found (2,856,186 ds/min), 26,011,047 states left on queue. +Progress(33) at 2024-11-06 14:47:32: 794,276,423 states generated (29,617,235 s/min), 84,974,312 distinct states found (2,949,882 ds/min), 26,868,750 states left on queue. +Progress(33) at 2024-11-06 14:48:32: 823,875,831 states generated (29,599,408 s/min), 88,004,386 distinct states found (3,030,074 ds/min), 27,771,984 states left on queue. +Progress(33) at 2024-11-06 14:49:32: 853,138,894 states generated (29,263,063 s/min), 91,006,890 distinct states found (3,002,504 ds/min), 28,636,661 states left on queue. +Checkpointing of run states/24-11-06-14-20-25.868 +Checkpointing completed at (2024-11-06 14:50:32) +Progress(33) at 2024-11-06 14:50:32: 882,514,167 states generated (29,375,273 s/min), 94,011,000 distinct states found (3,004,110 ds/min), 29,534,516 states left on queue. +Progress(33) at 2024-11-06 14:51:32: 911,838,377 states generated (29,324,210 s/min), 97,108,937 distinct states found (3,097,937 ds/min), 30,498,587 states left on queue. +Progress(33) at 2024-11-06 14:52:32: 940,646,920 states generated (28,808,543 s/min), 100,248,865 distinct states found (3,139,928 ds/min), 31,472,191 states left on queue. +Progress(33) at 2024-11-06 14:53:32: 970,074,175 states generated (29,427,255 s/min), 103,170,815 distinct states found (2,921,950 ds/min), 32,265,691 states left on queue. +Progress(33) at 2024-11-06 14:54:32: 999,627,974 states generated (29,553,799 s/min), 106,004,823 distinct states found (2,834,008 ds/min), 33,009,618 states left on queue. +Progress(34) at 2024-11-06 14:55:32: 1,029,148,983 states generated (29,521,009 s/min), 108,740,783 distinct states found (2,735,960 ds/min), 33,616,222 states left on queue. +Progress(34) at 2024-11-06 14:56:32: 1,058,582,001 states generated (29,433,018 s/min), 111,612,965 distinct states found (2,872,182 ds/min), 34,375,212 states left on queue. +Progress(34) at 2024-11-06 14:57:32: 1,088,123,602 states generated (29,541,601 s/min), 114,464,196 distinct states found (2,851,231 ds/min), 35,116,195 states left on queue. +Progress(34) at 2024-11-06 14:58:32: 1,117,684,936 states generated (29,561,334 s/min), 117,252,198 distinct states found (2,788,002 ds/min), 35,817,205 states left on queue. +Progress(34) at 2024-11-06 14:59:32: 1,147,356,249 states generated (29,671,313 s/min), 120,014,476 distinct states found (2,762,278 ds/min), 36,517,255 states left on queue. +Progress(34) at 2024-11-06 15:00:32: 1,176,921,098 states generated (29,564,849 s/min), 122,859,312 distinct states found (2,844,836 ds/min), 37,291,096 states left on queue. +Progress(34) at 2024-11-06 15:01:32: 1,206,454,440 states generated (29,533,342 s/min), 125,830,942 distinct states found (2,971,630 ds/min), 38,147,762 states left on queue. +Progress(34) at 2024-11-06 15:02:32: 1,235,721,673 states generated (29,267,233 s/min), 128,869,493 distinct states found (3,038,551 ds/min), 39,035,481 states left on queue. +Progress(34) at 2024-11-06 15:03:32: 1,265,097,779 states generated (29,376,106 s/min), 131,669,552 distinct states found (2,800,059 ds/min), 39,746,864 states left on queue. +Progress(34) at 2024-11-06 15:04:32: 1,294,408,098 states generated (29,310,319 s/min), 134,604,630 distinct states found (2,935,078 ds/min), 40,584,235 states left on queue. +Progress(34) at 2024-11-06 15:05:32: 1,323,792,755 states generated (29,384,657 s/min), 137,579,390 distinct states found (2,974,760 ds/min), 41,446,478 states left on queue. +Progress(34) at 2024-11-06 15:06:32: 1,353,085,163 states generated (29,292,408 s/min), 140,575,723 distinct states found (2,996,333 ds/min), 42,309,510 states left on queue. +Progress(34) at 2024-11-06 15:07:32: 1,381,809,417 states generated (28,724,254 s/min), 143,655,566 distinct states found (3,079,843 ds/min), 43,220,682 states left on queue. +Progress(34) at 2024-11-06 15:08:32: 1,411,255,848 states generated (29,446,431 s/min), 146,482,192 distinct states found (2,826,626 ds/min), 43,944,938 states left on queue. +Progress(34) at 2024-11-06 15:09:32: 1,440,646,323 states generated (29,390,475 s/min), 149,419,989 distinct states found (2,937,797 ds/min), 44,763,293 states left on queue. +Progress(34) at 2024-11-06 15:10:32: 1,470,298,568 states generated (29,652,245 s/min), 152,041,419 distinct states found (2,621,430 ds/min), 45,311,911 states left on queue. +Progress(35) at 2024-11-06 15:11:32: 1,499,747,712 states generated (29,449,144 s/min), 154,696,867 distinct states found (2,655,448 ds/min), 45,842,895 states left on queue. +Progress(35) at 2024-11-06 15:12:32: 1,529,256,993 states generated (29,509,281 s/min), 157,493,365 distinct states found (2,796,498 ds/min), 46,535,472 states left on queue. +Progress(35) at 2024-11-06 15:13:32: 1,558,829,306 states generated (29,572,313 s/min), 160,256,575 distinct states found (2,763,210 ds/min), 47,212,471 states left on queue. +Progress(35) at 2024-11-06 15:14:32: 1,588,345,878 states generated (29,516,572 s/min), 163,002,602 distinct states found (2,746,027 ds/min), 47,862,117 states left on queue. +Progress(35) at 2024-11-06 15:15:32: 1,617,885,675 states generated (29,539,797 s/min), 165,699,121 distinct states found (2,696,519 ds/min), 48,472,896 states left on queue. +Progress(35) at 2024-11-06 15:16:32: 1,647,559,965 states generated (29,674,290 s/min), 168,343,286 distinct states found (2,644,165 ds/min), 49,065,377 states left on queue. +Progress(35) at 2024-11-06 15:17:32: 1,677,033,250 states generated (29,473,285 s/min), 171,134,409 distinct states found (2,791,123 ds/min), 49,823,330 states left on queue. +Progress(35) at 2024-11-06 15:18:32: 1,706,730,266 states generated (29,697,016 s/min), 173,860,974 distinct states found (2,726,565 ds/min), 50,493,221 states left on queue. +Error: Invariant LogSafety is violated. +Error: The behavior up to this point is: +State 1: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a3 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 2: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 1, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a3 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 3: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 1, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a3 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 4: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 1, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [term |-> 1, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a3 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 5: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 1, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [term |-> 1, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a3 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 6: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [term |-> 1, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a3 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 7: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 0, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 8: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 9: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 10: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 2, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + nextSendLsn |-> (a1 :> 1) ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 11: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 2, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 12: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 13: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<1>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 14: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 1) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 15: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 2) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<1>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 16: +/\ prop_state = ( p1 :> + [ term |-> 1, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a2 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + nextSendLsn |-> (a2 :> 3) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<1, 1>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 17: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> <<>>, + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 2, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<1, 1>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 18: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 1, + wal |-> <<1, 1>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 19: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 20: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> <<>> ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 21: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [term |-> 3, wal |-> <<>>, termHistory |-> <<[term |-> 0, lsn |-> 1]>>] ) +/\ committed = {} + +State 22: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 1) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 3, + wal |-> <<>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] ) +/\ committed = {} + +State 23: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 3, + wal |-> <<1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] ) +/\ committed = {} + +State 24: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 3, + wal |-> <<1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 25: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "campaign", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> <<>>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 26: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >>, + nextSendLsn |-> <<>> ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 27: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >>, + nextSendLsn |-> (a3 :> 1) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 28: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<4>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >>, + nextSendLsn |-> (a3 :> 1) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 29: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<4>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >>, + nextSendLsn |-> (a3 :> 2) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<4>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 30: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<4>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >>, + nextSendLsn |-> (a1 :> 1 @@ a3 :> 2) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<4>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 31: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<4>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >>, + nextSendLsn |-> (a1 :> 2 @@ a3 :> 2) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<4>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<4>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1]} + +State 32: +/\ prop_state = ( p1 :> + [ term |-> 4, + wal |-> <<4>>, + state |-> "leader", + votes |-> + ( a1 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 2, lsn |-> 1]>>, + flushLsn |-> 1 ] @@ + a3 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 2 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >>, + nextSendLsn |-> (a1 :> 2 @@ a3 :> 2) ] @@ + p2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + state |-> "leader", + votes |-> + ( a2 :> + [ termHistory |-> + <<[term |-> 0, lsn |-> 1], [term |-> 1, lsn |-> 1]>>, + flushLsn |-> 3 ] @@ + a3 :> + [ termHistory |-> <<[term |-> 0, lsn |-> 1]>>, + flushLsn |-> 1 ] ), + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >>, + nextSendLsn |-> (a2 :> 3 @@ a3 :> 2) ] ) +/\ acc_state = ( a1 :> + [ term |-> 4, + wal |-> <<4>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] @@ + a2 :> + [ term |-> 3, + wal |-> <<1, 1>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 1, lsn |-> 1], + [term |-> 3, lsn |-> 3] >> ] @@ + a3 :> + [ term |-> 4, + wal |-> <<4>>, + termHistory |-> + << [term |-> 0, lsn |-> 1], + [term |-> 2, lsn |-> 1], + [term |-> 4, lsn |-> 1] >> ] ) +/\ committed = {[term |-> 1, lsn |-> 1], [term |-> 4, lsn |-> 1]} + +1712918117 states generated, 174460942 distinct states found, 50658619 states left on queue. +The depth of the complete state graph search is 35. +Finished in 58min 19s at (2024-11-06 15:18:45) +Trace exploration spec path: ./MCProposerAcceptorStatic_TTrace_1730902825.tla diff --git a/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a5_t2_l2.cfg-2024-11-06--12-09-32.log b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a5_t2_l2.cfg-2024-11-06--12-09-32.log new file mode 100644 index 0000000000..c43d52302b --- /dev/null +++ b/safekeeper/spec/tlc-results/MCProposerAcceptorStatic.tla-MCProposerAcceptorStatic_p2_a5_t2_l2.cfg-2024-11-06--12-09-32.log @@ -0,0 +1,89 @@ +git revision: 864f4667d +Platform: Linux neon-dev-arm64-1 6.8.0-48-generic #48-Ubuntu SMP PREEMPT_DYNAMIC Fri Sep 27 14:35:45 UTC 2024 aarch64 aarch64 aarch64 GNU/Linux +CPU Info Linux: Neoverse-N1 +CPU Cores Linux: 80 +CPU Info Mac: +CPU Cores Mac: +Spec: MCProposerAcceptorStatic.tla +Config: models/MCProposerAcceptorStatic_p2_a5_t2_l2.cfg +---- +CONSTANTS +NULL = NULL +proposers = {p1, p2} +acceptors = {a1, a2, a3, a4, a5} +max_term = 2 +max_entries = 2 +SPECIFICATION Spec +CONSTRAINT StateConstraint +INVARIANT +TypeOk +ElectionSafety +LogIsMonotonic +LogSafety +SYMMETRY ProposerAcceptorSymmetry +CHECK_DEADLOCK FALSE +ALIAS Alias + +---- + +TLC2 Version 2.20 of Day Month 20?? (rev: f68cb71) +Running breadth-first search Model-Checking with fp 90 and seed 2164066158568118414 with 80 workers on 80 cores with 54613MB heap and 61440MB offheap memory [pid: 30788] (Linux 6.8.0-48-generic aarch64, Ubuntu 21.0.4 x86_64, OffHeapDiskFPSet, DiskStateQueue). +Parsing file /home/arseny/neon/safekeeper/spec/MCProposerAcceptorStatic.tla +Parsing file /tmp/tlc-13824636513165485309/TLC.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLC.tla) +Parsing file /home/arseny/neon/safekeeper/spec/ProposerAcceptorStatic.tla +Parsing file /tmp/tlc-13824636513165485309/_TLCTrace.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla) +Parsing file /tmp/tlc-13824636513165485309/Integers.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Integers.tla) +Parsing file /tmp/tlc-13824636513165485309/Sequences.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla) +Parsing file /tmp/tlc-13824636513165485309/FiniteSets.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla) +Parsing file /tmp/tlc-13824636513165485309/Naturals.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla) +Parsing file /tmp/tlc-13824636513165485309/TLCExt.tla (jar:file:/home/arseny/tla2tools.jar!/tla2sany/StandardModules/TLCExt.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 Integers +Semantic processing of module ProposerAcceptorStatic +Semantic processing of module TLCExt +Semantic processing of module _TLCTrace +Semantic processing of module MCProposerAcceptorStatic +Starting... (2024-11-06 12:09:33) +Computing initial states... +Finished computing initial states: 1 distinct state generated at 2024-11-06 12:09:36. +Progress(16) at 2024-11-06 12:09:39: 405,675 states generated (405,675 s/min), 18,042 distinct states found (18,042 ds/min), 7,612 states left on queue. +Progress(23) at 2024-11-06 12:10:39: 12,449,257 states generated (12,043,582 s/min), 467,293 distinct states found (449,251 ds/min), 161,057 states left on queue. +Progress(25) at 2024-11-06 12:11:39: 24,461,332 states generated (12,012,075 s/min), 861,011 distinct states found (393,718 ds/min), 267,072 states left on queue. +Progress(26) at 2024-11-06 12:12:39: 36,440,377 states generated (11,979,045 s/min), 1,234,052 distinct states found (373,041 ds/min), 355,372 states left on queue. +Progress(26) at 2024-11-06 12:13:39: 48,327,873 states generated (11,887,496 s/min), 1,583,736 distinct states found (349,684 ds/min), 425,209 states left on queue. +Progress(27) at 2024-11-06 12:14:39: 60,246,136 states generated (11,918,263 s/min), 1,933,499 distinct states found (349,763 ds/min), 494,269 states left on queue. +Progress(28) at 2024-11-06 12:15:39: 71,977,716 states generated (11,731,580 s/min), 2,265,302 distinct states found (331,803 ds/min), 553,777 states left on queue. +Progress(28) at 2024-11-06 12:16:39: 83,644,537 states generated (11,666,821 s/min), 2,575,451 distinct states found (310,149 ds/min), 594,142 states left on queue. +Progress(29) at 2024-11-06 12:17:39: 95,287,089 states generated (11,642,552 s/min), 2,888,793 distinct states found (313,342 ds/min), 639,273 states left on queue. +Progress(29) at 2024-11-06 12:18:39: 107,000,972 states generated (11,713,883 s/min), 3,194,255 distinct states found (305,462 ds/min), 673,353 states left on queue. +Progress(29) at 2024-11-06 12:19:39: 118,305,248 states generated (11,304,276 s/min), 3,467,775 distinct states found (273,520 ds/min), 692,915 states left on queue. +Progress(29) at 2024-11-06 12:20:39: 129,954,327 states generated (11,649,079 s/min), 3,763,186 distinct states found (295,411 ds/min), 720,349 states left on queue. +Progress(29) at 2024-11-06 12:21:39: 141,251,359 states generated (11,297,032 s/min), 4,020,407 distinct states found (257,221 ds/min), 724,036 states left on queue. +Progress(30) at 2024-11-06 12:22:39: 152,551,873 states generated (11,300,514 s/min), 4,284,278 distinct states found (263,871 ds/min), 733,726 states left on queue. +Progress(30) at 2024-11-06 12:23:39: 164,324,788 states generated (11,772,915 s/min), 4,569,569 distinct states found (285,291 ds/min), 746,476 states left on queue. +Progress(30) at 2024-11-06 12:24:39: 175,121,317 states generated (10,796,529 s/min), 4,779,505 distinct states found (209,936 ds/min), 723,070 states left on queue. +Progress(31) at 2024-11-06 12:25:39: 186,238,236 states generated (11,116,919 s/min), 5,016,034 distinct states found (236,529 ds/min), 712,944 states left on queue. +Progress(31) at 2024-11-06 12:26:39: 197,884,578 states generated (11,646,342 s/min), 5,276,094 distinct states found (260,060 ds/min), 705,471 states left on queue. +Progress(31) at 2024-11-06 12:27:39: 208,535,096 states generated (10,650,518 s/min), 5,463,450 distinct states found (187,356 ds/min), 665,661 states left on queue. +Progress(32) at 2024-11-06 12:28:39: 219,424,829 states generated (10,889,733 s/min), 5,673,673 distinct states found (210,223 ds/min), 637,975 states left on queue. +Progress(32) at 2024-11-06 12:29:39: 230,906,372 states generated (11,481,543 s/min), 5,903,516 distinct states found (229,843 ds/min), 606,255 states left on queue. +Progress(33) at 2024-11-06 12:30:39: 241,261,887 states generated (10,355,515 s/min), 6,065,731 distinct states found (162,215 ds/min), 552,728 states left on queue. +Progress(33) at 2024-11-06 12:31:39: 252,028,921 states generated (10,767,034 s/min), 6,255,487 distinct states found (189,756 ds/min), 509,620 states left on queue. +Progress(33) at 2024-11-06 12:32:39: 262,856,171 states generated (10,827,250 s/min), 6,431,063 distinct states found (175,576 ds/min), 448,834 states left on queue. +Progress(34) at 2024-11-06 12:33:39: 273,211,882 states generated (10,355,711 s/min), 6,586,644 distinct states found (155,581 ds/min), 386,905 states left on queue. +Progress(34) at 2024-11-06 12:34:39: 283,843,415 states generated (10,631,533 s/min), 6,743,916 distinct states found (157,272 ds/min), 315,135 states left on queue. +Progress(35) at 2024-11-06 12:35:39: 293,931,115 states generated (10,087,700 s/min), 6,878,405 distinct states found (134,489 ds/min), 241,126 states left on queue. +Progress(36) at 2024-11-06 12:36:39: 303,903,441 states generated (9,972,326 s/min), 6,996,394 distinct states found (117,989 ds/min), 152,775 states left on queue. +Progress(37) at 2024-11-06 12:37:39: 313,501,886 states generated (9,598,445 s/min), 7,093,031 distinct states found (96,637 ds/min), 54,009 states left on queue. +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 = 1.2E-4 + based on the actual fingerprints: val = 2.1E-6 +318172398 states generated, 7127950 distinct states found, 0 states left on queue. +The depth of the complete state graph search is 44. +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 9 and the 95th percentile is 3). +Finished in 28min 43s at (2024-11-06 12:38:16)