| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
| |
A sequence of length n is defined as a function whose domain is
equal to 1..n (note: 1-indexing), so just use the domain directly
instead of manually constructing the range.
|
| |
|
|
|
|
|
|
| |
- 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.
|
|
|
This spec models a potential direction for future changes to the
bucket state synchronization protocols; in this case greatly
simplified to involve just a single data bucket between multiple
distributors and a single content node.
The core assumption is that if this mechanism is correct for one
bucket, it will be correct for any larger set of buckets (assuming
bucket independence, which is a half-truth due to splits and joins in
an actual system). It is important to note that this only models
single-replica eventual consistency. It is not intended to cover
cross-replica consistency, as that is inherently a much more complex
story. The model may be expanded to cover this case later.
This specification is explicitly bounded in its state space and is
therefore only able to model a subset of the infinite state space of
a real system. Such is life.
|
