-- Reverse is involutive
propReverse :: Property
propReverse =
  property $ do
    xs <- forAll $ Gen.list (Range.linear 0 100) Gen.alpha
    reverse (reverse xs) === xs

What about testing the properties of a whole system?

• Retrieved data matches submitted data.
• Uniqueness constraints.
• Users only see what they’re supposed to.

State machine testing!

The Plan

• State machines
• Property based testing for state machines
• Examples

What else can be modelled as a state machine?

• Games
• Routing
• Web applications

Web app state machine

Keeps track of game scores and player ratings.

API

Properties

• Can only register-first once
• Player count matches number of successful registrations
• Retrieving a player matches what was POSTed

Big picture

• Use a state machine to model an app.
• Randomly generate inputs.
• Execute inputs against the app.
• Update the model.
• Check that the model agrees with reality.

State

data LeaderboardState (v :: * -> *) =
  LeaderboardState Bool

Inputs

data PlayerCount (v :: * -> *) =
  PlayerCount
  
data RegisterFirst (v :: * -> *) =
  RegisterFirst Registration

data Register (v :: * -> *) =
  Register AdminToken Registration

Initial state

initialState :: LeaderboardState v
initialState = LeaderboardState False

Something to consider

All inputs are generated before execution.

All inputs are generated before execution.

token1 <- RegisterFirst registration1

All inputs are generated before execution.

token1 <- RegisterFirst registration1
token2 <- Register token1 registration2

Solution

data Var a v

Solution

data Var a v

Var a Symbolic
Var a Concrete

Solution

data Var a v

Var a Symbolic
Var a Concrete

Symbolic :: * -> *
Concrete :: * -> *

Commands

Bundle together:

• Generation of an input.
• Execution of an input.
• Preconditions.
• State updates.
• Postconditions / assertions.

data Command n m state =
  forall input output.
  Command {








  }

data Command n m state =
  forall input output.
  Command {
    commandGen ::
      state Symbolic -> Maybe (n (input Symbolic))






  }

data Command n m state =
  forall input output.
  Command {
    commandGen ::
      state Symbolic -> Maybe (n (input Symbolic))

  , commandExecute ::
      input Concrete -> m output



  }

data Command n m state =
  forall input output.
  Command {
    commandGen ::
      state Symbolic -> Maybe (n (input Symbolic))

  , commandExecute ::
      input Concrete -> m output

  , commandCallbacks ::
      [Callback input output state]
  }

data Callback input output state =
    Require ( state Symbolic
              -> input Symbolic
              -> Bool)

data Callback input output state =
    Require ( state Symbolic
              -> input Symbolic
              -> Bool)
  | Update ( forall v. Ord1 v
             => state v
             -> input v
             -> Var output v
             -> state v)

data Callback input output state =
    Require ( state Symbolic
              -> input Symbolic
              -> Bool)
  | Update ( forall v. Ord1 v
             => state v
             -> input v
             -> Var output v
             -> state v)
  | Ensure ( state Concrete
             -> state Concrete
             -> input Concrete
             -> output
             -> Test ())

HTraversable

class HTraversable t where
  htraverse
    :: Applicative f
    => (forall a. g a -> f (h a)) -> t g -> f (t h)

(            a -> f b    ) -> t a -> f (t b)

(forall a. g a -> f (h a)) -> t g -> f (t h)

htraverse
  :: (forall a. Symbolic a -> Either e (Concrete a))
  -> t Symbolic
  -> Either e (t Concrete)

data PlayerCount (v :: * -> *) =
  PlayerCount
  
data RegisterFirst (v :: * -> *) =
  RegisterFirst Registration

data Register (v :: * -> *) =
  Register AdminToken Registration

Property:

Registering our first player only succeeds once

State

newtype SimpleState (v :: * -> *) =
  SimpleState Bool

Inputs

newtype RegFirst (v :: * -> *) =
    RegFirst RegisterPlayer
  deriving (Eq, Show)

