Test.StateMachine.Sequential

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

Documentation

forAllCommands

Arguments

:: Testable prop

=> (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))

=> CommandNames cmd

=> (Traversable cmd, Foldable resp)

=> StateMachine model cmd m resp

-> Maybe Int

Minimum number of commands.

-> (Commands cmd resp -> prop)

Predicate.

-> Property

generateCommands

Arguments

:: (Foldable resp, Show (model Symbolic))

=> CommandNames cmd

=> StateMachine model cmd m resp

-> Maybe Int

Minimum number of commands.

-> Gen (Commands cmd resp)

generateCommandsState

Arguments

:: Foldable resp

=> Show (model Symbolic)

=> CommandNames cmd

=> StateMachine model cmd m resp

-> Counter

-> Maybe Int

Minimum number of commands.

-> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd resp)

measureFrequency

Arguments

:: (Foldable resp, Show (model Symbolic))

=> CommandNames cmd

=> StateMachine model cmd m resp

-> Maybe Int

Minimum number of commands.

-> Int

Maximum number of commands.

-> IO (Map (String, Maybe String) Int)

calculateFrequency :: CommandNames cmd => Commands cmd resp -> Map (String, Maybe String) Int

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

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

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

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

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', B1', 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

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

Constructors

MustShrink

DontShrink

initValidateEnv :: model Symbolic -> ValidateEnv model

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

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

executeCommands

Arguments

:: (Traversable cmd, Foldable resp)

=> (MonadCatch m, MonadIO m)

=> StateMachine model cmd m resp

-> TChan (Pid, HistoryEvent cmd resp)

-> Pid

-> Bool

Check invariant and post-condition?

-> Commands cmd resp

-> StateT (Environment, model Symbolic, Counter, 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 resp. CommandNames cmd => Commands cmd resp -> [(String, Int)]

commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String]

checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property

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

transitionMatrix :: forall cmd. CommandNames cmd => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int