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
47
48
49
50

use super::super::super::support::arb_vv;
use core::cmp::Ordering;
use proptest::prelude::*;

proptest! {
    /// The relation is a partial order: reflexive, antisymmetric, transitive.
    #[test]
    fn prop_partial_order_reflexive_antisymmetric_transitive(
        a in arb_vv(), b in arb_vv(), c in arb_vv(),
    ) {
        prop_assert_eq!(a.partial_cmp(&a), Some(Ordering::Equal));
        if a <= b && b <= a {
            prop_assert_eq!(&a, &b);
        }
        if a <= b && b <= c {
            prop_assert!(a <= c);
        }
    }

    /// Concurrency is exactly incomparability under the partial order.
    #[test]
    fn prop_concurrent_iff_incomparable(a in arb_vv(), b in arb_vv()) {
        prop_assert_eq!(a.concurrent(&b), a.partial_cmp(&b).is_none());
        if a.concurrent(&b) {
            prop_assert!(!a.happens_before(&b));
            prop_assert!(!b.happens_before(&a));
        }
    }

    /// A local event moves a vector strictly up the order.
    #[test]
    fn prop_increment_dominates(a in arb_vv(), station in 0u32..6) {
        let mut b = a.clone();
        let before = b.get(station);
        let after = b.increment(station);
        prop_assert_eq!(after, before.saturating_add(1));
        // Generation keeps counters below the ceiling, so the bump is strict.
        prop_assert!(a.happens_before(&b));
    }

    /// A station outside a vector's history reads as zero, and observing zero
    /// there changes nothing.
    #[test]
    fn prop_absent_equals_zero(a in arb_vv(), station in 100u32..200) {
        prop_assert_eq!(a.get(station), 0); // 100..200 is outside the 0..6 domain.
        let mut b = a.clone();
        b.observe(station, 0);
        prop_assert_eq!(&a, &b);
    }
}