Inputs

newtype RegFirst (v :: * -> *) =
    RegFirst RegisterPlayer
  deriving (Eq, Show)

newtype RegFirstForbidden (v :: * -> *) =
  RegFirstForbidden RegisterPlayer
  deriving (Eq, Show)

cRegisterFirst

cRegisterFirst
  :: ( MonadGen n
     , MonadIO m
     , MonadTest m
     )
  => ClientEnv
  -> Command n m SimpleState
cRegisterFirst env =
  Command cRegisterFirstGen
          (cRegisterFirstExe env)
          cRegisterFirstCallbacks

cRegisterFirstGen
  :: MonadGen n
  => SimpleState Symbolic
  -> Maybe (n (RegFirst Symbolic))

cRegisterFirstGen
  :: MonadGen n
  => SimpleState Symbolic
  -> Maybe (n (RegFirst Symbolic))
cRegisterFirstGen (SimpleState registeredFirst) =
  if registeredFirst
  then Nothing
  else Just (RegFirst <$> genRegPlayerRandomAdmin)

cRegisterFirstExe
  :: ( MonadIO m
     , MonadTest m
     )
  => ClientEnv
  -> RegFirst Concrete
  -> m ResponsePlayer

cRegisterFirstExe
  :: ( MonadIO m
     , MonadTest m
     )
  => ClientEnv
  -> RegFirst Concrete
  -> m ResponsePlayer
cRegisterFirstExe env (RegFirst rp) =
  evalEither =<< successClient env (registerFirst rp)

successClient
  :: MonadIO m
  => ClientEnv -> ClientM a -> m (Either ServantError a)

evalEither
  :: (MonadTest m, Show x, HasCallStack)
  => Either x a -> m a

  evalEither =<< successClient env (registerFirst rp)

cRegisterFirstCallbacks
  :: [Callback RegFirst ResponsePlayer SimpleState]

cRegisterFirstCallbacks
  :: [Callback RegFirst ResponsePlayer SimpleState]
cRegisterFirstCallbacks =
  [ Require $ \(SimpleState registeredFirst) _i ->
      not registeredFirst







  ]

cRegisterFirstCallbacks
  :: [Callback RegFirst ResponsePlayer SimpleState]
cRegisterFirstCallbacks =
  [ Require $ \(SimpleState registeredFirst) _i ->
      not registeredFirst
  , Update $ \_sOld _i _o -> SimpleState True






  ]

cRegisterFirstCallbacks
  :: [Callback RegFirst ResponsePlayer SimpleState]
cRegisterFirstCallbacks =
  [ Require $ \(SimpleState registeredFirst) _i ->
      not registeredFirst
  , Update $ \_sOld _i _o -> SimpleState True
  , Ensure $ \_sOld _sNew _input out ->
      case out of
        (ResponsePlayer (LS.PlayerId (Auto mId))
                        (Token token)) -> do
          assert $ not (BS.null t)
          assert $ maybe False (>= 0) mId
  ]

cRegisterFirstForbidden

cRegisterFirstForbiddenGen
  :: MonadGen n
  => SimpleState Symbolic
  -> Maybe (n (RegFirstForbidden Symbolic))

cRegisterFirstForbiddenGen
  :: MonadGen n
  => SimpleState Symbolic
  -> Maybe (n (RegFirstForbidden Symbolic))
cRegisterFirstForbiddenGen (SimpleState registeredFirst) =
  if registeredFirst
  then Just (RegFirstForbidden <$> genRegPlayerRandomAdmin)
  else Nothing

cRegisterFirstForbiddenExe
  :: ( MonadIO m
     , MonadTest m
     )
  => ClientEnv
  -> RegFirstForbidden Concrete
  -> m ServantError

cRegisterFirstForbiddenExe
  :: ( MonadIO m
     , MonadTest m
     )
  => ClientEnv
  -> RegFirstForbidden Concrete
  -> m ServantError
