Event as defined in Labelling is misleading

[edsko]

Module Test.StateMachine.Labelling defines

data Event model cmd resp (r :: Type -> Type) = Event
  { eventBefore :: model r
  , eventCmd    :: cmd   r
  , eventAfter  :: model r
  , eventResp   :: resp  r
  }
  deriving stock Show

While this is not wrong in that module, it is misleading and rather dangerous. This type is based on,and almost equal to the one I define in my blog post, but not quite. Compare to the Event type defined in Test.StateMachine.Lockstep.NAry:

data Event t r = Event {
      before   :: Model t    r
    , cmd      :: Cmd   t :@ r
    , after    :: Model t    r
    , mockResp :: Resp t (MockHandle t) (RealHandles t)
    }

This records the mock response, not the real one. This is critical: if this records the real response, and then the rest of my blog post is used as is, then the postcondition becomes trivial, comparing the real response to itself.

[stevana]

Hmm, yeah I can see that being problematic.

I don't remember why I did it like I did (perhaps I misunderstood your code?), and I'm not actively using that code anymore today, so I guess maybe the right thing is to simply remove it?