axioms Subsequence for Seq[__]

automaton LossyChannel(M: type)
  signature
    input  send(m: M),
           crash
    output receive(m: M)
  states
    buffer: Seq[M] := {}
  transitions
    input send(m)
      eff buffer := buffer |- m
    input crash
      eff buffer := choose b where subsequence(b,buffer)
    output receive(m)
      pre buffer ~= {} /\ m = head(buffer)
      eff buffer := tail(buffer)