cRegisterFirstForbiddenExe env (RegFirstForbidden rp) =
  evalEither =<< failureClient env (registerFirst rp)

cRegisterFirstForbiddenCallbacks
  :: [Callback RegFirstForbidden ServantError SimpleState]

cRegisterFirstForbiddenCallbacks
  :: [Callback RegFirstForbidden ServantError SimpleState]
cRegisterFirstForbiddenCallbacks = [
    Require $ \(SimpleState registeredFirst) _input ->
      registeredFirst





  ]

cRegisterFirstForbiddenCallbacks
  :: [Callback RegFirstForbidden ServantError SimpleState]
cRegisterFirstForbiddenCallbacks = [
    Require $ \(SimpleState registeredFirst) _input ->
      registeredFirst
  , Ensure $ \_sOld _sNew _input se ->
      case se of
        FailureResponse{..} ->
          responseStatus === forbidden403
        _ -> failure
  ]

propRegisterFirst

propRegisterFirst :: ClientEnv -> IO () -> TestTree
propRegisterFirst env reset =

propRegisterFirst :: ClientEnv -> IO () -> TestTree
propRegisterFirst env reset =
  testProperty "register-first" . property $ do
    let
      initialState = SimpleState False

propRegisterFirst :: ClientEnv -> IO () -> TestTree
propRegisterFirst env reset =
  testProperty "register-first" . property $ do
    let
      initialState = SimpleState False
      cs = [ cRegisterFirst env
           , cRegisterFirstForbidden env]

propRegisterFirst :: ClientEnv -> IO () -> TestTree
propRegisterFirst env reset =
  testProperty "register-first" . property $ do
    let
      initialState = SimpleState False
      cs = [ cRegisterFirst env
           , cRegisterFirstForbidden env]
    actions <- forAll $
      Gen.sequential (Range.linear 1 100) initialState cs

propRegisterFirst :: ClientEnv -> IO () -> TestTree
propRegisterFirst env reset =
  testProperty "register-first" . property $ do
    let
      initialState = SimpleState False
      cs = [ cRegisterFirst env
           , cRegisterFirstForbidden env]
    actions <- forAll $
      Gen.sequential (Range.linear 1 100) initialState cs

    liftIO reset
    executeSequential initialState actions

Test setup

• Start a temporary database instance
• Fork a thread to run our server (starting with DB migration)
• Run properties with ClientEnv

cRegisterFirstGen (SimpleState registeredFirst) =
  if registeredFirst
  then Nothing
  else Just (RegFirst <$> genRegPlayerRandomAdmin)

cRegisterFirstGen (SimpleState registeredFirst) =
  Just (RegFirst <$> genRegPlayerRandomAdmin)

cRegisterFirstCallbacks =
  [ Require $ \(SimpleState registeredFirst) _i ->
      not registeredFirst
  , Update $ \_sOld _i _o -> SimpleState True
  , Ensure $ \_sOld _sNew _input out ->
      case out of
        (ResponsePlayer (LS.PlayerId (Auto mId))
                        (Token token)) -> do
          assert $ not (BS.null t)
          assert $ maybe False (>= 0) mId
  ]

cRegisterFirstCallbacks =
  [ 
    
    Update $ \_sOld _i _o -> SimpleState True
  , Ensure $ \_sOld _sNew _input out ->
      case out of
        (ResponsePlayer (LS.PlayerId (Auto mId))
                        (Token token)) -> do
          assert $ not (BS.null t)
          assert $ maybe False (>= 0) mId
  ]

Property

Successfully registering a player increments the player count.

State

data LeaderboardState (v :: * -> *) =
  LeaderboardState
  { _players :: M.Map Text (PlayerWithRsp v)
  , _admins  :: S.Set Text
  }
deriving instance Show1 v => Show (LeaderboardState v)
deriving instance Eq1 v => Eq (LeaderboardState v)

