From 0b9b52da8ca18438aae86737a87495c7359679ff Mon Sep 17 00:00:00 2001 From: Tor Brede Vekterli Date: Tue, 22 Aug 2023 17:15:07 +0200 Subject: 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. --- storage/specs/bucketinfo/bucketinfo.tla | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'storage') 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} = {} -- cgit v1.2.3