Minor spec simplifications

- Nat (the set of natural numbers) is already present in Integers,
  so no need to extend Naturals.
- Instead of computing cardinality of constant sets to verify that
  that the provided set has at least one element, just compare against
  the empty set.

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} = {}