tla/storage: initial implementation [doubled buckets problem investigation] #616

Serpentian · 2025-10-31T21:39:17Z

The PR is here in order to have a place, where I can show, how changes from RFC make the situation better and in order to investigate traces of doubled buckets

Run the tests with:

JAVA_OPTS="-DTLA-Library=../../src" tlc
    DoubledBucketsSmallTest.tla -config DoubledBucketsSmallTest.cfg -workers 6

TODO: refactor network reorder and drop to use storage states
TODO: ctest integration

Serpentian · 2025-10-31T21:48:55Z

Doubled buckets after master switch

Traces of DoubledBucketsSmallTest.tla

Error: Invariant NoActiveSimultaneousInv is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]
/\ totalSentCount = 0

State 2: <TestNext line 99, col 13 to line 101, col 44 of module DoubledBucketsSmallTest>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]
/\ totalSentCount = 1

State 3: <TestNext line 84, col 12 to line 93, col 38 of module DoubledBucketsSmallTest>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |-> <<>>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |->
            << [ type |-> "BUCKET_RECV_RESPONSE",
                 content |-> [status |-> TRUE, bucket |-> b1] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]
/\ totalSentCount = 1

State 4: <TestNext line 84, col 12 to line 93, col 38 of module DoubledBucketsSmallTest>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> TRUE] ] >>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]
/\ totalSentCount = 1

State 5: <TestNext line 84, col 12 to line 93, col 38 of module DoubledBucketsSmallTest>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |-> <<>>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "ACTIVE",
                       bucket |-> b1,
                       destination |-> "NULL" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 2, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]
/\ totalSentCount = 1

State 6: <TestNext line 79, col 11 to line 80, col 37 of module DoubledBucketsSmallTest>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |-> <<>>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "ACTIVE",
                       bucket |-> b1,
                       destination |-> "NULL" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 2, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [status |-> "replica", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]
/\ totalSentCount = 1

Traces of MasterDoubledTest.tla

Error: Invariant NoActiveSimultaneousInv is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ phase = 1
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]

State 2: <TestNext line 50, col 6 to line 62, col 48 of module SpecificDoubledTest>
/\ phase = 1
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]

State 3: <TestNext line 50, col 6 to line 62, col 48 of module SpecificDoubledTest>
/\ phase = 1
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |-> <<>>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |->
            << [ type |-> "BUCKET_RECV_RESPONSE",
                 content |-> [status |-> TRUE, bucket |-> b1] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]

State 4: <TestNext line 50, col 6 to line 62, col 48 of module SpecificDoubledTest>
/\ phase = 1
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> TRUE] ] >>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]

State 5: <TestNext line 50, col 6 to line 62, col 48 of module SpecificDoubledTest>
/\ phase = 1
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |-> <<>>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "ACTIVE",
                       bucket |-> b1,
                       destination |-> "NULL" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 2, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]

State 6: <TestNext line 64, col 6 to line 68, col 18 of module SpecificDoubledTest>
/\ phase = 3
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |-> <<>>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "ACTIVE",
                       bucket |-> b1,
                       destination |-> "NULL" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 2, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]

"Phase 3: failover, s2 becomes master"
State 7: <TestNext line 70, col 6 to line 74, col 18 of module SpecificDoubledTest>
/\ phase = 4
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENDING",
                       bucket |-> b1,
                       destination |-> "rs2" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       destination |-> "rs2" ] ] >>,
        s3 |-> <<>>,
        s4 |-> <<>> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>],
  s3 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |-> <<>>,
        s4 |->
            << [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "RECEIVING",
                       bucket |-> b1,
                       destination |-> "rs1" ] ],
               [ type |-> "REPLICATION_BUCKET",
                 content |->
                     [ status |-> "ACTIVE",
                       bucket |-> b1,
                       destination |-> "NULL" ] ] >> ],
  s4 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>, s4 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs1", s3 |-> "rs2", s4 |-> "rs2"]
