{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module : Test.StateMachine.Types
-- 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)
--
-- This module contains the main types exposed to the user. The module
-- is perhaps best read indirectly, on a per need basis, via the main
-- module "Test.StateMachine".
--
-----------------------------------------------------------------------------
module Test.StateMachine.Types
( -- * Untyped actions
Untyped(..)
-- * Type aliases
, StateMachine
, stateMachine
, StateMachine'(..)
, Generator
, Shrinker
, Precondition
, Transition
, Postcondition
, InitialModel
, Result(..)
, Semantics
, Runner
-- * Data type generic operations
, module Test.StateMachine.Types.Generics
-- * Higher-order functors, foldables and traversables
, module Test.StateMachine.Types.HFunctor
-- * References
, module Test.StateMachine.Types.References
)
where
import Data.Functor.Classes
(Ord1)
import Data.Typeable
(Typeable)
import Data.Void
(Void)
import Test.QuickCheck
(Gen, Property)
import Test.StateMachine.Types.Generics
import Test.StateMachine.Types.HFunctor
import Test.StateMachine.Types.References
------------------------------------------------------------------------
-- | An untyped action is an action where the response type is hidden
-- away using an existential type.
--
-- We need to hide the response type when generating actions, because
-- in general the actions we want to generate will have different
-- response types; and thus we can only type the generating function
-- if we hide the response type.
data Untyped (act :: (* -> *) -> * -> *) where
Untyped :: (Show resp, Typeable resp) => act Symbolic resp -> Untyped act
------------------------------------------------------------------------
-- | A (non-failing) state machine record bundles up all functionality
-- needed to perform our tests.
type StateMachine model act m = StateMachine' model act Void m
-- | Same as above, but with possibly failing semantics.
data StateMachine' model act err m = StateMachine
{ generator' :: Generator model act
, shrinker' :: Shrinker act
, precondition' :: Precondition model act
, transition' :: Transition model act
, postcondition' :: Postcondition model act
, model' :: InitialModel model
, semantics' :: Semantics act err m
, runner' :: Runner m
}
-- | Helper for lifting non-failing semantics to a possibly failing
-- state machine record.
stateMachine
:: Functor m
=> Generator model act
-> Shrinker act
-> Precondition model act
-> Transition model act
-> Postcondition model act
-> InitialModel model
-> (forall resp. act Concrete resp -> m resp)
-> Runner m
-> StateMachine' model act Void m
stateMachine gen shr precond trans post model sem run =
StateMachine gen shr precond trans post model (fmap Ok . sem) run
-- | When generating actions we have access to a model containing
-- symbolic references.
type Generator model act = model Symbolic -> Gen (Untyped act)
-- | Shrinking should preserve the response type of the action.
type Shrinker act = forall (v :: * -> *) resp.
act v resp -> [act v resp]
-- | Pre-conditions are checked while generating, at this stage we do
-- not yet have access to concrete references.
type Precondition model act = forall resp.
model Symbolic -> act Symbolic resp -> Bool
-- | The transition function must be polymorphic in the type of
-- variables used, as it is used both while generating and executing.
type Transition model act = forall resp v. Ord1 v =>
model v -> act v resp -> v resp -> model v
-- | Post-conditions are checked after the actions have been executed
-- and we got a response.
type Postcondition model act = forall resp.
model Concrete -> act Concrete resp -> resp -> Property
-- | The initial model is polymorphic in the type of references it uses,
-- so that it can be used both in the pre- and the post-condition
-- check.
type InitialModel m = forall (v :: * -> *). m v
-- | The result of executing an action.
data Result resp err = Ok resp | Fail err
-- | When we execute our actions we have access to concrete references.
type Semantics act err m = forall resp. act Concrete resp -> m (Result resp err)
-- | How to run the monad used by the semantics.
type Runner m = m Property -> IO Property