{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}
module Test.StateMachine.Types
( StateMachine(..)
, Command(..)
, Commands(..)
, lengthCommands
, ParallelCommandsF(..)
, ParallelCommands
, Pair(..)
, fromPair
, toPair
, Reason(..)
, module Test.StateMachine.Types.Environment
, module Test.StateMachine.Types.GenSym
, module Test.StateMachine.Types.History
, module Test.StateMachine.Types.References
) where
import Data.Functor.Classes
(Ord1, Show1)
import Data.Matrix
(Matrix)
import Data.Semigroup
(Semigroup)
import Prelude
import Test.QuickCheck
(Gen)
import Test.StateMachine.Logic
import Test.StateMachine.Types.Environment
import Test.StateMachine.Types.GenSym
import Test.StateMachine.Types.History
import Test.StateMachine.Types.References
data StateMachine model cmd m resp = StateMachine
{ initModel :: forall r. model r
, transition :: forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r
, precondition :: model Symbolic -> cmd Symbolic -> Logic
, postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
, invariant :: Maybe (model Concrete -> Logic)
, generator :: model Symbolic -> Maybe (Gen (cmd Symbolic))
, distribution :: Maybe (Matrix Int)
, shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
, semantics :: cmd Concrete -> m (resp Concrete)
, mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
}
data Command cmd resp = Command !(cmd Symbolic) !(resp Symbolic) ![Var]
deriving instance (Show (cmd Symbolic), Show (resp Symbolic)) => Show (Command cmd resp)
newtype Commands cmd resp = Commands
{ unCommands :: [Command cmd resp] }
deriving (Semigroup, Monoid)
deriving instance (Show (cmd Symbolic), Show (resp Symbolic)) => Show (Commands cmd resp)
lengthCommands :: Commands cmd resp -> Int
lengthCommands = length . unCommands
data Reason
= Ok
| PreconditionFailed String
| PostconditionFailed String
| InvariantBroken String
| ExceptionThrown
deriving (Eq, Show)
data ParallelCommandsF t cmd resp = ParallelCommands
{ prefix :: !(Commands cmd resp)
, suffixes :: [t (Commands cmd resp)]
}
deriving instance (Show (cmd Symbolic), Show (resp Symbolic), Show (t (Commands cmd resp))) =>
Show (ParallelCommandsF t cmd resp)
data Pair a = Pair
{ proj1 :: !a
, proj2 :: !a
}
deriving (Eq, Ord, Show, Functor, Foldable, Traversable)
fromPair :: Pair a -> (a, a)
fromPair (Pair x y) = (x, y)
toPair :: (a, a) -> Pair a
toPair (x, y) = Pair x y
type ParallelCommands = ParallelCommandsF Pair