data PlayerWithRsp v =
  PlayerWithRsp
  { _pwrRsp      :: Var ResponsePlayer v




  }
  deriving (Eq, Show)

data PlayerWithRsp v =
  PlayerWithRsp
  { _pwrRsp      :: Var ResponsePlayer v
  , _pwrEmail    :: Text
  , _pwrUsername :: Text
  , _pwrPassword :: Text
  , _pwrIsAdmin  :: Maybe Bool
  }
  deriving (Eq, Show)

Commands

cRegFirst

Update $
  \_ (RegFirst lbr@LeaderboardRegistration{..}) rsp ->

Update $
  \_ (RegFirst lbr@LeaderboardRegistration{..}) rsp ->
     let
       player = mkPlayerWithRsp lbr rsp

Update $
  \_ (RegFirst lbr@LeaderboardRegistration{..}) rsp ->
     let
       player = mkPlayerWithRsp lbr rsp
       players = M.singleton _lbrEmail player

Update $
  \_ (RegFirst lbr@LeaderboardRegistration{..}) rsp ->
     let
       player = mkPlayerWithRsp lbr rsp
       players = M.singleton _lbrEmail player
       admins = S.singleton _lbrEmail

Update $
  \_ (RegFirst lbr@LeaderboardRegistration{..}) rsp ->
     let
       player = mkPlayerWithRsp lbr rsp
       players = M.singleton _lbrEmail player
       admins = S.singleton _lbrEmail
     in
       LeaderboardState players admins

cGetPlayerCount

data GetPlayerCount (v :: * -> *) =
    GetPlayerCount
  deriving (Eq, Show)

Ensure $ \(LeaderboardState ps as) _sNew _i c -> do
  length ps === fromIntegral c
  assert $ length ps >= length as

cRegister

data Register (v :: * -> *) =
  Register RegisterPlayer (PlayerWithRsp v)
  deriving (Eq, Show)

cRegisterGen rs@(LeaderboardState ps as) =
  if null as
  then Nothing

cRegisterGen rs@(LeaderboardState ps as) =
  if null as
  then Nothing
  else
    let
      maybeGenAdmin :: Maybe (n (PlayerWithRsp v))
      maybeGenAdmin =
        pure $ (M.!) ps <$> (Gen.element . S.toList $ as)

cRegisterGen rs@(LeaderboardState ps as) =
  if null as
  then Nothing
  else
    let
      maybeGenAdmin :: Maybe (n (PlayerWithRsp v))
      maybeGenAdmin =
        pure $ (M.!) ps <$> (Gen.element . S.toList $ as)
    in
      (Register <$> genRegPlayerRandomAdmin ps <*>)
        <$> maybeGenAdmin

cRegisterExecute
  :: ( MonadIO m
     , MonadTest m
     )
  => ClientEnv
  -> Register Concrete
  -> m ResponsePlayer
cRegisterExecute env (Register rp p) =
  let
    t = clientToken p
  in
    evalEither =<< successClient env (register t rp)

Require $ \(LeaderboardState _ as) (Register _ p) ->
  S.member (_pwrEmail p) as

Update $
  \(LeaderboardState ps as)
   (Register rp@LeaderboardRegistration{..} _)
   rsp ->

Update $
  \(LeaderboardState ps as)
   (Register rp@LeaderboardRegistration{..} _)
   rsp ->
     let
       newPlayers =
         M.insert _lbrEmail (mkPlayerWithRsp rp rsp) ps

Update $
  \(LeaderboardState ps as)
   (Register rp@LeaderboardRegistration{..} _)
   rsp ->
     let
       newPlayers =
         M.insert _lbrEmail (mkPlayerWithRsp rp rsp) ps
       newAdmins =
         case _lbrIsAdmin of
           Just True -> S.insert _lbrEmail as
           _         -> as

