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

use proptest::prelude::*;

/// Dense physical-reading window for clock-driven properties.
const SKEW_PHYSICAL_MAX: u64 = 4096;

/// Local physical readings: dense low values plus the top of `u64`, including
/// the former pre-S5 sentinel.
pub(super) fn physical_reading() -> impl Strategy<Value = u64> {
    prop_oneof![
        0u64..=SKEW_PHYSICAL_MAX,
        (u64::MAX - SKEW_PHYSICAL_MAX)..=u64::MAX,
    ]
}

/// Remote physical times. The high window stops one below `u64::MAX`, because
/// `(u64::MAX, u16::MAX)` has no successor for `after`.
pub(super) fn remote_physical() -> impl Strategy<Value = u64> {
    prop_oneof![
        0u64..=SKEW_PHYSICAL_MAX,
        (u64::MAX - SKEW_PHYSICAL_MAX)..=(u64::MAX - 1),
    ]
}