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 |

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

calculateFrequency :: (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Map (String, Maybe String) Int 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.

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 #

:: (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 #