{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- 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
, okTransition
, okPostcondition
, okSemantics
, StateMachine'(..)
, Generator
, Shrinker
, Precondition
, Transition
, Transition'
, Postcondition
, Postcondition'
, InitialModel
, Result(..)
, ppResult
, Semantics
, Semantics'
, Runner
, Reason(..)
-- * 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, Show1)
import Data.Typeable
(Typeable)
import Data.Void
(Void, absurd)
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 m Void
-- | Same as above, but with possibly failing semantics.
data StateMachine' model act m err = StateMachine
{ generator' :: Generator model act
, shrinker' :: Shrinker act
, precondition' :: Precondition model act
, transition' :: Transition' model act err
, postcondition' :: Postcondition' model act err
, model' :: InitialModel model
, semantics' :: Semantics' act m err
, runner' :: Runner m
}
-- | Helper for lifting non-failing semantics to a possibly failing
-- state machine record.
stateMachine
:: forall m model act
. Functor m
=> Generator model act
-> Shrinker act
-> Precondition model act
-> Transition model act
-> Postcondition model act
-> InitialModel model
-> Semantics act m
-> Runner m
-> StateMachine' model act m Void
stateMachine gen shr precond trans post model sem run =
StateMachine gen shr precond (okTransition trans)
(okPostcondition post) model (okSemantics sem) run
okTransition :: Transition model act -> Transition' model act Void
okTransition transition model act (Success resp) = transition model act resp
okTransition _ _ _ (Fail false) = absurd false
okPostcondition :: Postcondition model act -> Postcondition' model act Void
okPostcondition postcondition model act (Success resp) = postcondition model act resp
okPostcondition _ _ _ (Fail false) = absurd false
okSemantics :: Functor m => Semantics act m -> Semantics' act m Void
okSemantics sem = fmap Success . sem
-- | 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, Show1 v) =>
model v -> act v resp -> v resp -> model v
type Transition' model act err = forall resp v. (Ord1 v, Show1 v) =>
model v -> act v resp -> Result err (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 -> Bool
type Postcondition' model act err = forall resp.
model Concrete -> act Concrete resp -> Result err resp -> Bool
-- | 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
-- | When we execute our actions we have access to concrete references.
type Semantics act m = forall resp. act Concrete resp -> m resp
-- | The result of executing an action.
data Result err resp = Success resp | Fail err
deriving Functor
ppResult :: (Show err, Show resp) => Result err resp -> String
ppResult (Success resp) = show resp
ppResult (Fail err) = show err
type Semantics' act m err = forall resp. act Concrete resp -> m (Result err resp)
-- | How to run the monad used by the semantics.
type Runner m = m Property -> IO Property
data Reason = Ok | PreconditionFailed | PostconditionFailed
deriving (Eq, Show)