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

use super::super::super::support::{arb_vv, dot};
use super::{arb_dots, have};
use crate::metis::DotSet;
use proptest::prelude::*;

proptest! {
    /// Intersection is the meet of the have-set lattice.
    #[test]
    fn prop_intersect_is_the_meet(a in arb_dots(), b in arb_dots(), c in arb_dots()) {
        let (sa, sb, sc) = (have(&a), have(&b), have(&c));
        let both = sa.intersect(&sb);
        for station in 0u32..4 {
            for counter in 1u64..13 {
                prop_assert_eq!(
                    both.contains(dot(station, counter)),
                    sa.contains(dot(station, counter)) && sb.contains(dot(station, counter))
                );
            }
        }
        prop_assert_eq!(&both, &sb.intersect(&sa));
        prop_assert_eq!(sa.intersect(&sb).intersect(&sc), sa.intersect(&sb.intersect(&sc)));
        prop_assert_eq!(sa.intersect(&sa), sa);
    }

    /// On intersections, floor is exact while high water is lax.
    #[test]
    fn prop_floor_is_exact_and_high_water_lax_on_intersections(
        a in arb_dots(), b in arb_dots(), v in arb_vv(), w in arb_vv(),
    ) {
        let (sa, sb) = (have(&a), have(&b));
        let both = sa.intersect(&sb);
        prop_assert_eq!(both.floor(), sa.floor().meet(&sb.floor()));
        let met_high_waters = sa.high_water().meet(&sb.high_water());
        prop_assert!(both.high_water() <= met_high_waters);
        prop_assert_eq!(
            DotSet::from_cut(&v.meet(&w)),
            DotSet::from_cut(&v).intersect(&DotSet::from_cut(&w))
        );
    }
}