Copyright | (C) 2017 ATS Advanced Telematic Systems GmbH |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Stevan Andjelkovic <stevan.andjelkovic@here.com> |
Stability | provisional |
Portability | non-portable (GHC extensions) |
Safe Haskell | None |
Language | Haskell2010 |
Synopsis
- data StateMachine model cmd m resp = StateMachine {
- initModel :: forall r. model r
- transition :: forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r
- precondition :: model Symbolic -> cmd Symbolic -> Logic
- postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
- invariant :: Maybe (model Concrete -> Logic)
- generator :: model Symbolic -> Maybe (Gen (cmd Symbolic))
- distribution :: Maybe (Matrix Int)
- shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
- semantics :: cmd Concrete -> m (resp Concrete)
- mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
- data Command cmd resp = Command !(cmd Symbolic) !(resp Symbolic) ![Var]
- newtype Commands cmd resp = Commands {
- unCommands :: [Command cmd resp]
- lengthCommands :: Commands cmd resp -> Int
- data ParallelCommandsF t cmd resp = ParallelCommands {}
- type ParallelCommands = ParallelCommandsF Pair
- data Pair a = Pair {}
- fromPair :: Pair a -> (a, a)
- toPair :: (a, a) -> Pair a
- data Reason
- module Test.StateMachine.Types.Environment
- module Test.StateMachine.Types.GenSym
- module Test.StateMachine.Types.History
- module Test.StateMachine.Types.References
Documentation
data StateMachine model cmd m resp Source #
StateMachine | |
|
data Command cmd resp Source #
Previously symbolically executed command
Invariant: the variables must be the variables in the response.
newtype Commands cmd resp Source #
Commands | |
|
lengthCommands :: Commands cmd resp -> Int Source #
data ParallelCommandsF t cmd resp Source #
Instances
(Show (cmd Symbolic), Show (resp Symbolic), Show (t (Commands cmd resp))) => Show (ParallelCommandsF t cmd resp) Source # | |
Defined in Test.StateMachine.Types showsPrec :: Int -> ParallelCommandsF t cmd resp -> ShowS # show :: ParallelCommandsF t cmd resp -> String # showList :: [ParallelCommandsF t cmd resp] -> ShowS # |
type ParallelCommands = ParallelCommandsF Pair Source #
Instances
Functor Pair Source # | |
Foldable Pair Source # | |
Defined in Test.StateMachine.Types fold :: Monoid m => Pair m -> m # foldMap :: Monoid m => (a -> m) -> Pair a -> m # foldr :: (a -> b -> b) -> b -> Pair a -> b # foldr' :: (a -> b -> b) -> b -> Pair a -> b # foldl :: (b -> a -> b) -> b -> Pair a -> b # foldl' :: (b -> a -> b) -> b -> Pair a -> b # foldr1 :: (a -> a -> a) -> Pair a -> a # foldl1 :: (a -> a -> a) -> Pair a -> a # elem :: Eq a => a -> Pair a -> Bool # maximum :: Ord a => Pair a -> a # | |
Traversable Pair Source # | |
Eq a => Eq (Pair a) Source # | |
Ord a => Ord (Pair a) Source # | |
Show a => Show (Pair a) Source # | |