Update $
  \(LeaderboardState ps as)
   (Register rp@LeaderboardRegistration{..} _)
   rsp ->
     let
       newPlayers =
         M.insert _lbrEmail (mkPlayerWithRsp rp rsp) ps
       newAdmins =
         case _lbrIsAdmin of
           Just True -> S.insert _lbrEmail as
           _         -> as
     in
       LeaderboardState newPlayers newAdmins

propRegisterCount env reset =
  testProperty "register-counts" . property $ do

propRegisterCount env reset =
  testProperty "register-counts" . property $ do
  let
    initialState = LeaderboardState M.empty S.empty

propRegisterCount env reset =
  testProperty "register-counts" . property $ do
  let
    initialState = LeaderboardState M.empty S.empty
    commands = [
        cRegisterFirst env
      , cRegisterFirstForbidden env
      , cRegister env
      , cGetPlayerCount env
      ]
  -- rest is the same as register-first

Property

Data retrieved for a player matches data entered

cMe

cMe
  :: ( MonadGen n
     , MonadTest m
     , MonadIO m
     )
  => ClientEnv
  -> Command n m LeaderboardState
cMe env =
    Command cMeGen (cMeExecute env) cMeCallbacks

cMeGen
  :: MonadGen n
  => LeaderboardState Symbolic
  -> Maybe (n (Me Symbolic))
cMeGen (LeaderboardState ps _) =
  (fmap . fmap) Me (genPlayerWithRsp ps)

cMeExecute
  :: ( MonadIO m
     , MonadTest m
     )
  => ClientEnv
  -> Me Concrete
  -> m Player
cMeExecute env (Me pwr) =
  evalEither =<< successClient env (me (clientToken pwr))

cMeCallbacks =
  [ Require $ \(LeaderboardState ps _) (Me p) ->
      M.member (_pwrEmail p) ps









  ]

cMeCallbacks =
  [ Require $ \(LeaderboardState ps _) (Me p) ->
      M.member (_pwrEmail p) ps
  , Ensure $
    \(LeaderboardState ps _) _ _ Player{..} -> do
      PlayerWithRsp{..} <- eval (ps M.! _playerEmail)






  ]

cMeCallbacks =
  [ Require $ \(LeaderboardState ps _) (Me p) ->
      M.member (_pwrEmail p) ps
  , Ensure $
    \(LeaderboardState ps _) _ _ Player{..} -> do
      PlayerWithRsp{..} <- eval (ps M.! _playerEmail)
      let
        pwrAdmin = fromMaybe True _pwrIsAdmin




  ]

cMeCallbacks =
  [ Require $ \(LeaderboardState ps _) (Me p) ->
      M.member (_pwrEmail p) ps
  , Ensure $
    \(LeaderboardState ps _) _ _ Player{..} -> do
      PlayerWithRsp{..} <- eval (ps M.! _playerEmail)
      let
        pwrAdmin = fromMaybe True _pwrIsAdmin
      _rspId (concrete _pwrRsp) === LS.PlayerId _playerId
      _pwrUsername === _playerUsername
      _pwrEmail === _playerEmail
      pwrAdmin === _playerIsAdmin
  ]

cMeCallbacks =
  [ Require $ \(LeaderboardState ps _) (Me p) ->
      M.member (_pwrEmail p) ps
  , Ensure $
    \(LeaderboardState ps _) _ _ p@Player{..} -> do
      pwr@PlayerWithRsp{..} <- eval (ps M.! _playerEmail)
      let
        pwrAdmin = fromMaybe True _pwrIsAdmin
      _rspId (concrete _pwrRsp) === LS.PlayerId _playerId
      _pwrUsername === _playerUsername
      _pwrEmail === _playerEmail
      pwrAdmin === _playerIsAdmin
  ]

cMeCallbacks =
  [





        pwrAdmin = fromMaybe True _pwrIsAdmin




  ]

cMeCallbacks =
  [





        pwrAdmin = fromMaybe False _pwrIsAdmin




  ]

This talk

Sources

Images