Is it possible for Elle to capture lost updates (phenomenon P4)?

[SungHoHong2]

Hello Jepsen Developers,

I have been testing Elle to capture the transaction anomalies with hand-written test-cases
So far, G0 ~ G2 anomalies stated in the paper are all captured.
But I'm a bit lost when I tried to implement the test-case for lost update which may not be described.
I have found in Redis-Raft that Elle is used for capturing the lost updates for Redis.
Would it be possible to have an example test case that shows Elle captures the lost-update?

[aphyr]

The lost updates in the Redis analysis manifest as divergence in the version order, which is reported as incompatible version orders in Elle--you can see examples in the case studies linked in the redis report. Elle doesn't have a precise definition of P4 (lost update) yet, so there's no anomaly called :lost-update in Elle's inferences. I'd love to do it, I just don't have a robust definition that maps to Adya's formalism yet. If you'd like to figure this out, please do--I'd like to add it. :)