advancedtelematic/quickcheck-state-machine

Testing asynchronous APIs

stevana opened this issue · 3 comments

stevana commented

Work in progress.

Consider the following example, a simple server that when sent a number
replies by sending the sum of all numbers it has been sent so far (asynchronously,
say on a message bus).

data Action v :: * -> * where
  Add :: Int -> Action v ()
  Sum :: Action v Int

Model = Int

next m (Add i) = m + i
next m Sum     = m

post m (Add i) _ = True
post m Sum     i = i == m

So far so good, but what is the semantics for Sum?

sem (Add i) = apiCallToEndpoint i server
sem Sum     = ?

It doesn't really make sense, the Sum action is created by the
environment (message bus).

Here's an idea, don't generate Sum actions. Instead let the user
provide a function:

environmentEvents :: TChan History -> IO ()

That has access to the history channel, and can listen to the bus and
add Sum events. It's important that the user adds a InvocationEvent
for Sum immediately after it sees a ResponseEvent for Add on the
channel -- otherwise linearisation might fail, e.g.:

|--- Add 1 ---| |--- Add 2 ---|
                                 |-- Sum 1 --|

The ResponseEvent for Sum should be added when the actual message
appears on the message bus.

One clear downside of this approach is that it exposes an implementation
detail, the history channel, to the user. I'm also not sure what to do
about pids (we can't/shouldn't have multiple pending invocations on the
same pid -- that would break sequentiality of the thread).

stevana commented

One way to hide the history channel from the user, could be to have the user provide a function that triggers invocation events:

triggers :: action Concrete resp -> Maybe (exists resp'. action Concrete resp')

And another function that creates response events:

environmentResponses :: Producer IO (Constructor, Dynamic)

In the above example the implementations of these would be something like:

triggers (Add i) = Just Sum
triggers Sum    = Nothing

environmentResponses = do
  msg <- readMessageFromBus
  case msg of
    'S' : 'u' : 'm' : ' ' : n : [] -> yield (Constructor "Sum", toDyn (read n :: Int))
    _ -> environmentResponses
stevana commented

I still think this is an interesting topic, but I'm not working on this actively.

If I would revisit it, then I would try to combine what I've learned from https://github.com/advancedtelematic/quickcheck-state-machine-distributed and the literature on behavioral programming.