minerva 0.2.0

Causal ordering for distributed systems
use super::{arb_cut, arb_subroster, is_genuine_cut};
use crate::metis::VersionVector;
use proptest::prelude::*;

proptest! {
    #[test]
    fn prop_closures_preserve_gap_freedom(
        a in arb_cut(), b in arb_cut(), roster in arb_subroster(),
    ) {
        prop_assert!(is_genuine_cut(&a.meet(&b)));
        prop_assert!(is_genuine_cut(&a.merge(&b)));
        prop_assert!(is_genuine_cut(&a.restrict(roster.iter().copied())));
    }

    #[test]
    fn prop_closures_agree_with_the_vector_operations(
        a in arb_cut(), b in arb_cut(), roster in arb_subroster(),
    ) {
        let (va, vb) = (a.as_vector().clone(), b.as_vector().clone());
        let (met, merged, restricted) = (
            a.meet(&b),
            a.merge(&b),
            a.restrict(roster.iter().copied()),
        );

        prop_assert_eq!(met.as_vector(), &va.meet(&vb));
        prop_assert_eq!(merged.as_vector(), &va.merge(&vb));
        prop_assert_eq!(restricted.as_vector(), &va.restrict(roster.iter().copied()));
    }

    #[test]
    fn prop_partial_order_delegates_to_the_vector(a in arb_cut(), b in arb_cut()) {
        prop_assert_eq!(a.partial_cmp(&b), a.as_vector().partial_cmp(b.as_vector()));
    }

    #[test]
    fn prop_order_preserved_under_meet_merge_restrict(
        a in arb_cut(), b in arb_cut(), roster in arb_subroster(),
    ) {
        let met = a.meet(&b);
        let merged = a.merge(&b);
        prop_assert!(met <= a && met <= b);
        prop_assert!(a <= merged && b <= merged);

        if a <= b {
            let ra = a.restrict(roster.iter().copied());
            let rb = b.restrict(roster.iter().copied());
            prop_assert!(ra <= rb);
        }
    }

    #[test]
    fn prop_difference_is_the_residual(a in arb_cut(), b in arb_cut()) {
        let owed = a.difference(&b);

        prop_assert_eq!(&owed, &a.as_vector().difference(b.as_vector()));
        prop_assert_eq!(b.as_vector().merge(&owed), a.merge(&b).into_vector());
        prop_assert_eq!(owed == VersionVector::new(), a <= b);

        let owed_dots = a.to_have_set().difference(&b.to_have_set()).count();
        let owed_count = owed
            .iter()
            .map(|(station, count)| count - b.as_vector().get(station))
            .sum::<u64>();
        prop_assert_eq!(owed_dots as u64, owed_count);
    }
}