extern crate alloc;
use alloc::collections::{BTreeMap, BTreeSet};
use alloc::vec::Vec;
use crate::metis::{Dot, DotMap, DotSet, Dotted};
use proptest::prelude::*;
mod convergence;
mod delta;
mod disjoint;
mod merge;
mod restriction;
type Doc = Dotted<DotMap<u8, DotSet>>;
#[derive(Clone, Debug)]
enum Op {
Add { replica: usize, key: u8 },
Remove { replica: usize, key: u8 },
Gossip { from: usize, to: usize },
}
const REPLICAS: usize = 3;
fn arb_ops() -> impl Strategy<Value = Vec<Op>> {
let op = prop_oneof![
(0..REPLICAS, 0u8..3).prop_map(|(replica, key)| Op::Add { replica, key }),
(0..REPLICAS, 0u8..3).prop_map(|(replica, key)| Op::Remove { replica, key }),
(0..REPLICAS, 0..REPLICAS).prop_map(|(from, to)| Op::Gossip { from, to }),
];
prop::collection::vec(op, 0..24)
}
struct Record {
minted: BTreeMap<Dot, u8>,
expelled: BTreeSet<Dot>,
}
fn run(ops: &[Op]) -> (Vec<Doc>, Record) {
let mut live: Vec<Doc> = (0..REPLICAS).map(|_| Dotted::new()).collect();
let mut record = Record {
minted: BTreeMap::new(),
expelled: BTreeSet::new(),
};
for op in ops {
match *op {
Op::Add { replica, key } => {
let station = u32::try_from(replica).unwrap();
let fresh = live[replica].next_dot(station);
let mut held = DotSet::new();
assert!(held.insert(fresh));
let delta = Dotted::from_store(DotMap::singleton(key, held));
live[replica] = live[replica].merge(&delta);
let _ = record.minted.insert(fresh, key);
}
Op::Remove { replica, key } => {
let observed = live[replica].store().get(&key).cloned().unwrap_or_default();
for dot in observed.difference(&DotSet::new()) {
let _ = record.expelled.insert(dot);
}
let delta = Dotted::from_context(observed);
live[replica] = live[replica].merge(&delta);
}
Op::Gossip { from, to } => {
let learned = live[to].merge(&live[from]);
live[to] = learned;
}
}
}
(live, record)
}
fn expected(record: &Record) -> DotMap<u8, DotSet> {
let mut store = DotMap::new();
for (&minted, &key) in &record.minted {
if record.expelled.contains(&minted) {
continue;
}
let mut held: DotSet = store.get(&key).cloned().unwrap_or_default();
assert!(held.insert(minted));
let _ = store.insert(key, held);
}
store
}