{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
-----------------------------------------------------------------------------
-- |
-- Module : Test.StateMachine
-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : Stevan Andjelkovic <stevan@advancedtelematic.com>
-- Stability : provisional
-- Portability : non-portable (GHC extensions)
--
-- The main module for state machine based testing.
--
-----------------------------------------------------------------------------
module Test.StateMachine
( -- * Sequential property helper
sequentialProperty
, sequentialProperty'
-- * Parallel property helper
, parallelProperty
, parallelProperty'
, module Test.StateMachine.Types
) where
import Control.Monad.State
(StateT, evalStateT, lift, replicateM_)
import qualified Data.Map as M
import Test.QuickCheck
(Gen)
import Test.QuickCheck.Monadic
(monadic, monadicIO, run)
import Test.QuickCheck.Property
(Property, forAllShrink)
import qualified Test.StateMachine.Internal.IxMap as IxM
import Test.StateMachine.Internal.Parallel
import Test.StateMachine.Internal.Sequential
import Test.StateMachine.Internal.Types
import Test.StateMachine.Internal.Utils
import Test.StateMachine.Types
------------------------------------------------------------------------
-- | This function builds a property that tests if your model is agrees
-- with your semantics when running commands sequentially.
sequentialProperty
:: CommandConstraint ix cmd
=> Monad m
=> Show (model ConstIntRef)
=> StateMachineModel model cmd -- ^ Model
-> Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator
-> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker
-> (forall resp. cmd refs resp -> m (Response_ refs resp)) -- ^ Semantics
-> (m Property -> Property)
-> Property
sequentialProperty smm gen shrinker sem runM =
sequentialProperty' smm (lift gen) () shrinker (const (const sem)) runM
-- | Same as above, except it provides more flexibility.
sequentialProperty'
:: CommandConstraint ix cmd
=> Show (model ConstIntRef)
=> Monad m
=> StateMachineModel model cmd -- ^ Model
-> StateT s Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator
-> s -- ^ Generator state
-> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker
-> (forall resp. model ConstIntRef ->
MayResponse_ ConstIntRef resp ->
cmd refs resp ->
m (Response_ refs resp)) -- ^ Semantics
-> (m Property -> Property)
-> Property
sequentialProperty' smm gen s shrinker sem runM =
forAllShrink
(fst . fst <$> liftGen' gen s 0 M.empty)
(liftShrink shrinker)
$ \cmds -> collectStats cmds $
monadic (runM . flip evalStateT IxM.empty) $
checkSequentialInvariant smm (initialModel smm) sem cmds
------------------------------------------------------------------------
-- | This function builds a property that tests your semantics for race
-- conditions, by runnings commands in parallel and then trying to
-- linearise the resulting history.
--
-- /Note:/ Make sure that your model passes the sequential property first.
parallelProperty
:: CommandConstraint ix cmd
=> StateMachineModel model cmd -- ^ Model
-> Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator
-> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker
-> (forall resp. cmd refs resp -> IO (Response_ refs resp)) -- ^ Semantics
-> Property
parallelProperty smm gen shrinker sem
= parallelProperty' smm (lift gen) () shrinker sem (return ())
parallelProperty'
:: CommandConstraint ix cmd
=> StateMachineModel model cmd -- ^ Model
-> StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -- ^ Generator
-> genState
-> (forall resp refs'. Shrinker (cmd refs' resp)) -- ^ Shrinker
-> (forall resp. cmd refs resp -> IO (Response_ refs resp)) -- ^ Semantics
-> IO () -- ^ Cleanup
-> Property
parallelProperty' smm gen genState shrinker sem clean
= forAllShrink
(liftGenFork' gen genState)
(liftShrinkFork shrinker)
$ \fork -> monadicIO $ replicateM_ 10 $ do
run clean
hist <- run $ liftSemFork sem fork
checkParallelInvariant smm hist