Copyright	(C) 2017 ATS Advanced Telematic Systems GmbH
License	BSD-style (see the file LICENSE)
Maintainer	Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
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 :: forall prop (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (m :: Type -> Type). (Testable prop, Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd resp -> prop) -> Property
existsCommands :: forall model cmd (m :: Type -> Type) (resp :: (Type -> Type) -> Type) prop. (Testable prop, Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> [model Symbolic -> Gen (cmd Symbolic)] -> (Commands cmd resp -> prop) -> Property
generateCommands :: forall (resp :: (Type -> Type) -> Type) (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd resp)
generateCommandsState :: forall model (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic) Gen (Commands cmd resp)
deadlockError :: forall model (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) b. (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b
getUsedVars :: Foldable f => f Symbolic -> [Var]
shrinkCommands :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp]
shrinkAndValidate :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)]
data ValidateEnv (model :: (Type -> Type) -> Type) = ValidateEnv {
- veModel :: model Symbolic
- veScope :: Map Var Var
- veCounter :: Counter
}
data ShouldShrink
- = MustShrink
- | DontShrink
initValidateEnv :: model Symbolic -> ValidateEnv model
runCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands' :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) m model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason)
getChanContents :: MonadIO m => TChan a -> m [a]
data Check
- = CheckPrecondition
- | CheckEverything
- | CheckNothing
executeCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason
prettyPrintHistory :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO ()
prettyPrintHistory' :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type) tag. (CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete), CanDiff [tag]) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> IO ()
prettyCommands :: forall (m :: Type -> Type) (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). (MonadIO m, CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m ()
prettyCommands' :: forall (m :: Type -> Type) (model :: (Type -> Type) -> Type) tag (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). (MonadIO m, CanDiff (model Concrete), CanDiff [tag], Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> Property -> PropertyM m ()
saveCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). (Show (cmd Symbolic), Show (resp Symbolic)) => FilePath -> Commands cmd resp -> Property -> Property
runSavedCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m, Read (cmd Symbolic), Read (resp Symbolic)) => StateMachine model cmd m resp -> FilePath -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason)
commandNames :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> [(String, Int)]
commandNamesInOrder :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> [String]
coverCommandNames :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> Property -> Property
checkCommandNames :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> Property -> Property
showLabelledExamples :: forall tag (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type). (Show tag, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> IO ()
showLabelledExamples' :: forall tag (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type). (Show tag, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> Int -> ([Event model cmd resp Symbolic] -> [tag]) -> (tag -> Bool) -> IO ()

Documentation

forAllCommands Source #

Arguments

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

existsCommands Source #

Arguments

:: forall model cmd (m :: Type -> Type) (resp :: (Type -> Type) -> Type) prop. (Testable prop, Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic))
=> StateMachine model cmd m resp
-> [model Symbolic -> Gen (cmd Symbolic)]	Generators.
-> (Commands cmd resp -> prop)	Predicate.
-> Property

Generate commands from a list of generators.

generateCommands Source #

Arguments

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

generateCommandsState Source #

Arguments

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

deadlockError :: forall model (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) b. (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b Source #

getUsedVars :: Foldable f => f Symbolic -> [Var] Source #

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

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

shrinkAndValidate :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] Source #

Validate list of commands, optionally shrinking one of the commands

The input to this function is a list of commands (Commands), for example

[A, B, C, D, E, F, G, H]

The result is a list of Commands, i.e. a list of lists. The outermost list is used for all the shrinking possibilities. For example, let's assume we haven't shrunk something yet, and therefore need to shrink one of the commands. Let's further assume that only commands B and E can be shrunk, to B1, B2 and E1, E2, E3 respectively. Then the result will look something like

[    -- outermost list recording all the shrink possibilities
    [A', B1', C', D', E' , F', G', H']   -- B shrunk to B1
  , [A', B2', C', D', E' , F', G', H']   -- B shrunk to B2
  , [A', B' , C', D', E1', F', G', H']   -- E shrunk to E1
  , [A', B' , C', D', E2', F', G', H']   -- E shrunk to E2
  , [A', B' , C', D', E3', F', G', H']   -- E shrunk to E3
]

where one of the commands has been shrunk and all commands have been validated and renumbered (references updated). So, in this example, the result will contain at most 5 lists; it may contain fewer, since some of these lists may not be valid.

If we _did_ already shrink something, then no commands will be shrunk, and the resulting list will either be empty (if the list of commands was invalid) or contain a single element with the validated and renumbered commands.

data ValidateEnv (model :: (Type -> Type) -> Type) Source #

Environment required during shrinkAndValidate

Constructors

ValidateEnv

Fields

veModel :: model Symbolic
The model we're starting validation from
veScope :: Map Var Var
Reference renumbering
When a command
```
Command .. [Var i, ..]
```
is changed during validation to
```
Command .. [Var j, ..]
```
then any subsequent uses of Var i should be replaced by Var j. This is recorded in veScope. When we remove the first command altogether (during shrinking), then Var i won't appear in the veScope and shrank candidates that contain commands referring to Var i should be considered as invalid.
veCounter :: Counter
Counter (for generating new references)

data ShouldShrink Source #

Constructors

MustShrink
DontShrink

initValidateEnv :: model Symbolic -> ValidateEnv model Source #

runCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) Source #

runCommands' :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) m model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason) Source #

getChanContents :: MonadIO m => TChan a -> m [a] Source #

data Check Source #

Constructors

CheckPrecondition
CheckEverything
CheckNothing

executeCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason Source #

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

prettyPrintHistory' :: forall (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (m :: Type -> Type) (resp :: (Type -> Type) -> Type) tag. (CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete), CanDiff [tag]) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> IO () Source #

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

prettyCommands' :: forall (m :: Type -> Type) (model :: (Type -> Type) -> Type) tag (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). (MonadIO m, CanDiff (model Concrete), CanDiff [tag], Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> Property -> PropertyM m () Source #

Variant of prettyCommands that also prints the tags covered by each command.

saveCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). (Show (cmd Symbolic), Show (resp Symbolic)) => FilePath -> Commands cmd resp -> Property -> Property Source #

runSavedCommands :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type) model. (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m, Read (cmd Symbolic), Read (resp Symbolic)) => StateMachine model cmd m resp -> FilePath -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason) Source #

commandNames :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> [(String, Int)] Source #

commandNamesInOrder :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> [String] Source #

coverCommandNames :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> Property -> Property Source #

Fail if some commands have not been executed.

checkCommandNames :: forall (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type). CommandNames cmd => Commands cmd resp -> Property -> Property Source #

Print the percentage of each command used. The prefix check is an unfortunate remaining for backwards compatibility.

showLabelledExamples :: forall tag (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type). (Show tag, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> IO () Source #

showLabelledExamples' Source #

Arguments

:: forall tag (model :: (Type -> Type) -> Type) (cmd :: (Type -> Type) -> Type) (resp :: (Type -> Type) -> Type) (m :: Type -> Type). (Show tag, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic), Traversable cmd, Foldable resp)
=> StateMachine model cmd m resp
-> Maybe Int	Seed
-> Int	Number of tests to run to find examples
-> ([Event model cmd resp Symbolic] -> [tag])
-> (tag -> Bool)	Tag filter (can be `const True`)
-> IO ()

Show minimal examples for each of the generated tags.