/\ storages = [s1 |-> [buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s2 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"] @@ b4 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s3 |-> [buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 2, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})], s4 |-> [buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b4 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "replica", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0, s4 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b4 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {} @@ b4 :> {})]]

"Phase 3: failover, s2 becomes master"

Doubled buckets after stray TCP

Traces of StrayTCPDoubledTest

State 1: <Initial predicate>
/\ phase = 1
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 2: <TestNext line 47, col 6 to line 51, col 41 of module StrayTCPDoubledTest>
/\ phase = 2
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 3: <TestNext line 53, col 6 to line 57, col 41 of module StrayTCPDoubledTest>
/\ phase = 3
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 4: <TestNext line 59, col 6 to line 68, col 48 of module StrayTCPDoubledTest>
/\ phase = 3
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ],
               [ type |-> "RECOVERY_BUCKET_STAT",
                 content |-> [bucket |-> b1] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 5: <TestNext line 59, col 6 to line 68, col 48 of module StrayTCPDoubledTest>
/\ phase = 3
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [type |-> "RECOVERY_BUCKET_STAT", content |-> [bucket |-> b1]],
               [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 6: <TestNext line 59, col 6 to line 68, col 48 of module StrayTCPDoubledTest>
/\ phase = 3
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |->
      [ s1 |->
            << [ type |-> "RECOVERY_BUCKET_STAT_RESPONSE",
                 content |->
                     [ status |-> "NULL",
                       bucket |-> b1,
                       transferring |-> FALSE ] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>> ] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 7: <TestNext line 59, col 6 to line 68, col 48 of module StrayTCPDoubledTest>
/\ phase = 3
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 8: <TestNext line 70, col 6 to line 74, col 60 of module StrayTCPDoubledTest>
/\ phase = 4
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 9: <TestNext line 76, col 6 to line 84, col 48 of module StrayTCPDoubledTest>
/\ phase = 4
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 3, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 10: <TestNext line 76, col 6 to line 84, col 48 of module StrayTCPDoubledTest>
/\ phase = 4
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |->
      [ s1 |->
            << [ type |-> "BUCKET_RECV_RESPONSE",
                 content |-> [status |-> TRUE, bucket |-> b1] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>> ],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 3, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 1, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 11: <TestNext line 76, col 6 to line 84, col 48 of module StrayTCPDoubledTest>
/\ phase = 4
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> TRUE] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 1, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 12: <TestNext line 76, col 6 to line 84, col 48 of module StrayTCPDoubledTest>
/\ phase = 4
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 13: <TestNext line 86, col 6 to line 91, col 60 of module StrayTCPDoubledTest>
/\ phase = 5
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 14: <TestNext line 93, col 6 to line 95, col 18 of module StrayTCPDoubledTest>
/\ phase = 6
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "GARBAGE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 5, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 15: <TestNext line 97, col 6 to line 102, col 18 of module StrayTCPDoubledTest>
/\ phase = 7
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |->
      [ s1 |->
            << [ type |-> "BUCKET_RECV_RESPONSE",
                 content |-> [status |-> TRUE, bucket |-> b1] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>> ] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "GARBAGE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 5, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 16: <TestNext line 104, col 6 to line 109, col 60 of module StrayTCPDoubledTest>
/\ phase = 8
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |->
      [ s1 |->
            << [ type |-> "BUCKET_RECV_RESPONSE",
                 content |-> [status |-> TRUE, bucket |-> b1] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>> ] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "GARBAGE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 5, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 17: <TestNext line 111, col 6 to line 119, col 27 of module StrayTCPDoubledTest>
/\ phase = 8
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "GARBAGE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 5, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 1, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 18: <TestNext line 111, col 6 to line 119, col 27 of module StrayTCPDoubledTest>
/\ phase = 8
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |->
      [ s1 |->
            <<[type |-> "RECOVERY_BUCKET_STAT", content |-> [bucket |-> b1]]>>,
        s2 |-> <<>>,
        s3 |-> <<>> ] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "GARBAGE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 5, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 1, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 19: <TestNext line 111, col 6 to line 119, col 27 of module StrayTCPDoubledTest>
/\ phase = 8
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "RECOVERY_BUCKET_STAT_RESPONSE",
                 content |->
                     [ status |-> "GARBAGE",
                       bucket |-> b1,
                       transferring |-> FALSE ] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "GARBAGE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 5, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 1, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 20: <TestNext line 111, col 6 to line 119, col 27 of module StrayTCPDoubledTest>
/\ phase = 8
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [networkReorderCount |-> 1, networkDropCount |-> 0, bucketSendCount |-> 2, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "GARBAGE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 5, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 0, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [networkReorderCount |-> 0, networkDropCount |-> 1, bucketSendCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), status |-> "master", vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 2], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

1528 states generated, 332 distinct states found, 61 states left on queue.

Traces of DoubledBucketsTest.tla

Error: Invariant NoActiveSimultaneousInv is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 2: <StorageStateApply line 638, col 16 to line 638, col 65 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 1, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 3: <StorageStateApply line 643, col 19 to line 643, col 75 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 1, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 4: <StorageStateApply line 640, col 19 to line 640, col 73 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ],
               [ type |-> "RECOVERY_BUCKET_STAT",
                 content |-> [bucket |-> b1] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 1, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 5: <ReorderOneNetworkMessage line 595, col 5 to line 600, col 41 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [type |-> "RECOVERY_BUCKET_STAT", content |-> [bucket |-> b1]],
               [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 1, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 6: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |->
      [ s1 |->
            << [ type |-> "RECOVERY_BUCKET_STAT_RESPONSE",
                 content |->
                     [ status |-> "NULL",
                       bucket |-> b1,
                       transferring |-> FALSE ] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>> ] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 1, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs3"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 1, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 7: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 1, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 2, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 8: <StorageStateApply line 638, col 16 to line 638, col 65 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 3, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 9: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |->
      [ s1 |->
            << [ type |-> "BUCKET_RECV_RESPONSE",
                 content |-> [status |-> TRUE, bucket |-> b1] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>> ],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENDING", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 3, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {b1}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 1, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 10: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> TRUE] ] >>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 1, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 11: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "BUCKET_RECV",
                 content |-> [bucket |-> b1, final |-> FALSE] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "NULL", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 12: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |->
      [ s1 |->
            << [ type |-> "BUCKET_RECV_RESPONSE",
                 content |-> [status |-> TRUE, bucket |-> b1] ] >>,
        s2 |-> <<>>,
        s3 |-> <<>> ] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 13: <DropOneNetworkMessage line 607, col 8 to line 611, col 44 of module storage>
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 14: <StorageStateApply line 640, col 19 to line 640, col 73 of module storage>
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |->
      [ s1 |->
            <<[type |-> "RECOVERY_BUCKET_STAT", content |-> [bucket |-> b1]]>>,
        s2 |-> <<>>,
        s3 |-> <<>> ] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 15: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |->
      [ s1 |-> <<>>,
        s2 |-> <<>>,
        s3 |->
            << [ type |-> "RECOVERY_BUCKET_STAT_RESPONSE",
                 content |->
                     [ status |-> "SENT",
                       bucket |-> b1,
                       transferring |-> FALSE ] ] >> ],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "RECEIVING", destination |-> "rs1"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 1], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

State 16: <Next line 625, col 15 to line 633, col 73 of module storage>
/\ network = [ s1 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s2 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>],
  s3 |-> [s1 |-> <<>>, s2 |-> <<>>, s3 |-> <<>>] ]
/\ storageToReplicaset = [s1 |-> "rs1", s2 |-> "rs2", s3 |-> "rs3"]
/\ storages = [s1 |-> [errinj |-> [bucketSendCount |-> 2, networkReorderCount |-> 1, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "SENT", destination |-> "rs2"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 4, s2 |-> 0, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> TRUE, rw_lock |-> TRUE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s2 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 0, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b3 :> [status |-> "NULL", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 2, s3 |-> 0], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})], s3 |-> [errinj |-> [bucketSendCount |-> 0, networkReorderCount |-> 0, networkDropCount |-> 1, bucketRWRefCount |-> 0, bucketRORefCount |-> 0, bucketRWUnRefCount |-> 0, bucketROUnRefCount |-> 0], status |-> "master", buckets |-> (b1 :> [status |-> "ACTIVE", destination |-> "NULL"] @@ b2 :> [status |-> "NULL", destination |-> "NULL"] @@ b3 :> [status |-> "ACTIVE", destination |-> "NULL"]), vclock |-> [s1 |-> 0, s2 |-> 0, s3 |-> 2], transferingBuckets |-> {}, bucketRefs |-> (b1 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b2 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE] @@ b3 :> [ro |-> 0, rw |-> 0, ro_lock |-> FALSE, rw_lock |-> FALSE]), gcAck |-> (b1 :> {} @@ b2 :> {} @@ b3 :> {})]]

4925668839 states generated, 91003145 distinct states found, 52694822 states left on queue.
The depth of the complete state graph search is 17.
Finished in 05h 32min at (2025-11-02 22:48:03)
Trace exploration spec path: ./DoubledBucketsTest_TTrace_1762092911.tla

Gerold103 · 2025-10-31T22:41:33Z

Man, this is impressive 😨. Genius idea to use TLA for this 🔥!

Run the tests with: ```sh JAVA_OPTS="-DTLA-Library=../../src" tlc DoubledBucketsSmallTest.tla -config DoubledBucketsSmallTest.cfg -workers 6 -continue -checkpoint 10 ``` DoubledBucketsSmallTest reliably reproduces the doubled bucket problem, which is related to master change. DoubledBucketsTest requires constraints to become useful. NO_DOC=tla NO_TEST=tla

This commit implements first part of RFC for doubled buckets: syncing of replication after making a bucket `SENDING`, this protects us from the doubled bucket after master switch situation, and consequently, fixes the MasterDoubledTest and DoubledBucketsSmall tests, which reproduce that issue. Part of tarantool#576 NO_DOC=tla NO_TEST=tla

This commit prohibits any recovery or rebalancer related stuff on the masters, which have not yet synced with the replicaset after becoming master. Part of tarantool#214 NO_DOC=tla NO_TEST=tla

This commit prepares vshard bucket rebalancing algorithm to be resistant for the tarantool#214 issue. It introduces the persistent bucket generation, which is incremented on every `SENDING` status. Part of tarantool#214 NO_DOC=tla NO_TEST=tla

This commit should resolve the tarantool#214 issue. Works as follows: Recovery uses that generation in order to distinguish, which bucket is more recent, if it cannot find a bucket on the sender node. So, firstly, the node goes to the sender, if there's a bucket with any state and greater generation, local one is `GARBAGE`, we don't care about the status here. If bucket generation is equal to the local one, we use the old logic, if the bucket is missing from remote node, then fullscan all masters of the cluster. When all of the nodes replied, if there exists higher generation, the local is `GARBAGE`, `ACTIVE` otherwise. Part of tarantool#214 NO_DOC=tla NO_TEST=tla

This is the test, I'm going to execute on VM for week. Let's try finding the doubled buckets cases. NO_DOC=tla NO_TEST=tla

Serpentian self-assigned this Oct 31, 2025

Serpentian changed the title ~~tla/storage: initial implementation~~ tla/storage: initial implementation [doubled buckets problem investigation] Oct 31, 2025

Serpentian force-pushed the vshard-storage-tla-plus-spec branch 6 times, most recently from 11e601a to 5aecb0e Compare November 5, 2025 08:46

Serpentian added 6 commits November 5, 2025 12:01

tla/storage: implement prohibiting recovery and rebalance before sync

8c174ee

This commit prohibits any recovery or rebalancer related stuff on the masters, which have not yet synced with the replicaset after becoming master. Part of tarantool#214 NO_DOC=tla NO_TEST=tla

tla/storage: implement bucket generations

858afe4

This commit prepares vshard bucket rebalancing algorithm to be resistant for the tarantool#214 issue. It introduces the persistent bucket generation, which is incremented on every `SENDING` status. Part of tarantool#214 NO_DOC=tla NO_TEST=tla

tla/storage: add big doubled test

e7ad7ef

This is the test, I'm going to execute on VM for week. Let's try finding the doubled buckets cases. NO_DOC=tla NO_TEST=tla

Serpentian force-pushed the vshard-storage-tla-plus-spec branch from 5aecb0e to e7ad7ef Compare November 5, 2025 10:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

tla/storage: initial implementation [doubled buckets problem investigation] #616

tla/storage: initial implementation [doubled buckets problem investigation] #616

Uh oh!

Serpentian commented Oct 31, 2025 •

edited

Loading

Uh oh!

Serpentian commented Oct 31, 2025 •

edited

Loading

Uh oh!

Gerold103 commented Oct 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

tla/storage: initial implementation [doubled buckets problem investigation] #616

Are you sure you want to change the base?

tla/storage: initial implementation [doubled buckets problem investigation] #616

Uh oh!

Conversation

Serpentian commented Oct 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Serpentian commented Oct 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Gerold103 commented Oct 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Serpentian commented Oct 31, 2025 •

edited

Loading

Serpentian commented Oct 31, 2025 •

edited

Loading