Testing Distributed Systems

// property-based tests with fast-check: the CRDT merge and an idempotent ledger apply
import fc from 'fast-check';

const counter = fc.dictionary(fc.constantFrom('A', 'B', 'C'), fc.nat(100));
test('G-counter merge is commutative, associative and idempotent', () => {
  fc.assert(fc.property(counter, counter, counter, (a, b, c) => {
    expect(mergeG(a, b)).toEqual(mergeG(b, a));
    expect(mergeG(mergeG(a, b), c)).toEqual(mergeG(a, mergeG(b, c)));
    expect(mergeG(a, a)).toEqual(a);
  }));
});

const transfer = fc.record({ key: fc.uuid(), amount: fc.integer({ min: 1, max: 10_000 }) });
test('applying a log twice gives the same balances', () => {
  fc.assert(fc.property(fc.array(transfer), log => {
    const once = applyAll(new Ledger(), log);
    const twice = applyAll(applyAll(new Ledger(), log), log);             // retries, redeliveries
    expect(twice.balances()).toEqual(once.balances());
  }));
});

\* a fragment of TLA+: an invariant the model checker tries to break
TypeOK      == leader \in [Terms -> Nodes \cup {None}]
OneLeader   == \A t \in Terms : Cardinality({n \in Nodes : role[n] = "leader" /\ term[n] = t}) <= 1
Conserved   == Sum(balance) = InitialTotal