Module I_IntVector

Vector Clocks.

An integer vector where each replica is restricted to incrementing its own index i. This index is generated at random and assigned to a numsite value when calling make () or make_in_range n. All subsequent calls to update operations will only act on the position noted by numsite.

By default, Immutable_types.Mergeable.make just calls Immutable_types.IVector.make_in_range n with n = 11. You can override this by calling make_in_range directly.

A Vector Clock is a Immutable_types.IVector with type elt = int list

include Immutable_types.IVector with type elt = int list
include Immutable_types.Mergeable
type t

Type of mergeable elements.

val make : unit -> t

Create a new mergeable element.

val merge : t -> t -> t

merge a b will merge the state of a and the one from b to create a new mergeable element.

type elt = int list

Type of the contents of an IVector

val make_in_range : int -> t

make_in_range n creates a new IVector of size ranging from 0 to n. being n greater than 0 and smaller than 2^30.

When merging two CRDTs of different sizes, the smaller one grows and pads the remaining space with zeros.

val query : t -> elt

query t returns the raw state of t

val incr : t -> t

incr t increments the position associated with the numsite of t. See I_IntVector for more information on numsites.