diff options
| author | Tor Brede Vekterli <vekterli@yahooinc.com> | 2023-08-23 10:54:56 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-08-23 10:54:56 +0200 |
| commit | 0b90f4fd3efc480d7fa2f46b037ccb6b3c5e13a9 (patch) | |
| tree | aae2045237e81bffe82f6ee737b74c908aec9436 /storage | |
| parent | 2a45a1c85f78bac78a8eace3c99998e1c92e1c4a (diff) | |
| parent | 0b9b52da8ca18438aae86737a87495c7359679ff (diff) | |
Merge pull request #28111 from vespa-engine/vekterli/minor-spec-simplifications
Minor spec simplifications
Diffstat (limited to 'storage')
| -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} = {} |