Convenient way for manually writing examples

[edsko]

Writing example Commands by hand (when developing the tests, or when wanting to save particular generated tests) is a bit inconvenient. Not only does Commands capture the result of the mock implementation (and so when the model changes, we have to update our examples, if even if the commands are still the same), we also have to manually deal with references. To make this a bit more convenient, I wrote the following helper, which I find rather neat:

{-# LANGUAGE ScopedTypeVariables #-}

module Test.Util.QSM (
    Example -- opaque
  , run
  , run'
  , example
  ) where

import           Control.Monad
import           Control.Monad.Fail
import           Data.Typeable

import           Test.StateMachine.Sequential
import           Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2

data Example cmd a =
    Done a
  | Run (cmd Symbolic) ([Var] -> Example cmd a)
  | Fail String

instance Functor (Example cmd) where
  fmap = liftM

instance Applicative (Example cmd) where
  pure  = Done
  (<*>) = ap

instance Monad (Example cmd) where
  return         = pure
  Done a   >>= f = f a
  Run c k  >>= f = Run c (k >=> f)
  Fail err >>= _ = Fail err

instance MonadFail (Example cmd) where
  fail = Fail

-- | Run a command, and capture its references
run :: Typeable a => cmd Symbolic -> Example cmd [Reference a Symbolic]
run cmd = Run cmd (Done . map (Reference . Symbolic))

-- | Run a command, ignoring its references
run' :: cmd Symbolic -> Example cmd ()
run' cmd = Run cmd (\_vars -> Done ())

example :: forall model cmd m resp. Rank2.Foldable resp
        => StateMachine model cmd m resp
        -> Example cmd ()
        -> Commands cmd resp
example sm =
    Commands . fst . flip runGenSym newCounter . go (initModel sm)
  where
    go :: model Symbolic -> Example cmd () -> GenSym [Command cmd resp]
    go _ (Done ())   = return []
    go _ (Fail err)  = error $ "example: " ++ err
    go m (Run cmd k) = do
        resp <- mock sm m cmd

        let m' :: model Symbolic
            m' = transition sm m cmd resp

            vars :: [Var]
            vars = getUsedVars resp

            cmd' :: Command cmd resp
            cmd' = Command cmd resp vars

        (cmd' :) <$> go m' (k vars)

For example, I am currently working on some tests to do with threads, killing them, etc. Here are some manually written Commands:

_forkCount :: Commands (At IO Cmd) (At IO Success)
_forkCount = example sm' $ do
    run' $ At $ Fork
    run' $ At $ CountTopLevel

_forkKillCount :: Commands (At IO Cmd) (At IO Success)
_forkKillCount = example sm' $ do
    [tid] <- run $ At Fork
    run' $ At $ Kill tid
    run' $ At $ CountTopLevel

Quite nice, I think. Might be worth adding to the library?

[edsko]

Slightly better version perhaps, checking preconditions:

example :: forall model cmd m resp. (Rank2.Foldable resp, Show (cmd Symbolic))
        => StateMachine model cmd m resp
        -> Example cmd ()
        -> Commands cmd resp
example sm =
    Commands . fst . flip runGenSym newCounter . go (initModel sm)
  where
    go :: model Symbolic -> Example cmd () -> GenSym [Command cmd resp]
    go _ (Done ())   = return []
    go _ (Fail err)  = error $ "example: " ++ err
    go m (Run cmd k) = do
        case Logic.logic (precondition sm m cmd) of
          Logic.VFalse counterexample ->
            error $ "Invalid command " ++ show cmd ++ ": " ++ show counterexample
          Logic.VTrue -> do
            resp <- mock sm m cmd

            let m' :: model Symbolic
                m' = transition sm m cmd resp

                vars :: [Var]
                vars = getUsedVars resp

                cmd' :: Command cmd resp
                cmd' = Command cmd resp vars

            (cmd' :) <$> go m' (k vars)

[kderme]

+1 from me on this. I had also found it inconvenient to write manual commands.

[stevana]

Might be worth adding to the library?

Neat, sure!

[kderme]

I think Free Monad may also be used:

data ExampleF cmd a =
    Done
  | Run (cmd Symbolic) ([Var] -> a)
  | Fail String
  deriving Functor

type Example cmd = Free (ExampleF cmd)

instance MonadFail (Example cmd) where
    fail = liftF . Fail

But maybe is an overkill?

[edsko]

It would just change the example right? I don't feel very strongly about that, though personally I generally find code that doesn't use the free monad package easier to understand, and performance for these commands is not going to be critical (if your tests are slow because are generating so many commands that you need a better performing interpreter, then the interpreter is the least of your worries, I think :D ).