minerva 0.2.0

Causal ordering for distributed systems
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

extern crate alloc;

use alloc::collections::BTreeSet;
use alloc::vec::Vec;

use crate::metis::{Dot, DotSet};
use proptest::prelude::*;

mod difference;
mod exact;
mod lattice;
mod reads;
mod restriction;

/// A receipt stream over a small dot domain, including duplicates and dot zero.
fn arb_dots() -> impl Strategy<Value = Vec<(u32, u64)>> {
    prop::collection::vec((0u32..4, 0u64..12), 0..24)
}

/// Sub-rosters over and slightly past the dot domain's stations, duplicates included.
fn arb_subroster() -> impl Strategy<Value = Vec<u32>> {
    prop::collection::vec(0u32..6, 0..6)
}

/// Builds a have-set by inserting every dot in order. A drawn pair naming
/// the non-dot counter zero cannot cross into the identity type, so it
/// drops here --- the same no-op the door's zero refusal used to give
/// (ruling R-91).
fn have(dots: &[(u32, u64)]) -> DotSet {
    let mut set = DotSet::new();
    for &pair in dots {
        if let Ok(dot) = Dot::try_from(pair) {
            let _ = set.insert(dot);
        }
    }
    set
}

/// The reference model: the plain set of genuine dots. The crossing is the
/// model's `dot != 0` filter: a drawn zero counter is no dot and drops.
fn model(dots: &[(u32, u64)]) -> BTreeSet<Dot> {
    dots.iter()
        .copied()
        .filter_map(|pair| Dot::try_from(pair).ok())
        .collect()
}