diff options
Diffstat (limited to 'storage/specs')
| -rw-r--r-- | storage/specs/bucketinfo/bucketinfo.tla | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/storage/specs/bucketinfo/bucketinfo.tla b/storage/specs/bucketinfo/bucketinfo.tla index ba540ae1763..8224ff6a4f1 100644 --- a/storage/specs/bucketinfo/bucketinfo.tla +++ b/storage/specs/bucketinfo/bucketinfo.tla @@ -1,6 +1,6 @@ ------------------------------ MODULE bucketinfo ------------------------------ -EXTENDS Naturals, FiniteSets, Sequences, Integers, TLC +EXTENDS FiniteSets, Sequences, Integers, TLC (***************************************************************************) (* This spec models the state synchronization mechanisms for a single data *) @@ -42,13 +42,13 @@ CONSTANTS DistributorNodes, ContentNode, ClusterStates, NodeEpochs, MutatingOps, Null ASSUME /\ IsFiniteSet(DistributorNodes) - /\ Cardinality(DistributorNodes) > 0 + /\ DistributorNodes # {} /\ IsFiniteSet(ClusterStates) - /\ Cardinality(ClusterStates) > 0 + /\ ClusterStates # {} /\ IsFiniteSet(NodeEpochs) - /\ Cardinality(NodeEpochs) > 0 + /\ NodeEpochs # {} /\ IsFiniteSet(MutatingOps) - /\ Cardinality(MutatingOps) > 0 + /\ MutatingOps # {} /\ ClusterStates \subseteq (Nat \ {0}) /\ NodeEpochs \subseteq (Nat \ {0}) /\ DistributorNodes \intersect {ContentNode} = {} |