tla/storage: add big doubled test

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

Author: Serpentian

proofs/tla/test/storage/DoubledBigTest.cfg

@@ -0,0 +1,27 @@
+INIT Init
+NEXT Next
+
+CONSTANTS
+    Storages <- StoragesC
+    ReplicaSets <- ReplicaSetsC
+    BucketIds <- BucketIdsC
+    StorageAssignments <- StorageAssignmentsC
+    BucketAssignments <- BucketAssignmentsC
+    MasterAssignments <- MasterAssignmentsC
+    b1 = b1
+    b2 = b2
+    b3 = b3
+    b4 = b4
+
+SYMMETRY Symmetry
+
+INVARIANTS
+    NetworkTypeInv
+    StorageTypeInv
+    StorageToReplicasetTypeInv
+    NoActiveSimultaneousInv
+
+CONSTRAINT
+    SendLimitConstraint
+    NetworkBoundConstraint
+    RefConstraint

proofs/tla/test/storage/DoubledBigTest.tla

@@ -0,0 +1,70 @@
+--------------------------- MODULE DoubledBigTest ------------------------------
+EXTENDS storage, utils
+
+CONSTANTS b1, b2, b3, b4
+
+StoragesC == {"s1", "s2", "s3", "s4"}
+ReplicaSetsC == {"rs1", "rs2", "rs3"}
+BucketIdsC == {b1, b2, b3, b4}
+StorageAssignmentsC == [rs1 |-> {"s1", "s2"},
+                       rs2 |-> {"s3"},
+                       rs3 |-> {"s4"}]
+BucketAssignmentsC == [rs1 |-> {b1},
+                       rs2 |-> {b2},
+                       rs3 |-> {b3, b4}]
+MasterAssignmentsC == [rs1 |-> {"s1"},
+                       rs2 |-> {"s3"},
+                       rs3 |-> {"s4"}]
+
+(***************************************************************************)
+(*                           CONSTRAINTS                                   *)
+(***************************************************************************)
+
+MAX_TOTAL_SENDS == 3
+
+\* 1. Limit total bucket sends - prevent endless transfers.
+SendLimitConstraint ==
+    LET totalSends ==
+        SetSum({ storages[i].errinj.bucketSendCount : i \in StoragesC })
+    IN totalSends =< MAX_TOTAL_SENDS
+
+\* 2. Keep network bounded - avoid message explosion.
+NetworkBoundConstraint ==
+    /\ \A s1, s2 \in StoragesC :
+            Len(network[s1][s2]) =< 3
+    /\ \A s \in StoragesC :
+        /\ storages[s].errinj.networkReorderCount <= 2
+        /\ storages[s].errinj.networkDropCount <= 2
+
+RefConstraint ==
+    \A s1 \in StoragesC :
+        /\ storages[s1].errinj.bucketRWRefCount <= 2
+        /\ storages[s1].errinj.bucketRORefCount <= 2
+        /\ storages[s1].errinj.bucketRWUnRefCount <= 2
+        /\ storages[s1].errinj.bucketROUnRefCount <= 2
+
+(***************************************************************************)
+(*                            SYMMETRY                                     *)
+(***************************************************************************)
+
+Symmetry ==
+    Permutations(BucketIdsC)
+
+(***************************************************************************)
+(*                           STATE INVARIANTS                              *)
+(***************************************************************************)
+
+NoActiveSimultaneousInv ==
+    \* No bucket can be ACTIVE in storages belonging to different ReplicaSets
+    \A b \in BucketIds :
+        \A rs1, rs2 \in ReplicaSets :
+            rs1 # rs2 =>
+                ~(\E s1, s2 \in Storages :
+                     storageToReplicaset[s1] = rs1 /\
+                     storageToReplicaset[s2] = rs2 /\
+                     storages[s1].status = "master" /\
+                     storages[s2].status = "master" /\
+                     storages[s1].buckets[b].status = "ACTIVE" /\
+                     storages[s2].buckets[b].status = "ACTIVE")
+
+================================================================================