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)
Safe Haskell	None
Language	Haskell2010

Test.StateMachine.Sequential

Description

This module contains helpers for generating, shrinking, and checking sequential programs.

Synopsis

forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd -> prop) -> Property
generateCommands :: (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd)
generateCommandsState :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd)
measureFrequency :: (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Maybe Int -> Int -> IO (Map (String, Maybe String) Int)
calculateFrequency :: (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Map (String, Maybe String) Int
getUsedVars :: Foldable f => f Symbolic -> Set Var
shrinkCommands :: (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd -> [Commands cmd]
liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic]) -> Command cmd -> [Command cmd]
validCommands :: forall model cmd m resp. (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd -> State (model Symbolic, Set Var, Counter) (Maybe (Commands cmd))
filterMaybe :: (a -> Maybe b) -> [a] -> [b]
modelCheck :: forall model cmd resp m. Monad m => StateMachine model cmd m resp -> Commands cmd -> PropertyM m Reason
runCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> Commands cmd -> PropertyM m (History cmd resp, model Concrete, Reason)
getChanContents :: TChan a -> IO [a]
executeCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Bool -> Commands cmd -> StateT (Environment, model Concrete) m Reason
prettyPrintHistory :: forall model cmd m resp. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO ()
prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m ()
commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [(String, Int)]
commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [String]
checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Property -> Property
transitionMatrix :: forall cmd. GConName1 (Rep1 cmd) => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int

Documentation

forAllCommands Source #

Arguments

:: Testable prop
=> (Show (cmd Symbolic), Show (model Symbolic))
=> (Generic1 cmd, GConName1 (Rep1 cmd))
=> (Foldable cmd, Foldable resp)
=> StateMachine model cmd m resp
-> Maybe Int	Minimum number of commands.
-> (Commands cmd -> prop)	Predicate.
-> Property

generateCommands Source #

Arguments

:: (Foldable resp, Show (model Symbolic))
=> (Generic1 cmd, GConName1 (Rep1 cmd))
=> StateMachine model cmd m resp
-> Maybe Int	Minimum number of commands.
-> Gen (Commands cmd)

generateCommandsState Source #

Arguments

:: Foldable resp
=> Show (model Symbolic)
=> (Generic1 cmd, GConName1 (Rep1 cmd))
=> StateMachine model cmd m resp
-> Counter
-> Maybe Int	Minimum number of commands.
-> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd)

measureFrequency Source #

Arguments

:: (Foldable resp, Show (model Symbolic))
=> (Generic1 cmd, GConName1 (Rep1 cmd))
=> StateMachine model cmd m resp
-> Maybe Int	Minimum number of commands.
-> Int	Maximum number of commands.
-> IO (Map (String, Maybe String) Int)

calculateFrequency :: (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Map (String, Maybe String) Int Source #

getUsedVars :: Foldable f => f Symbolic -> Set Var Source #

shrinkCommands :: (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd -> [Commands cmd] Source #

Shrink commands in a pre-condition and scope respecting way.

liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic]) -> Command cmd -> [Command cmd] Source #

validCommands :: forall model cmd m resp. (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd -> State (model Symbolic, Set Var, Counter) (Maybe (Commands cmd)) Source #

filterMaybe :: (a -> Maybe b) -> [a] -> [b] Source #

modelCheck :: forall model cmd resp m. Monad m => StateMachine model cmd m resp -> Commands cmd -> PropertyM m Reason Source #

runCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> Commands cmd -> PropertyM m (History cmd resp, model Concrete, Reason) Source #

getChanContents :: TChan a -> IO [a] Source #

executeCommands Source #

Arguments

:: (Traversable cmd, Foldable resp)
=> (MonadCatch m, MonadBaseControl IO m)
=> StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Bool	Check invariant and post-condition?
-> Commands cmd
-> StateT (Environment, model Concrete) m Reason

prettyPrintHistory :: forall model cmd m resp. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO () Source #

prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m () Source #

commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [(String, Int)] Source #

commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [String] Source #

checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Property -> Property Source #

Print distribution of commands and fail if some commands have not been executed.

transitionMatrix :: forall cmd. GConName1 (Rep1 cmd) => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int Source #