test(command): the delivery property delays, splits, repeats and replays, and covers swaps, restarts, limits and eviction (improvise-z2vr)
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
edf474d2a3
commit
bfaccae5d4
@@ -85,11 +85,15 @@ at least as new as the watermark claims, never older.
|
|||||||
not which keys sit in the client's window, and an insert or remove shifts cells into and out of it
|
not which keys sit in the client's window, and an insert or remove shifts cells into and out of it
|
||||||
without moving them. The ADR has the client re-derive positions from the axis changes and fetch what
|
without moving them. The ADR has the client re-derive positions from the axis changes and fetch what
|
||||||
it lacks. That needs ADR 008's render model, which this layer does not have. So the client records a
|
it lacks. That needs ADR 008's render model, which this layer does not have. So the client records a
|
||||||
notice that moved an axis (`restructured`), asks `Fetch { window: true }`, and the host answers with a
|
notice that moved an axis or set `flags.views` (`restructured`), asks `Fetch { window: true }`, and the host answers with a
|
||||||
`Window` body whose `carried` notice holds the axis changes, in order. This is a fetch, not a
|
`Window` body whose `carried` notice holds the axis changes, in order. This is a fetch, not a
|
||||||
correction, so the required test "a frame `[AddItem, SetCell]` ... and no client asks for a correction"
|
correction, so the required test "a frame `[AddItem, SetCell]` ... and no client asks for a correction"
|
||||||
holds: it asserts no `Ask::Correction` was sent. When the render model exists the client can narrow
|
holds: it asserts no `Ask::Correction` was sent. When the render model exists the client can narrow
|
||||||
the fetch to the cells that entered its window.
|
the fetch to the cells that entered its window (improvise-bw4p.9).
|
||||||
|
|
||||||
|
A view command (`SetAxis`, `TransposeAxes`, a page selection, a hide) moves positions and no key, and
|
||||||
|
reaches the client only as `flags.views`. So that flag counts as an axis change on both sides: the client
|
||||||
|
fetches its window, and the host answers a correction over a range holding the flag with a window body.
|
||||||
|
|
||||||
## 4. The client
|
## 4. The client
|
||||||
|
|
||||||
@@ -106,6 +110,14 @@ body is a gap unless it starts at or below the watermark. Otherwise `held += tar
|
|||||||
watermark becomes `through`, and the queued notices it covers are dropped. A late reply older than
|
watermark becomes `through`, and the queued notices it covers are dropped. A late reply older than
|
||||||
the watermark therefore cannot regress the state, which is what makes a retry safe.
|
the watermark therefore cannot regress the state, which is what makes a retry safe.
|
||||||
|
|
||||||
|
**A correction from an older generation of the same host is a duplicate, whatever the watermark.** Epochs
|
||||||
|
of different hosts are not ordered, so a late reply from a dead host is told apart only by being
|
||||||
|
covered: a duplicate answer prunes every queued entry from another epoch and moves `seen` onto the live
|
||||||
|
epoch, so a late notice from a dead host costs one extra round and cannot livelock `sync`.
|
||||||
|
|
||||||
|
`poll` hands a pulled notice only to the shape it asked about. A notice carries only that shape's keys,
|
||||||
|
and applying it to another tracked shape would advance that shape past keys it never saw.
|
||||||
|
|
||||||
`connection_lost`, `request_failed` and `unreadable` set `stale`, which `wants` turns into
|
`connection_lost`, `request_failed` and `unreadable` set `stale`, which `wants` turns into
|
||||||
`Ask::Correction` from the watermark the client held. A duplicate whose `through` equals the watermark
|
`Ask::Correction` from the watermark the client held. A duplicate whose `through` equals the watermark
|
||||||
also clears `stale`: the host has said there is nothing newer.
|
also clears `stale`: the host has said there is nothing newer.
|
||||||
@@ -142,8 +154,8 @@ each `Command::Model` that lands, and `Host::deliver` answers a `Request`.
|
|||||||
and never the workbook. A value a failed command wrote is not in it.
|
and never the workbook. A value a failed command wrote is not in it.
|
||||||
|
|
||||||
**Rollback.** `Host::mutating_frame` clones the `Delivery` beside the app snapshot and the session
|
**Rollback.** `Host::mutating_frame` clones the `Delivery` beside the app snapshot and the session
|
||||||
mirrors, and `undo_frame` puts it back. The clone is cheap (`Arc` for outputs, notices and structure,
|
mirrors, and `undo_frame` puts it back. The clone is cheap: `Arc` for outputs, notices and structure,
|
||||||
bounded by the log's capacity). So a refused frame consumes no publication number and publishes nothing.
|
and both the log and the outbox hold at most `capacity` notices. So a refused frame consumes no publication number and publishes nothing.
|
||||||
|
|
||||||
**The ADR and ADR 001 disagree here, and ADR 001 wins until ADR 006 exists.** Clause 9 says a frame
|
**The ADR and ADR 001 disagree here, and ADR 001 wins until ADR 006 exists.** Clause 9 says a frame
|
||||||
whose later command fails keeps its earlier commands and their notices, "each command commits on its own
|
whose later command fails keeps its earlier commands and their notices, "each command commits on its own
|
||||||
@@ -151,12 +163,22 @@ whose later command fails keeps its earlier commands and their notices, "each co
|
|||||||
not in the tree. The required test "a refused command consumes no publication number, and the commands
|
not in the tree. The required test "a refused command consumes no publication number, and the commands
|
||||||
before it in its frame stay published" is split in two. The first half is tested. The second is
|
before it in its frame stay published" is split in two. The first half is tested. The second is
|
||||||
tested as its opposite, `commands_before_a_refused_one_are_rolled_back_with_their_notices_under_adr_001`,
|
tested as its opposite, `commands_before_a_refused_one_are_rolled_back_with_their_notices_under_adr_001`,
|
||||||
which is the test to flip when per-command commit lands: the publisher already supports it, since it
|
which is the test to flip when per-command commit lands (improvise-bw4p.8): the publisher already supports it, since it
|
||||||
publishes whatever the host tells it committed.
|
publishes whatever the host tells it committed.
|
||||||
|
|
||||||
|
**Nothing is published while nobody can hear it.** With no live shape and no attached transport
|
||||||
|
(`Host::attach_notices`), a commit only advances the publication number: no structure is read, nothing is
|
||||||
|
diffed, the log is cleared and the queued structure is forgotten. A shape that goes live, or a transport
|
||||||
|
that attaches, re-reads the structure, so its first diff is against a known state. Without this every
|
||||||
|
host pays for delivery on every command while nothing consumes it. The outbox exists only while a
|
||||||
|
transport is attached, and keeps the newest `capacity` notices; a transport that falls behind sees a gap
|
||||||
|
and asks for a correction. The axis diff is linear in the items (`diff_items`, set lookups), and its test
|
||||||
|
counts comparisons on a counting item type rather than reading a clock.
|
||||||
|
|
||||||
**The host instance** is a random id, never a time (`Host::new` takes one from `RandomState`).
|
**The host instance** is a random id, never a time (`Host::new` takes one from `RandomState`).
|
||||||
`RandomState` has no entropy on `wasm32-unknown-unknown`, so a worker must pass a real one through
|
`RandomState` has no entropy on `wasm32-unknown-unknown`, so a worker must pass a real one through
|
||||||
`Host::with_instance`. A restarted host with the same id would accept a stale watermark as current.
|
`Host::with_instance`. A restarted host with the same id would accept a stale watermark as current.
|
||||||
|
`Worker` still calls `Host::new` (improvise-bw4p.7).
|
||||||
|
|
||||||
**Eviction** (`evict_idle`) takes a local count and an idle length in the same unit, never a wall clock
|
**Eviction** (`evict_idle`) takes a local count and an idle length in the same unit, never a wall clock
|
||||||
compared across machines. An evicted key is announced in the next notice and forgotten; naming it again
|
compared across machines. An evicted key is announced in the next notice and forgotten; naming it again
|
||||||
@@ -185,13 +207,16 @@ The token in a request is carried and echoed by the client and never read by the
|
|||||||
function call; `WireEdge` passes request and reply through JSON text, the adapter at a wire boundary,
|
function call; `WireEdge` passes request and reply through JSON text, the adapter at a wire boundary,
|
||||||
so the lossless properties are exercised by every test that uses it. Neither adds a `ClientFrame` or
|
so the lossless properties are exercised by every test that uses it. Neither adds a `ClientFrame` or
|
||||||
`ServerFrame` variant: the page does not read notices yet, and adding the frames means changing the
|
`ServerFrame` variant: the page does not read notices yet, and adding the frames means changing the
|
||||||
browser and the worker together (ADR 008 replaces `Projection`). A transport pushes
|
browser and the worker together (ADR 008 replaces `Projection`; improvise-bw4p.10). A transport
|
||||||
`Host::take_notices()`.
|
pushes `Host::take_notices()`.
|
||||||
|
|
||||||
## Not done, and why
|
## Not done, and why
|
||||||
|
|
||||||
- **The notices are not sent by the socket or worker hosts.** They need frame variants and the page
|
- **The notices are not sent by the socket or worker hosts.** They need frame variants and the page
|
||||||
(above).
|
(above).
|
||||||
|
- **Positions and column totals are not on the wire.** A correction carries `(key, value)` and no row or
|
||||||
|
column, and `Output` holds body cells only. The ADR attaches the position when output is sent and lists
|
||||||
|
totals among the moved keys. Both need the render model and the totals' own keys (ADR 008, clause 10).
|
||||||
- **A twin at the serving end** (a server-side watermark or filter) is not built; the ADR allows it and
|
- **A twin at the serving end** (a server-side watermark or filter) is not built; the ADR allows it and
|
||||||
does not require it.
|
does not require it.
|
||||||
- **A pushed filter** is the client's `window`, applied on every request.
|
- **A pushed filter** is the client's `window`, applied on every request.
|
||||||
|
|||||||
@@ -93,3 +93,58 @@ token and that watermark.
|
|||||||
|
|
||||||
A one-cell window, a remove that moves South into it. The notice lists only North, so a client that
|
A one-cell window, a remove that moves South into it. The notice lists only North, so a client that
|
||||||
fetches moved keys alone ends with an empty window.
|
fetches moved keys alone ends with an empty window.
|
||||||
|
|
||||||
|
## Review of #348, round one
|
||||||
|
|
||||||
|
Each test below was written against the behaviour the review reported and failed before its fix, or, for
|
||||||
|
the cost tests, was run against a quadratic rival.
|
||||||
|
|
||||||
|
### diffing_a_category_compares_each_item_a_bounded_number_of_times
|
||||||
|
|
||||||
|
Items are a type whose `eq` is counted. Rival: `contains` on the slices in `diff_items`, which makes the
|
||||||
|
count quadratic and fails every size. A wall-clock test would have passed on a fast machine.
|
||||||
|
|
||||||
|
### a_commit_with_nothing_live_and_no_transport_reads_nothing
|
||||||
|
|
||||||
|
Counts `Structure::of` calls. Rival: the idle skip removed.
|
||||||
|
|
||||||
|
### the_outbox_and_the_clone_a_frame_takes_are_bounded
|
||||||
|
|
||||||
|
Rival: the outbox truncation removed, so twenty commits leave twenty queued.
|
||||||
|
|
||||||
|
### a_late_window_reply_from_an_older_generation_does_not_regress
|
||||||
|
|
||||||
|
Rival: the older-generation guard disabled (fails this test in the protocol crate).
|
||||||
|
|
||||||
|
### a_late_notice_from_a_dead_host_settles_against_the_live_one
|
||||||
|
|
||||||
|
Rival: the duplicate arm no longer prunes other epochs' entries; the random property also fails.
|
||||||
|
|
||||||
|
### a_poll_for_one_shape_leaves_the_other_shapes_alone
|
||||||
|
|
||||||
|
Rival: pulled notices applied to every shape.
|
||||||
|
|
||||||
|
### a_transpose_empties_a_partial_window_of_the_cell_that_left_it
|
||||||
|
|
||||||
|
A transpose moves no key. Rival: `flags.views` not counted as a structural change in the client and the
|
||||||
|
host. `a_dropped_views_notice_is_answered_with_the_window_not_an_empty_key_list` fails with the host
|
||||||
|
alone changed.
|
||||||
|
|
||||||
|
### wide_integers_are_canonical_on_input
|
||||||
|
|
||||||
|
Both spellings are refused outside their range: a JSON number at or above 2^53, a string below it, a
|
||||||
|
sign, leading zeros and trailing space.
|
||||||
|
|
||||||
|
### an_item_insert_position_crosses_as_a_wide_integer
|
||||||
|
|
||||||
|
`ItemInserted.at` is a `u128` through `wide`.
|
||||||
|
|
||||||
|
### a_fetch_covers_only_the_notices_it_named_when_a_later_commit_is_already_in_the_state
|
||||||
|
|
||||||
|
Rival: a fetch answered with `through: at`. The first version of the random property did not catch it (it
|
||||||
|
delivered each notice before the next commit); the property now splits, delays, duplicates and replays
|
||||||
|
notices and old replies, and fails the rival on every run, which this test also does by name.
|
||||||
|
|
||||||
|
### equal_values_compare_equal_whatever_the_zero_counts_say
|
||||||
|
|
||||||
|
`ExactSum`'s equality compared the sign-of-zero counters even when the total was nonzero.
|
||||||
|
|||||||
@@ -152,6 +152,7 @@ struct Flaky<'a> {
|
|||||||
host: &'a mut Host,
|
host: &'a mut Host,
|
||||||
script: VecDeque<Option<Fault>>,
|
script: VecDeque<Option<Fault>>,
|
||||||
reached: Vec<Request>,
|
reached: Vec<Request>,
|
||||||
|
replies: Vec<Reply>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<'a> Flaky<'a> {
|
impl<'a> Flaky<'a> {
|
||||||
@@ -160,6 +161,7 @@ impl<'a> Flaky<'a> {
|
|||||||
host,
|
host,
|
||||||
script: VecDeque::new(),
|
script: VecDeque::new(),
|
||||||
reached: Vec::new(),
|
reached: Vec::new(),
|
||||||
|
replies: Vec::new(),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -179,6 +181,7 @@ impl Edge for Flaky<'_> {
|
|||||||
}
|
}
|
||||||
self.reached.push(request.clone());
|
self.reached.push(request.clone());
|
||||||
let reply = self.host.deliver(&request, 0);
|
let reply = self.host.deliver(&request, 0);
|
||||||
|
self.replies.push(reply.clone());
|
||||||
match fault {
|
match fault {
|
||||||
Some(Fault::DropReply) => Err(EdgeError::Failed),
|
Some(Fault::DropReply) => Err(EdgeError::Failed),
|
||||||
Some(Fault::Garble) => Err(EdgeError::Unreadable),
|
Some(Fault::Garble) => Err(EdgeError::Unreadable),
|
||||||
@@ -1034,6 +1037,28 @@ fn a_dropped_views_notice_is_answered_with_the_window_not_an_empty_key_list() {
|
|||||||
assert_eq!(client.held(&shape()), Some(&drawn(&host, &south_window())));
|
assert_eq!(client.held(&shape()), Some(&drawn(&host, &south_window())));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
fn a_fetch_covers_only_the_notices_it_named_when_a_later_commit_is_already_in_the_state() {
|
||||||
|
let mut host = host();
|
||||||
|
let id = connect(&mut host);
|
||||||
|
let mut client = settled(&mut host);
|
||||||
|
host.take_notices();
|
||||||
|
send(&mut host, id, vec![set("North", 1.0)]);
|
||||||
|
send(&mut host, id, vec![set("South", 2.0)]);
|
||||||
|
let notices = host.take_notices();
|
||||||
|
deliver_all(&mut client, ¬ices[..1]);
|
||||||
|
let mut edge = Flaky::new(&mut host);
|
||||||
|
client.sync(&mut edge, &shape(), 6);
|
||||||
|
assert_eq!(
|
||||||
|
client.watermark(&shape()),
|
||||||
|
Some(notices[0].stamp()),
|
||||||
|
"through, not at"
|
||||||
|
);
|
||||||
|
deliver_all(&mut client, ¬ices[1..]);
|
||||||
|
client.sync(&mut Flaky::new(&mut host), &shape(), 6);
|
||||||
|
held_equals_drawn(&client, &host);
|
||||||
|
}
|
||||||
|
|
||||||
// ── the whole thing, at random ─────────────────────────────────────────────
|
// ── the whole thing, at random ─────────────────────────────────────────────
|
||||||
|
|
||||||
mod random {
|
mod random {
|
||||||
@@ -1044,17 +1069,31 @@ mod random {
|
|||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
enum Op {
|
enum Op {
|
||||||
Set(bool, usize),
|
Set(bool, usize),
|
||||||
|
Both(usize, usize),
|
||||||
|
Clear(bool),
|
||||||
Add(usize),
|
Add(usize),
|
||||||
Remove(usize),
|
Remove(usize),
|
||||||
Formula,
|
Formula,
|
||||||
|
Transpose,
|
||||||
|
TightLimits,
|
||||||
|
Evict,
|
||||||
|
Swap,
|
||||||
|
Restart,
|
||||||
}
|
}
|
||||||
|
|
||||||
fn op() -> impl Strategy<Value = Op> {
|
fn op() -> impl Strategy<Value = Op> {
|
||||||
prop_oneof![
|
prop_oneof![
|
||||||
4 => (any::<bool>(), 0usize..8).prop_map(|(r, v)| Op::Set(r, v)),
|
6 => (any::<bool>(), 0usize..8).prop_map(|(r, v)| Op::Set(r, v)),
|
||||||
2 => (0usize..3).prop_map(Op::Add),
|
4 => (0usize..8, 0usize..8).prop_map(|(a, b)| Op::Both(a, b)),
|
||||||
1 => (0usize..3).prop_map(Op::Remove),
|
2 => any::<bool>().prop_map(Op::Clear),
|
||||||
|
3 => (0usize..3).prop_map(Op::Add),
|
||||||
|
2 => (0usize..3).prop_map(Op::Remove),
|
||||||
1 => Just(Op::Formula),
|
1 => Just(Op::Formula),
|
||||||
|
1 => Just(Op::Transpose),
|
||||||
|
1 => Just(Op::TightLimits),
|
||||||
|
1 => Just(Op::Evict),
|
||||||
|
1 => Just(Op::Swap),
|
||||||
|
1 => Just(Op::Restart),
|
||||||
]
|
]
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1070,9 +1109,25 @@ mod random {
|
|||||||
];
|
];
|
||||||
const EXTRA: [&str; 3] = ["East", "West", "North"];
|
const EXTRA: [&str; 3] = ["East", "West", "North"];
|
||||||
|
|
||||||
fn command(op: &Op) -> ModelCommand {
|
fn region(north: bool) -> &'static str {
|
||||||
|
["South", "North"][north as usize]
|
||||||
|
}
|
||||||
|
|
||||||
|
fn commands(op: &Op) -> Vec<ModelCommand> {
|
||||||
match op {
|
match op {
|
||||||
Op::Set(north, v) => set(["South", "North"][*north as usize], VALUES[*v]),
|
Op::Both(a, b) => vec![set("North", VALUES[*a]), set("South", VALUES[*b])],
|
||||||
|
other => command(other).into_iter().collect(),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn command(op: &Op) -> Option<ModelCommand> {
|
||||||
|
Some(match op {
|
||||||
|
Op::Both(..) => return None,
|
||||||
|
Op::Set(north, v) => set(region(*north), VALUES[*v]),
|
||||||
|
Op::Clear(north) => ModelCommand::ClearCell {
|
||||||
|
view: "Default".into(),
|
||||||
|
cell: record(region(*north)),
|
||||||
|
},
|
||||||
Op::Add(i) => add_item(EXTRA[*i]),
|
Op::Add(i) => add_item(EXTRA[*i]),
|
||||||
Op::Remove(i) => ModelCommand::RemoveItem {
|
Op::Remove(i) => ModelCommand::RemoveItem {
|
||||||
category: "Region".into(),
|
category: "Region".into(),
|
||||||
@@ -1082,26 +1137,49 @@ mod random {
|
|||||||
raw: "Double = Revenue * 2".into(),
|
raw: "Double = Revenue * 2".into(),
|
||||||
target_category: "_Measure".into(),
|
target_category: "_Measure".into(),
|
||||||
},
|
},
|
||||||
}
|
Op::Transpose => transpose(),
|
||||||
|
Op::Swap => ModelCommand::LoadModel("other.improv".into()),
|
||||||
|
Op::TightLimits | Op::Evict | Op::Restart => return None,
|
||||||
|
})
|
||||||
|
}
|
||||||
|
|
||||||
|
/// How a step's notices reach the client.
|
||||||
|
#[derive(Debug, Clone, Copy)]
|
||||||
|
enum Arrival {
|
||||||
|
Dropped,
|
||||||
|
Now,
|
||||||
|
Twice,
|
||||||
|
Split,
|
||||||
|
Late(usize),
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
struct Weather {
|
struct Weather {
|
||||||
deliver_notice: bool,
|
arrival: Arrival,
|
||||||
lose_connection: bool,
|
lose_connection: bool,
|
||||||
sync: Vec<Option<u8>>,
|
sync: Vec<Option<u8>>,
|
||||||
|
replay: Option<usize>,
|
||||||
}
|
}
|
||||||
|
|
||||||
fn weather() -> impl Strategy<Value = Weather> {
|
fn weather() -> impl Strategy<Value = Weather> {
|
||||||
|
let arrival = prop_oneof![
|
||||||
|
2 => Just(Arrival::Dropped),
|
||||||
|
4 => Just(Arrival::Now),
|
||||||
|
1 => Just(Arrival::Twice),
|
||||||
|
4 => Just(Arrival::Split),
|
||||||
|
3 => (1usize..4).prop_map(Arrival::Late),
|
||||||
|
];
|
||||||
(
|
(
|
||||||
any::<bool>(),
|
arrival,
|
||||||
0u8..8,
|
0u8..8,
|
||||||
proptest::collection::vec(proptest::option::of(0u8..3), 0..3),
|
proptest::collection::vec(proptest::option::of(0u8..3), 0..3),
|
||||||
|
proptest::option::of(0usize..16),
|
||||||
)
|
)
|
||||||
.prop_map(|(deliver_notice, lose, sync)| Weather {
|
.prop_map(|(arrival, lose, sync, replay)| Weather {
|
||||||
deliver_notice,
|
arrival,
|
||||||
lose_connection: lose == 0,
|
lose_connection: lose == 0,
|
||||||
sync,
|
sync,
|
||||||
|
replay,
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -1118,32 +1196,102 @@ mod random {
|
|||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// A host over `wb` that can load a second document, as a restarted host would be.
|
||||||
|
fn host_over(wb: Workbook, instance: u64) -> Host {
|
||||||
|
let storage = crate::storage::MemoryFs::new();
|
||||||
|
let mut other = Workbook::new("Other");
|
||||||
|
other.add_category("Product").unwrap();
|
||||||
|
other.add_item("Product", "Widget").unwrap();
|
||||||
|
other.add_item("_Measure", "Units").unwrap();
|
||||||
|
other.active_view_mut().set_axis("Product", Axis::Row);
|
||||||
|
other.active_view_mut().set_axis("_Measure", Axis::Column);
|
||||||
|
crate::persistence::save_to(&storage, &other, std::path::Path::new("other.improv"))
|
||||||
|
.unwrap();
|
||||||
|
let mut app = App::new(wb, None);
|
||||||
|
app.storage = Box::new(storage);
|
||||||
|
app.rebuild_layout();
|
||||||
|
let mut host = Host::with_instance(app, instance);
|
||||||
|
host.attach_notices();
|
||||||
|
host
|
||||||
|
}
|
||||||
|
|
||||||
|
fn arrive(
|
||||||
|
client: &mut EdgeClient,
|
||||||
|
held_back: &mut Vec<(usize, Notice)>,
|
||||||
|
step: usize,
|
||||||
|
w: &Weather,
|
||||||
|
fresh: Vec<Notice>,
|
||||||
|
) {
|
||||||
|
for (i, n) in fresh.into_iter().enumerate() {
|
||||||
|
match w.arrival {
|
||||||
|
Arrival::Split if i == 0 => deliver_all(client, &[n]),
|
||||||
|
Arrival::Split => held_back.push((step + 1, n)),
|
||||||
|
Arrival::Dropped => {}
|
||||||
|
Arrival::Now => deliver_all(client, &[n]),
|
||||||
|
Arrival::Twice => deliver_all(client, &[n.clone(), n]),
|
||||||
|
Arrival::Late(k) => held_back.push((step + k, n)),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
let (due, later): (Vec<_>, Vec<_>) = held_back.drain(..).partition(|(at, _)| *at <= step);
|
||||||
|
*held_back = later;
|
||||||
|
let notices: Vec<Notice> = due.into_iter().map(|(_, n)| n).collect();
|
||||||
|
deliver_all(client, ¬ices);
|
||||||
|
}
|
||||||
|
|
||||||
proptest! {
|
proptest! {
|
||||||
#[test]
|
#[test]
|
||||||
fn a_corrected_state_is_the_target_and_correcting_it_again_is_the_zero_zset(
|
fn a_corrected_state_is_the_target_and_correcting_it_again_is_the_zero_zset(
|
||||||
steps in proptest::collection::vec((op(), weather()), 1..12),
|
steps in proptest::collection::vec((op(), weather()), 1..12),
|
||||||
window in windows(),
|
window in windows(),
|
||||||
) {
|
) {
|
||||||
let mut host = host();
|
let mut instance = 1;
|
||||||
let id = connect(&mut host);
|
let mut host = host_over(workbook(), instance);
|
||||||
|
let mut id = connect(&mut host);
|
||||||
let mut client = EdgeClient::new(session());
|
let mut client = EdgeClient::new(session());
|
||||||
client.track(shape(), window);
|
client.track(shape(), window);
|
||||||
client.sync(&mut Flaky::new(&mut host), &shape(), 6);
|
client.sync(&mut Flaky::new(&mut host), &shape(), 6);
|
||||||
host.take_notices();
|
host.take_notices();
|
||||||
|
let mut held_back: Vec<(usize, Notice)> = Vec::new();
|
||||||
|
let mut old: Vec<Reply> = Vec::new();
|
||||||
|
|
||||||
for (op, weather) in &steps {
|
for (step, (op, weather)) in steps.iter().enumerate() {
|
||||||
send(&mut host, id, vec![command(op)]);
|
match (commands(op), op) {
|
||||||
let notices = host.take_notices();
|
(cmds, _) if !cmds.is_empty() => {
|
||||||
if weather.deliver_notice {
|
send(&mut host, id, cmds);
|
||||||
deliver_all(&mut client, ¬ices);
|
}
|
||||||
|
(_, Op::TightLimits) => host.limit_delivery(2, 1),
|
||||||
|
(_, Op::Evict) => {
|
||||||
|
host.evict_idle(10, 0);
|
||||||
|
}
|
||||||
|
_ => {
|
||||||
|
instance += 1;
|
||||||
|
let wb = host.app().model_state.workbook.clone();
|
||||||
|
host = host_over(wb, instance);
|
||||||
|
id = connect(&mut host);
|
||||||
|
held_back.clear();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
let fresh = host.take_notices();
|
||||||
|
arrive(&mut client, &mut held_back, step, weather, fresh);
|
||||||
if weather.lose_connection {
|
if weather.lose_connection {
|
||||||
client.connection_lost();
|
client.connection_lost();
|
||||||
}
|
}
|
||||||
|
if let Some(i) = weather.replay.filter(|_| !old.is_empty()) {
|
||||||
|
match &old[i % old.len()] {
|
||||||
|
Reply::Correction(c) => {
|
||||||
|
client.apply(c);
|
||||||
|
}
|
||||||
|
Reply::Notices(list) => deliver_all(&mut client, list),
|
||||||
|
}
|
||||||
|
}
|
||||||
let script = weather.sync.iter().map(|f| f.map(fault)).collect();
|
let script = weather.sync.iter().map(|f| f.map(fault)).collect();
|
||||||
client.sync(&mut Flaky::scripted(&mut host, script), &shape(), 6);
|
let mut edge = Flaky::scripted(&mut host, script);
|
||||||
|
client.sync(&mut edge, &shape(), 6);
|
||||||
|
old.append(&mut edge.replies);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
let rest: Vec<Notice> = held_back.drain(..).map(|(_, n)| n).collect();
|
||||||
|
deliver_all(&mut client, &rest);
|
||||||
let (state, _) = client.poll(&mut WireEdge(Flaky::new(&mut host)), &shape());
|
let (state, _) = client.poll(&mut WireEdge(Flaky::new(&mut host)), &shape());
|
||||||
prop_assert_eq!(state, Synced::Settled);
|
prop_assert_eq!(state, Synced::Settled);
|
||||||
let want = drawn(&host, &window);
|
let want = drawn(&host, &window);
|
||||||
|
|||||||
Reference in New Issue
Block a user