Copyright  (C) 2017 ATS Advanced Telematic Systems GmbH 

License  BSDstyle (see the file LICENSE) 
Maintainer  Stevan Andjelkovic <stevan.andjelkovic@here.com> 
Stability  provisional 
Portability  nonportable (GHC extensions) 
Safe Haskell  None 
Language  Haskell2010 
This module contains helpers for generating, shrinking, and checking sequential programs.
Synopsis
 forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => CommandNames cmd => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp > Maybe Int > (Commands cmd resp > prop) > Property
 generateCommands :: (Foldable resp, Show (model Symbolic)) => CommandNames cmd => StateMachine model cmd m resp > Maybe Int > Gen (Commands cmd resp)
 generateCommandsState :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => CommandNames cmd => StateMachine model cmd m resp > Counter > Maybe Int > StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd resp)
 measureFrequency :: (Foldable resp, Show (model Symbolic)) => CommandNames cmd => StateMachine model cmd m resp > Maybe Int > Int > 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]
 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)]
 data ValidateEnv model = ValidateEnv {}
 data ShouldShrink
 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 :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp > TChan (Pid, HistoryEvent cmd resp) > Pid > Bool > 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
 transitionMatrix :: forall cmd. CommandNames cmd => Proxy (cmd Symbolic) > (String > String > Int) > Matrix Int
Documentation
:: 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 
:: (Foldable resp, Show (model Symbolic))  
=> CommandNames cmd  
=> StateMachine model cmd m resp  
> Maybe Int  Minimum number of commands. 
> Gen (Commands cmd resp) 
calculateFrequency :: CommandNames cmd => Commands cmd resp > Map (String, Maybe String) Int Source #
shrinkCommands :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp > Commands cmd resp > [Commands cmd resp] Source #
Shrink commands in a precondition 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)] 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', 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 Source #
Environment required during shrinkAndValidate
ValidateEnv  

initValidateEnv :: model Symbolic > ValidateEnv model Source #
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) Source #
getChanContents :: MonadIO m => TChan a > m [a] Source #
:: (Traversable cmd, Foldable resp)  
=> (MonadCatch m, MonadIO m)  
=> StateMachine model cmd m resp  
> TChan (Pid, HistoryEvent cmd resp)  
> Pid  
> Bool  Check invariant and postcondition? 
> 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 () 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 resp. CommandNames cmd => Commands cmd resp > [(String, Int)] Source #
commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp > [String] Source #
checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp > Property > Property Source #
Print distribution of commands and fail if some commands have not been executed.