-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Test monadic programs using state machine based models -- -- See README at -- https://github.com/stevana/quickcheck-state-machine#readme @package quickcheck-state-machine @version 0.8.0 module Test.StateMachine.Lockstep.Auxiliary data Elem (xs :: [k]) (a :: k) [ElemHead] :: Elem (k : ks) k [ElemTail] :: Elem ks k -> Elem (k' : ks) k npAt :: NP f xs -> Elem xs a -> f a -- | N-ary traversable functors -- -- TODO: Don't provide Elem explicitly (just instantiate c)? -- TODO: Introduce HTraverse into SOP? class NTraversable (f :: (k -> Type) -> [k] -> Type) nctraverse :: (NTraversable f, Applicative m, All c xs) => proxy c -> (forall a. c a => Elem xs a -> g a -> m (h a)) -> f g xs -> m (f h xs) ntraverse :: (NTraversable f, Applicative m, SListI xs) => (forall a. Elem xs a -> g a -> m (h a)) -> f g xs -> m (f h xs) ncfmap :: (NTraversable f, All c xs) => proxy c -> (forall a. c a => Elem xs a -> g a -> h a) -> f g xs -> f h xs nfmap :: (NTraversable f, SListI xs) => (forall a. Elem xs a -> g a -> h a) -> f g xs -> f h xs ncfoldMap :: forall proxy f g m c xs. (NTraversable f, Monoid m, All c xs) => proxy c -> (forall a. c a => Elem xs a -> g a -> m) -> f g xs -> m nfoldMap :: (NTraversable f, Monoid m, SListI xs) => (forall a. Elem xs a -> g a -> m) -> f g xs -> m -- | This module defines a predicate logic-like language and its -- counterexample semantics. module Test.StateMachine.Logic data Logic Bot :: Logic Top :: Logic (:&&) :: Logic -> Logic -> Logic (:||) :: Logic -> Logic -> Logic (:=>) :: Logic -> Logic -> Logic Not :: Logic -> Logic LogicPredicate :: LogicPredicate -> Logic Forall :: [a] -> (a -> Logic) -> Logic Exists :: [a] -> (a -> Logic) -> Logic Boolean :: Bool -> Logic Annotate :: String -> Logic -> Logic data LogicPredicate (:==) :: a -> a -> LogicPredicate (:/=) :: a -> a -> LogicPredicate (:<) :: a -> a -> LogicPredicate (:<=) :: a -> a -> LogicPredicate (:>) :: a -> a -> LogicPredicate (:>=) :: a -> a -> LogicPredicate Member :: a -> t a -> LogicPredicate NotMember :: a -> t a -> LogicPredicate dual :: LogicPredicate -> LogicPredicate strongNeg :: Logic -> Logic data Counterexample BotC :: Counterexample Fst :: Counterexample -> Counterexample Snd :: Counterexample -> Counterexample EitherC :: Counterexample -> Counterexample -> Counterexample ImpliesC :: Counterexample -> Counterexample NotC :: Counterexample -> Counterexample PredicateC :: LogicPredicate -> Counterexample ForallC :: a -> Counterexample -> Counterexample ExistsC :: [a] -> [Counterexample] -> Counterexample BooleanC :: Counterexample AnnotateC :: String -> Counterexample -> Counterexample data Value VFalse :: Counterexample -> Value VTrue :: Value boolean :: Logic -> Bool logic :: Logic -> Value evalLogicPredicate :: LogicPredicate -> Value -- | Gather user annotations of a true logic expression. -- -- 
--   >>> gatherAnnotations (Top .// "top")
--   ["top"]
--
-- -- 
--   >>> gatherAnnotations ((Bot .// "bot") .|| (Top .// "top"))
--   ["top"]
--
-- -- 
--   >>> gatherAnnotations (Top .// "top1" .&& Top .// "top2")
--   ["top1","top2"]
--
-- -- 
--   >>> gatherAnnotations (Bot .// "bot" .&& Top .// "top")
--   []
--
-- -- 
--   >>> gatherAnnotations (forall [1,2,3] (\i -> 0 .< i .// "positive"))
--   ["positive","positive","positive"]
--
-- -- 
--   >>> gatherAnnotations (forall [0,1,2,3] (\i -> 0 .< i .// "positive"))
--   []
--
-- -- 
--   >>> gatherAnnotations (exists [1,2,3] (\i -> 0 .< i .// "positive"))
--   ["positive"]
--
gatherAnnotations :: Logic -> [String] (.==) :: (Eq a, Show a) => a -> a -> Logic infix 5 .== (./=) :: (Eq a, Show a) => a -> a -> Logic infix 5 ./= (.<) :: (Ord a, Show a) => a -> a -> Logic infix 5 .< (.<=) :: (Ord a, Show a) => a -> a -> Logic infix 5 .<= (.>) :: (Ord a, Show a) => a -> a -> Logic infix 5 .> (.>=) :: (Ord a, Show a) => a -> a -> Logic infix 5 .>= member :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic infix 8 `member` notMember :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic infix 8 `notMember` (.//) :: Logic -> String -> Logic infixl 4 .// (.&&) :: Logic -> Logic -> Logic infixr 3 .&& (.||) :: Logic -> Logic -> Logic infixr 2 .|| (.=>) :: Logic -> Logic -> Logic infixr 1 .=> forall :: Show a => [a] -> (a -> Logic) -> Logic exists :: Show a => [a] -> (a -> Logic) -> Logic instance GHC.Show.Show Test.StateMachine.Logic.Value instance GHC.Show.Show Test.StateMachine.Logic.LogicPredicate instance GHC.Show.Show Test.StateMachine.Logic.Counterexample -- | A list diff. module Test.StateMachine.TreeDiff.List -- | List difference. -- -- 
--   >>> diffBy (==) "hello" "world"
--   [Swp 'h' 'w',Swp 'e' 'o',Swp 'l' 'r',Cpy 'l',Swp 'o' 'd']
--
-- -- 
--   >>> diffBy (==) "kitten" "sitting"
--   [Swp 'k' 's',Cpy 'i',Cpy 't',Cpy 't',Swp 'e' 'i',Cpy 'n',Ins 'g']
--
-- -- 
--   \xs ys -> length (diffBy (==) xs ys) >= max (length xs) (length (ys :: String))
--
-- -- 
--   \xs ys -> length (diffBy (==) xs ys) <= length xs + length (ys :: String)
--
-- -- Note: currently this has O(n*m) memory requirements, for the -- sake of more obviously correct implementation. diffBy :: forall a. (a -> a -> Bool) -> [a] -> [a] -> [Edit a] -- | List edit operations -- -- The Swp constructor is redundant, but it let us spot a -- recursion point when performing tree diffs. data Edit a -- | insert Ins :: a -> Edit a -- | delete Del :: a -> Edit a -- | copy unchanged Cpy :: a -> Edit a -- | swap, i.e. delete + insert Swp :: a -> a -> Edit a instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.TreeDiff.List.Edit a) -- | This module uses Expr for richer diffs than based on -- Tree. module Test.StateMachine.TreeDiff.Expr -- | A untyped Haskell-like expression. -- -- Having richer structure than just Tree allows to have richer -- diffs. data Expr -- | application App :: ConstructorName -> [Expr] -> Expr -- | record constructor Rec :: ConstructorName -> Map FieldName Expr -> Expr -- | list constructor Lst :: [Expr] -> Expr -- | Constructor name is a string type ConstructorName = String -- | Record field name is a string too. type FieldName = String -- | Type used in the result of ediff. data EditExpr EditApp :: ConstructorName -> [Edit EditExpr] -> EditExpr EditRec :: ConstructorName -> Map FieldName (Edit EditExpr) -> EditExpr EditLst :: [Edit EditExpr] -> EditExpr -- | unchanged tree EditExp :: Expr -> EditExpr -- | List edit operations -- -- The Swp constructor is redundant, but it let us spot a -- recursion point when performing tree diffs. data Edit a -- | insert Ins :: a -> Edit a -- | delete Del :: a -> Edit a -- | copy unchanged Cpy :: a -> Edit a -- | swap, i.e. delete + insert Swp :: a -> a -> Edit a -- | Diff two Expr. -- -- For examples see ediff in Data.TreeDiff.Class. exprDiff :: Expr -> Expr -> Edit EditExpr instance GHC.Show.Show Test.StateMachine.TreeDiff.Expr.Expr instance GHC.Classes.Eq Test.StateMachine.TreeDiff.Expr.Expr instance GHC.Show.Show Test.StateMachine.TreeDiff.Expr.EditExpr instance Test.QuickCheck.Arbitrary.Arbitrary Test.StateMachine.TreeDiff.Expr.Expr -- | A ToExpr class. module Test.StateMachine.TreeDiff.Class -- | Difference between two ToExpr values. -- -- 
--   >>> let x = (1, Just 2) :: (Int, Maybe Int)
--   
--   >>> let y = (1, Nothing)
--   
--   >>> prettyEditExpr (ediff x y)
--   _×_ 1 -(Just 2) +Nothing
--
-- -- 
--   >>> data Foo = Foo { fooInt :: Either Char Int, fooBool :: [Maybe Bool], fooString :: String } deriving (Eq, Generic)
--   
--   >>> instance ToExpr Foo
--
-- -- 
--   >>> prettyEditExpr $ ediff (Foo (Right 2) [Just True] "fo") (Foo (Right 3) [Just True] "fo")
--   Foo {fooBool = [Just True], fooInt = Right -2 +3, fooString = "fo"}
--
-- -- 
--   >>> prettyEditExpr $ ediff (Foo (Right 42) [Just True, Just False] "old") (Foo (Right 42) [Nothing, Just False, Just True] "new")
--   Foo
--     {fooBool = [-Just True, +Nothing, Just False, +Just True],
--      fooInt = Right 42,
--      fooString = -"old" +"new"}
--
ediff :: ToExpr a => a -> a -> Edit EditExpr -- | Compare different types. -- -- Note: Use with care as you can end up comparing apples with -- oranges. -- -- 
--   >>> prettyEditExpr $ ediff' ["foo", "bar"] [Just "foo", Nothing]
--   [-"foo", +Just "foo", -"bar", +Nothing]
--
ediff' :: (ToExpr a, ToExpr b) => a -> b -> Edit EditExpr -- | toExpr converts a Haskell value into untyped Haskell-like -- syntax tree, Expr. -- -- 
--   >>> toExpr ((1, Just 2) :: (Int, Maybe Int))
--   App "_\215_" [App "1" [],App "Just" [App "2" []]]
--
class ToExpr a toExpr :: ToExpr a => a -> Expr toExpr :: (ToExpr a, Generic a, All2 ToExpr (GCode a), GFrom a, GDatatypeInfo a) => a -> Expr listToExpr :: ToExpr a => [a] -> Expr -- | An alternative implementation for literal types. We use show -- representation of them. defaultExprViaShow :: Show a => a -> Expr -- | 
--   >>> prettyExpr $ sopToExpr (gdatatypeInfo (Proxy :: Proxy String)) (gfrom "foo")
--   _:_ 'f' "oo"
--
sopToExpr :: All2 ToExpr xss => DatatypeInfo xss -> SOP I xss -> Expr instance Test.StateMachine.TreeDiff.Class.ToExpr Test.StateMachine.TreeDiff.Expr.Expr instance Test.StateMachine.TreeDiff.Class.ToExpr () instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Types.Bool instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Types.Ordering instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Num.Integer.Integer instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Num.Natural.Natural instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Types.Float instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Types.Double instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Types.Int instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Int.Int8 instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Int.Int16 instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Int.Int32 instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Int.Int64 instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Types.Word instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Word.Word8 instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Word.Word16 instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Word.Word32 instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Word.Word64 instance Test.StateMachine.TreeDiff.Class.ToExpr (Data.Proxy.Proxy a) instance Test.StateMachine.TreeDiff.Class.ToExpr GHC.Types.Char instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (GHC.Maybe.Maybe a) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Test.StateMachine.TreeDiff.Class.ToExpr b) => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Either.Either a b) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr [a] instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Test.StateMachine.TreeDiff.Class.ToExpr b) => Test.StateMachine.TreeDiff.Class.ToExpr (a, b) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Test.StateMachine.TreeDiff.Class.ToExpr b, Test.StateMachine.TreeDiff.Class.ToExpr c) => Test.StateMachine.TreeDiff.Class.ToExpr (a, b, c) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Test.StateMachine.TreeDiff.Class.ToExpr b, Test.StateMachine.TreeDiff.Class.ToExpr c, Test.StateMachine.TreeDiff.Class.ToExpr d) => Test.StateMachine.TreeDiff.Class.ToExpr (a, b, c, d) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Test.StateMachine.TreeDiff.Class.ToExpr b, Test.StateMachine.TreeDiff.Class.ToExpr c, Test.StateMachine.TreeDiff.Class.ToExpr d, Test.StateMachine.TreeDiff.Class.ToExpr e) => Test.StateMachine.TreeDiff.Class.ToExpr (a, b, c, d, e) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, GHC.Real.Integral a) => Test.StateMachine.TreeDiff.Class.ToExpr (GHC.Real.Ratio a) instance Data.Fixed.HasResolution a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Fixed.Fixed a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Functor.Identity.Identity a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Functor.Const.Const a b) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Control.Applicative.ZipList a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (GHC.Base.NonEmpty a) instance Test.StateMachine.TreeDiff.Class.ToExpr Data.Void.Void instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Semigroup.Internal.Dual a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Semigroup.Internal.Sum a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Semigroup.Internal.Product a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Monoid.First a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Monoid.Last a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Semigroup.Min a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Semigroup.Max a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Semigroup.First a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Semigroup.Last a) instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Tree.Tree a) instance (Test.StateMachine.TreeDiff.Class.ToExpr k, Test.StateMachine.TreeDiff.Class.ToExpr v) => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Map.Internal.Map k v) instance Test.StateMachine.TreeDiff.Class.ToExpr k => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Set.Internal.Set k) instance Test.StateMachine.TreeDiff.Class.ToExpr v => Test.StateMachine.TreeDiff.Class.ToExpr (Data.IntMap.Internal.IntMap v) instance Test.StateMachine.TreeDiff.Class.ToExpr Data.IntSet.Internal.IntSet instance Test.StateMachine.TreeDiff.Class.ToExpr v => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Sequence.Internal.Seq v) instance Test.StateMachine.TreeDiff.Class.ToExpr Data.Text.Internal.Lazy.Text instance Test.StateMachine.TreeDiff.Class.ToExpr Data.Text.Internal.Text instance Test.StateMachine.TreeDiff.Class.ToExpr Data.Time.Calendar.Days.Day instance Test.StateMachine.TreeDiff.Class.ToExpr Data.Time.Clock.Internal.UTCTime.UTCTime instance Test.StateMachine.TreeDiff.Class.ToExpr Data.ByteString.Lazy.Internal.ByteString instance Test.StateMachine.TreeDiff.Class.ToExpr Data.ByteString.Internal.ByteString instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Vector.Vector a) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Data.Vector.Unboxed.Base.Unbox a) => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Vector.Unboxed.Base.Vector a) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Foreign.Storable.Storable a) => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Vector.Storable.Vector a) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Data.Primitive.Types.Prim a) => Test.StateMachine.TreeDiff.Class.ToExpr (Data.Vector.Primitive.Vector a) -- | Utilities to pretty print Expr and EditExpr module Test.StateMachine.TreeDiff.Pretty -- | Because we don't want to commit to single pretty printing library, we -- use explicit dictionary. data Pretty doc Pretty :: (ConstructorName -> doc) -> ([(FieldName, doc)] -> doc) -> ([doc] -> doc) -> (doc -> doc) -> (doc -> doc) -> (doc -> doc) -> ([doc] -> doc) -> (doc -> doc) -> (doc -> doc -> doc) -> Pretty doc [ppCon] :: Pretty doc -> ConstructorName -> doc [ppRec] :: Pretty doc -> [(FieldName, doc)] -> doc [ppLst] :: Pretty doc -> [doc] -> doc [ppCpy] :: Pretty doc -> doc -> doc [ppIns] :: Pretty doc -> doc -> doc [ppDel] :: Pretty doc -> doc -> doc [ppSep] :: Pretty doc -> [doc] -> doc [ppParens] :: Pretty doc -> doc -> doc [ppHang] :: Pretty doc -> doc -> doc -> doc -- | Pretty print an Expr using explicit pretty-printing dictionary. ppExpr :: Pretty doc -> Expr -> doc -- | Pretty print an Edit EditExpr using explicit -- pretty-printing dictionary. ppEditExpr :: Pretty doc -> Edit EditExpr -> doc -- | Like ppEditExpr but print unchanged parts only shallowly ppEditExprCompact :: Pretty doc -> Edit EditExpr -> doc -- | Pretty via pretty library. prettyPretty :: Pretty Doc -- | Pretty print Expr using pretty. -- -- 
--   >>> prettyExpr $ Rec "ex" (Map.fromList [("[]", App "bar" [])])
--   ex {`[]` = bar}
--
prettyExpr :: Expr -> Doc -- | Pretty print Edit EditExpr using -- pretty. prettyEditExpr :: Edit EditExpr -> Doc -- | Compact prettyEditExpr. prettyEditExprCompact :: Edit EditExpr -> Doc -- | Pretty via ansi-wl-pprint library (with colors). ansiWlPretty :: Pretty Doc -- | Pretty print Expr using ansi-wl-pprint. ansiWlExpr :: Expr -> Doc -- | Pretty print Edit EditExpr using -- ansi-wl-pprint. ansiWlEditExpr :: Edit EditExpr -> Doc -- | Compact ansiWlEditExpr ansiWlEditExprCompact :: Edit EditExpr -> Doc -- | Like ansiWlPretty but color the background. ansiWlBgPretty :: Pretty Doc -- | Pretty print Expr using ansi-wl-pprint. ansiWlBgExpr :: Expr -> Doc -- | Pretty print Edit EditExpr using -- ansi-wl-pprint. ansiWlBgEditExpr :: Edit EditExpr -> Doc -- | Compact ansiWlBgEditExpr. ansiWlBgEditExprCompact :: Edit EditExpr -> Doc -- | Escape field or constructor name -- -- 
--   >>> putStrLn $ escapeName "Foo"
--   Foo
--
-- -- 
--   >>> putStrLn $ escapeName "_×_"
--   _×_
--
-- -- 
--   >>> putStrLn $ escapeName "-3"
--   `-3`
--
-- -- 
--   >>> putStrLn $ escapeName "kebab-case"
--   kebab-case
--
-- -- 
--   >>> putStrLn $ escapeName "inner space"
--   `inner space`
--
-- -- 
--   >>> putStrLn $ escapeName $ show "looks like a string"
--   "looks like a string"
--
-- -- 
--   >>> putStrLn $ escapeName $ show "tricky" ++ "   "
--   `"tricky"   `
--
-- -- 
--   >>> putStrLn $ escapeName "[]"
--   `[]`
--
-- -- 
--   >>> putStrLn $ escapeName "_,_"
--   `_,_`
--
escapeName :: String -> String -- | Diffing of (expression) trees. -- -- Diffing arbitrary Haskell data. First we convert values to untyped -- haskell-like expression Expr using generically derivable -- ToExpr class. Then we can diff two Expr values. The -- conversion and diffing is done by ediff function. See type and -- function haddocks for an examples. -- -- Interesting modules: -- -- module Test.StateMachine.TreeDiff -- | Tree diffing working on containers Tree. module Test.StateMachine.TreeDiff.Tree -- | A breadth-traversal diff. -- -- It's different from gdiff, as it doesn't produce a flat edit -- script, but edit script iself is a tree. This makes visualising the -- diff much simpler. -- --

Examples

-- -- Let's start from simple tree. We pretty print them as s-expressions. -- -- 
--   >>> let x = Node 'a' [Node 'b' [], Node 'c' [return 'd', return 'e'], Node 'f' []]
--   
--   >>> ppTree PP.char x
--   (a b (c d e) f)
--
-- -- If we modify an argument in a tree, we'll notice it's changed: -- -- 
--   >>> let y = Node 'a' [Node 'b' [], Node 'c' [return 'x', return 'e'], Node 'f' []]
--   
--   >>> ppTree PP.char y
--   (a b (c x e) f)
--
-- -- 
--   >>> ppEditTree PP.char (treeDiff x y)
--   (a b (c -d +x e) f)
--
-- -- If we modify a constructor, the whole sub-trees is replaced, though -- there might be common subtrees. -- -- 
--   >>> let z = Node 'a' [Node 'b' [], Node 'd' [], Node 'f' []]
--   
--   >>> ppTree PP.char z
--   (a b d f)
--
-- -- 
--   >>> ppEditTree PP.char (treeDiff x z)
--   (a b -(c d e) +d f)
--
-- -- If we add arguments, they are spotted too: -- -- 
--   >>> let w = Node 'a' [Node 'b' [], Node 'c' [return 'd', return 'x', return 'e'], Node 'f' []]
--   
--   >>> ppTree PP.char w
--   (a b (c d x e) f)
--
-- -- 
--   >>> ppEditTree PP.char (treeDiff x w)
--   (a b (c d +x e) f)
--
treeDiff :: Eq a => Tree a -> Tree a -> Edit (EditTree a) -- | Type used in the result of treeDiff. -- -- It's essentially a Tree, but the forest list is changed from -- [tree a] to [Edit (tree a)]. This highlights -- that treeDiff performs a list diff on each tree level. data EditTree a EditNode :: a -> [Edit (EditTree a)] -> EditTree a -- | List edit operations -- -- The Swp constructor is redundant, but it let us spot a -- recursion point when performing tree diffs. data Edit a -- | insert Ins :: a -> Edit a -- | delete Del :: a -> Edit a -- | copy unchanged Cpy :: a -> Edit a -- | swap, i.e. delete + insert Swp :: a -> a -> Edit a instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.TreeDiff.Tree.EditTree a) module Test.StateMachine.Types.Rank2 class Functor (f :: (k -> Type) -> Type) fmap :: Functor f => (forall x. p x -> q x) -> f p -> f q gfmap :: (Generic1 f, Functor (Rep1 f)) => (forall a. p a -> q a) -> f p -> f q (<$>) :: Functor f => (forall x. p x -> q x) -> f p -> f q class Foldable (f :: (k -> Type) -> Type) foldMap :: (Foldable f, Monoid m) => (forall x. p x -> m) -> f p -> m gfoldMap :: (Generic1 f, Foldable (Rep1 f), Monoid m) => (forall a. p a -> m) -> f p -> m class (Functor t, Foldable t) => Traversable (t :: (k -> Type) -> Type) traverse :: (Traversable t, Applicative f) => (forall a. p a -> f (q a)) -> t p -> f (t q) gtraverse :: (Generic1 t, Traversable (Rep1 t), Applicative f) => (forall a. p a -> f (q a)) -> t p -> f (t q) instance Test.StateMachine.Types.Rank2.Traversable GHC.Generics.U1 instance Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.K1 i c) instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:+: g) instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:*: g) instance forall k (f :: * -> *) (g :: (k -> *) -> *). (Data.Traversable.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:.: g) instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Traversable f => Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.M1 i c f) instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Traversable f => Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.Rec1 f) instance Test.StateMachine.Types.Rank2.Foldable GHC.Generics.U1 instance Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.K1 i c) instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:+: g) instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:*: g) instance forall k (f :: * -> *) (g :: (k -> *) -> *). (Data.Foldable.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:.: g) instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Foldable f => Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.M1 i c f) instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Foldable f => Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.Rec1 f) instance Test.StateMachine.Types.Rank2.Functor GHC.Generics.U1 instance Test.StateMachine.Types.Rank2.Functor (GHC.Generics.K1 i c) instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:+: g) instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:*: g) instance forall k (f :: * -> *) (g :: (k -> *) -> *). (GHC.Base.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:.: g) instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Functor f => Test.StateMachine.Types.Rank2.Functor (GHC.Generics.M1 i c f) instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Functor f => Test.StateMachine.Types.Rank2.Functor (GHC.Generics.Rec1 f) -- | This module contains reference related types. It's taken almost -- verbatim from the Hedgehog library. module Test.StateMachine.Types.References newtype Var Var :: Int -> Var data Symbolic a [Symbolic] :: Typeable a => Var -> Symbolic a data Concrete a [Concrete] :: Typeable a => a -> Concrete a newtype Reference a r Reference :: r a -> Reference a r reference :: Typeable a => a -> Reference a Concrete concrete :: Reference a Concrete -> a opaque :: Reference (Opaque a) Concrete -> a newtype Opaque a Opaque :: a -> Opaque a unOpaque :: Opaque a -> a instance Test.StateMachine.TreeDiff.Class.ToExpr Test.StateMachine.Types.References.Var instance GHC.Read.Read Test.StateMachine.Types.References.Var instance GHC.Generics.Generic Test.StateMachine.Types.References.Var instance GHC.Show.Show Test.StateMachine.Types.References.Var instance GHC.Classes.Ord Test.StateMachine.Types.References.Var instance GHC.Classes.Eq Test.StateMachine.Types.References.Var instance GHC.Generics.Generic (Test.StateMachine.Types.References.Reference a r) instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Opaque a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Opaque a) instance GHC.Show.Show (Test.StateMachine.Types.References.Symbolic a) instance Data.Typeable.Internal.Typeable a => GHC.Read.Read (Test.StateMachine.Types.References.Symbolic a) instance GHC.Classes.Eq (Test.StateMachine.Types.References.Symbolic a) instance GHC.Classes.Ord (Test.StateMachine.Types.References.Symbolic a) instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Types.References.Concrete a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Concrete a) instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Concrete a) instance Data.Typeable.Internal.Typeable a => GHC.Read.Read (Test.StateMachine.Types.References.Reference a Test.StateMachine.Types.References.Symbolic) instance GHC.Show.Show (Test.StateMachine.Types.References.Opaque a) instance Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Opaque a) instance Test.StateMachine.TreeDiff.Class.ToExpr (r a) => Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Reference a r) instance Test.StateMachine.Types.Rank2.Functor (Test.StateMachine.Types.References.Reference a) instance Test.StateMachine.Types.Rank2.Foldable (Test.StateMachine.Types.References.Reference a) instance Test.StateMachine.Types.Rank2.Traversable (Test.StateMachine.Types.References.Reference a) instance (GHC.Classes.Eq a, Data.Functor.Classes.Eq1 r) => GHC.Classes.Eq (Test.StateMachine.Types.References.Reference a r) instance (GHC.Classes.Ord a, Data.Functor.Classes.Ord1 r) => GHC.Classes.Ord (Test.StateMachine.Types.References.Reference a r) instance (Data.Functor.Classes.Show1 r, GHC.Show.Show a) => GHC.Show.Show (Test.StateMachine.Types.References.Reference a r) instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Concrete instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Concrete instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Concrete instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Concrete a) instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Symbolic instance Test.StateMachine.TreeDiff.Class.ToExpr a => Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Symbolic a) instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Symbolic instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Symbolic -- | This module contains the notion of a history of an execution of a -- (parallel) program. module Test.StateMachine.Types.History newtype History cmd resp History :: History' cmd resp -> History cmd resp [unHistory] :: History cmd resp -> History' cmd resp type History' cmd resp = [(Pid, HistoryEvent cmd resp)] newtype Pid Pid :: Int -> Pid [unPid] :: Pid -> Int data HistoryEvent cmd resp Invocation :: !cmd Concrete -> !Set Var -> HistoryEvent cmd resp Response :: !resp Concrete -> HistoryEvent cmd resp Exception :: !String -> HistoryEvent cmd resp -- | An operation packs up an invocation event with its corresponding -- response event. data Operation cmd resp Operation :: cmd Concrete -> resp Concrete -> Pid -> Operation cmd resp Crash :: cmd Concrete -> String -> Pid -> Operation cmd resp -- | Given a sequential history, group invocation and response events into -- operations. makeOperations :: History' cmd resp -> [Operation cmd resp] -- | Given a parallel history, return all possible interleavings of -- invocations and corresponding response events. interleavings :: History' cmd resp -> Forest (Operation cmd resp) operationsPath :: Forest (Operation cmd resp) -> [Operation cmd resp] completeHistory :: (cmd Concrete -> resp Concrete) -> History cmd resp -> History cmd resp instance GHC.Classes.Ord Test.StateMachine.Types.History.Pid instance GHC.Show.Show Test.StateMachine.Types.History.Pid instance GHC.Classes.Eq Test.StateMachine.Types.History.Pid instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Concrete), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Concrete)) => GHC.Classes.Eq (Test.StateMachine.Types.History.History cmd resp) instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.History cmd resp) instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Concrete), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Concrete)) => GHC.Classes.Eq (Test.StateMachine.Types.History.HistoryEvent cmd resp) instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.HistoryEvent cmd resp) instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.Operation cmd resp) module Test.StateMachine.DotDrawing data GraphOptions GraphOptions :: FilePath -> GraphvizOutput -> GraphOptions [filePath] :: GraphOptions -> FilePath [graphvizOutput] :: GraphOptions -> GraphvizOutput -- | The possible Graphviz output formats (that is, those that actually -- produce a file). data GraphvizOutput -- | Windows Bitmap Format. Bmp :: GraphvizOutput -- | Pretty-printed Dot output with no layout performed. Canon :: GraphvizOutput -- | Reproduces the input along with layout information. DotOutput :: GraphvizOutput -- | As with DotOutput, but provides even more information on how -- the graph is drawn. The optional Version is the same as -- specifying the XDotVersion attribute. XDot :: Maybe Version -> GraphvizOutput -- | Encapsulated PostScript. Eps :: GraphvizOutput -- | FIG graphics language. Fig :: GraphvizOutput -- | Internal GD library format. Gd :: GraphvizOutput -- | Compressed version of Gd. Gd2 :: GraphvizOutput -- | Graphics Interchange Format. Gif :: GraphvizOutput -- | Icon image file format. Ico :: GraphvizOutput -- | Server-side imagemap. Imap :: GraphvizOutput -- | Client-side imagemap. Cmapx :: GraphvizOutput -- | As for Imap, except only rectangles are used as active areas. ImapNP :: GraphvizOutput -- | As for Cmapx, except only rectangles are used as active areas. CmapxNP :: GraphvizOutput -- | The JPEG image format. Jpeg :: GraphvizOutput -- | Portable Document Format. Pdf :: GraphvizOutput -- | Simple text format. Plain :: GraphvizOutput -- | As for Plain, but provides port names on head and tail nodes -- when applicable. PlainExt :: GraphvizOutput -- | Portable Network Graphics format. Png :: GraphvizOutput -- | PostScript. Ps :: GraphvizOutput -- | PostScript for PDF. Ps2 :: GraphvizOutput -- | Scalable Vector Graphics format. Svg :: GraphvizOutput -- | Compressed SVG format. SvgZ :: GraphvizOutput -- | Tagged Image File Format. Tiff :: GraphvizOutput -- | Vector Markup Language; Svg is usually preferred. Vml :: GraphvizOutput -- | Compressed VML format; SvgZ is usually preferred. VmlZ :: GraphvizOutput -- | Virtual Reality Modeling Language format; requires nodes to have a -- third dimension set via the Pos attribute (and with a -- Dim value of at least 3). Vrml :: GraphvizOutput -- | Wireless BitMap format; monochrome format usually used for mobile -- computing devices. WBmp :: GraphvizOutput -- | Google's WebP format; requires Graphviz >= 2.29.0. WebP :: GraphvizOutput data Rose a Rose :: a -> Map Pid a -> Rose a printDotGraph :: GraphOptions -> Rose [String] -> IO () instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.DotDrawing.Rose a) instance GHC.Base.Functor Test.StateMachine.DotDrawing.Rose module Test.StateMachine.Types.GenSym data GenSym a runGenSym :: GenSym a -> Counter -> (a, Counter) genSym :: Typeable a => GenSym (Reference a Symbolic) data Counter newCounter :: Counter instance GHC.Show.Show Test.StateMachine.Types.GenSym.Counter instance GHC.Base.Monad Test.StateMachine.Types.GenSym.GenSym instance GHC.Base.Applicative Test.StateMachine.Types.GenSym.GenSym instance GHC.Base.Functor Test.StateMachine.Types.GenSym.GenSym -- | This module contains environments that are used to translate between -- symbolic and concrete references. It's taken from the Hedgehog -- library. module Test.StateMachine.Types.Environment -- | A mapping of symbolic values to concrete values. newtype Environment Environment :: Map Var Dynamic -> Environment [unEnvironment] :: Environment -> Map Var Dynamic -- | Environment errors. data EnvironmentError EnvironmentValueNotFound :: !Var -> EnvironmentError EnvironmentTypeError :: !TypeRep -> !TypeRep -> EnvironmentError -- | Create an empty environment. emptyEnvironment :: Environment -- | Insert a symbolic / concrete pairing in to the environment. insertConcrete :: Var -> Dynamic -> Environment -> Environment insertConcretes :: [Var] -> [Dynamic] -> Environment -> Environment -- | Cast a Dynamic in to a concrete value. reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a) -- | Turns an environment in to a function for looking up a concrete value -- from a symbolic one. reifyEnvironment :: Environment -> forall a. Symbolic a -> Either EnvironmentError (Concrete a) -- | Convert a symbolic structure to a concrete one, using the provided -- environment. reify :: Traversable t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete) instance GHC.Base.Monoid Test.StateMachine.Types.Environment.Environment instance GHC.Base.Semigroup Test.StateMachine.Types.Environment.Environment instance GHC.Show.Show Test.StateMachine.Types.Environment.Environment instance GHC.Show.Show Test.StateMachine.Types.Environment.EnvironmentError instance GHC.Classes.Ord Test.StateMachine.Types.Environment.EnvironmentError instance GHC.Classes.Eq Test.StateMachine.Types.Environment.EnvironmentError module Test.StateMachine.Types data StateMachine model cmd m resp StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Maybe (Gen (cmd Symbolic))) -> (model Symbolic -> cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> (model Concrete -> m ()) -> StateMachine model cmd m resp [initModel] :: StateMachine model cmd m resp -> forall r. model r [transition] :: StateMachine model cmd m resp -> forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r [precondition] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> Logic [postcondition] :: StateMachine model cmd m resp -> model Concrete -> cmd Concrete -> resp Concrete -> Logic [invariant] :: StateMachine model cmd m resp -> Maybe (model Concrete -> Logic) [generator] :: StateMachine model cmd m resp -> model Symbolic -> Maybe (Gen (cmd Symbolic)) [shrinker] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> [cmd Symbolic] [semantics] :: StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete) [mock] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) [cleanup] :: StateMachine model cmd m resp -> model Concrete -> m () -- | Previously symbolically executed command -- -- Invariant: the variables must be the variables in the response. data Command cmd resp Command :: !cmd Symbolic -> !resp Symbolic -> ![Var] -> Command cmd resp getCommand :: Command cmd resp -> cmd Symbolic newtype Commands cmd resp Commands :: [Command cmd resp] -> Commands cmd resp [unCommands] :: Commands cmd resp -> [Command cmd resp] type NParallelCommands = ParallelCommandsF [] lengthCommands :: Commands cmd resp -> Int data ParallelCommandsF t cmd resp ParallelCommands :: !Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp [prefix] :: ParallelCommandsF t cmd resp -> !Commands cmd resp [suffixes] :: ParallelCommandsF t cmd resp -> [t (Commands cmd resp)] type ParallelCommands = ParallelCommandsF Pair data Pair a Pair :: !a -> !a -> Pair a [proj1] :: Pair a -> !a [proj2] :: Pair a -> !a fromPair :: Pair a -> (a, a) toPair :: (a, a) -> Pair a fromPair' :: ParallelCommandsF Pair cmd resp -> ParallelCommandsF [] cmd resp toPairUnsafe' :: ParallelCommandsF [] cmd resp -> ParallelCommandsF Pair cmd resp data Reason Ok :: Reason PreconditionFailed :: String -> Reason PostconditionFailed :: String -> Reason InvariantBroken :: String -> Reason ExceptionThrown :: String -> Reason MockSemanticsMismatch :: String -> Reason isOK :: Reason -> Bool noCleanup :: Monad m => model Concrete -> m () instance GHC.Base.Monoid (Test.StateMachine.Types.Commands cmd resp) instance GHC.Base.Semigroup (Test.StateMachine.Types.Commands cmd resp) instance GHC.Show.Show Test.StateMachine.Types.Reason instance GHC.Classes.Eq Test.StateMachine.Types.Reason instance Data.Traversable.Traversable Test.StateMachine.Types.Pair instance Data.Foldable.Foldable Test.StateMachine.Types.Pair instance GHC.Base.Functor Test.StateMachine.Types.Pair instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Types.Pair a) instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.Pair a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.Pair a) instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Show.Show (Test.StateMachine.Types.Command cmd resp) instance (GHC.Read.Read (cmd Test.StateMachine.Types.References.Symbolic), GHC.Read.Read (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Read.Read (Test.StateMachine.Types.Command cmd resp) instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Classes.Eq (Test.StateMachine.Types.Command cmd resp) instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Show.Show (Test.StateMachine.Types.Commands cmd resp) instance (GHC.Read.Read (cmd Test.StateMachine.Types.References.Symbolic), GHC.Read.Read (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Read.Read (Test.StateMachine.Types.Commands cmd resp) instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Classes.Eq (Test.StateMachine.Types.Commands cmd resp) instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (t (Test.StateMachine.Types.Commands cmd resp))) => GHC.Classes.Eq (Test.StateMachine.Types.ParallelCommandsF t cmd resp) instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (t (Test.StateMachine.Types.Commands cmd resp))) => GHC.Show.Show (Test.StateMachine.Types.ParallelCommandsF t cmd resp) -- | This module exports helpers that are useful for labelling properties. module Test.StateMachine.Labelling data Predicate a b Predicate :: (a -> Either b (Predicate a b)) -> Maybe b -> Predicate a b -- | Given an a, either successfully classify as b or -- continue looking [predApply] :: Predicate a b -> a -> Either b (Predicate a b) -- | End of the string -- -- The predicate is given a final chance to return a value. [predFinish] :: Predicate a b -> Maybe b -- | Construct simply predicate that returns Nothing on termination predicate :: (a -> Either b (Predicate a b)) -> Predicate a b -- | Maximum value found, if any maximum :: forall a b. Ord b => (a -> Maybe b) -> Predicate a b -- | Do a linear scan over the list, returning all successful -- classifications classify :: forall a b. [Predicate a b] -> [a] -> [b] data Event model cmd resp (r :: Type -> Type) Event :: model r -> cmd r -> model r -> resp r -> Event model cmd resp (r :: Type -> Type) [eventBefore] :: Event model cmd resp (r :: Type -> Type) -> model r [eventCmd] :: Event model cmd resp (r :: Type -> Type) -> cmd r [eventAfter] :: Event model cmd resp (r :: Type -> Type) -> model r [eventResp] :: Event model cmd resp (r :: Type -> Type) -> resp r -- | execCmds is just the repeated form of execCmd. execCmds :: forall model cmd m resp. StateMachine model cmd m resp -> Commands cmd resp -> [Event model cmd resp Symbolic] execHistory :: forall model cmd m resp. StateMachine model cmd m resp -> History cmd resp -> [Event model cmd resp Concrete] instance (GHC.Show.Show (model r), GHC.Show.Show (cmd r), GHC.Show.Show (resp r)) => GHC.Show.Show (Test.StateMachine.Labelling.Event model cmd resp r) instance GHC.Base.Functor (Test.StateMachine.Labelling.Predicate a) module Test.StateMachine.ConstructorName -- | The names of all possible commands -- -- This is used for things like tagging, coverage checking, etc. class CommandNames (cmd :: k -> Type) -- | Name of this particular command cmdName :: CommandNames cmd => cmd r -> String -- | Name of all possible commands cmdNames :: CommandNames cmd => Proxy (cmd r) -> [String] -- | Name of this particular command cmdName :: (CommandNames cmd, Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String -- | Name of all possible commands cmdNames :: forall r. (CommandNames cmd, CommandNames (Rep1 cmd)) => Proxy (cmd r) -> [String] -- | Convenience wrapper for Command commandName :: CommandNames cmd => Command cmd resp -> String instance Test.StateMachine.ConstructorName.CommandNames GHC.Generics.U1 instance Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.K1 i c) instance forall k (c :: GHC.Generics.Meta) (f :: k -> *). GHC.Generics.Constructor c => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.C c f) instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.D c f) instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.S c f) instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.CommandNames f, Test.StateMachine.ConstructorName.CommandNames g) => Test.StateMachine.ConstructorName.CommandNames (f GHC.Generics.:+: g) instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.CommandNames f, Test.StateMachine.ConstructorName.CommandNames g) => Test.StateMachine.ConstructorName.CommandNames (f GHC.Generics.:*: g) instance forall k (f :: k -> *). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.Rec1 f) -- | This module contains functions for visualing a history of a parallel -- execution. module Test.StateMachine.BoxDrawer -- | Event invocation or response. data EventType Open :: EventType Close :: EventType data Fork a Fork :: a -> a -> a -> Fork a -- | Given a history, and output from processes generate Doc with boxes exec :: [(EventType, Pid)] -> Fork [String] -> Doc instance GHC.Show.Show Test.StateMachine.BoxDrawer.EventType instance GHC.Base.Functor Test.StateMachine.BoxDrawer.Fork -- | This module exports some QuickCheck utility functions. Some of these -- should perhaps be upstreamed. module Test.StateMachine.Utils -- | Lifts a plain property into a monadic property. liftProperty :: Monad m => Property -> PropertyM m () -- | Lifts whenFail to PropertyM. whenFailM :: Monad m => IO () -> Property -> PropertyM m () -- | Lifts any to properties. anyP :: (a -> Property) -> [a] -> Property suchThatEither :: forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a) collects :: Show a => [a] -> Property -> Property -- | More permissive notion of shrinking where a value can shrink to itself -- -- For example -- -- 
--   shrink  3 == [0, 2] -- standard QuickCheck shrink
--   shrinkS 3 == [Shrunk True 0, Shrunk True 2, Shrunk False 3]
--
-- -- This is primarily useful when shrinking composite structures: the -- combinators here keep track of whether something was shrunk -- somewhere in the structure. For example, we have -- -- 
--      shrinkListS (shrinkPairS shrinkS shrinkS) [(1,3),(2,4)]
--   == [ Shrunk True  []             -- removed all elements of the list
--      , Shrunk True  [(2,4)]        -- removed the first
--      , Shrunk True  [(1,3)]        -- removed the second
--      , Shrunk True  [(0,3),(2,4)]  -- shrinking the '1'
--      , Shrunk True  [(1,0),(2,4)]  -- shrinking the '3'
--      , Shrunk True  [(1,2),(2,4)]  -- ..
--      , Shrunk True  [(1,3),(0,4)]  -- shrinking the '2'
--      , Shrunk True  [(1,3),(1,4)]  -- ..
--      , Shrunk True  [(1,3),(2,0)]  -- shrinking the '4'
--      , Shrunk True  [(1,3),(2,2)]  -- ..
--      , Shrunk True  [(1,3),(2,3)]  -- ..
--      , Shrunk False [(1,3),(2,4)]  -- the original unchanged list
--      ]
--
data Shrunk a Shrunk :: Bool -> a -> Shrunk a [wasShrunk] :: Shrunk a -> Bool [shrunk] :: Shrunk a -> a shrinkS :: Arbitrary a => a -> [Shrunk a] shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]] -- | Shrink list without shrinking elements. shrinkListS' :: [a] -> [Shrunk [a]] -- | Shrink list by only shrinking elements. shrinkListS'' :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]] shrinkPairS :: (a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)] shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)] pickOneReturnRest :: [a] -> [(a, [a])] pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a], [a]))] pickOneReturnRestL :: [[a]] -> [(a, [[a]])] mkModel :: StateMachine model cmd m resp -> History cmd resp -> model Concrete instance GHC.Base.Functor Test.StateMachine.Utils.Shrunk instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Utils.Shrunk a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Utils.Shrunk a) -- | This module contains helpers for generating, shrinking, and checking -- sequential programs. module Test.StateMachine.Sequential forAllCommands :: 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 -- | Generate commands from a list of generators. existsCommands :: forall model cmd m resp 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 :: (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 m resp. 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 :: (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b getUsedVars :: Foldable f => f Symbolic -> [Var] -- | Shrink commands in a pre-condition and scope respecting way. shrinkCommands :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [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', 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. 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)] -- | Environment required during shrinkAndValidate data ValidateEnv model ValidateEnv :: model Symbolic -> Map Var Var -> Counter -> ValidateEnv model -- | The model we're starting validation from [veModel] :: ValidateEnv model -> model Symbolic -- | 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. [veScope] :: ValidateEnv model -> Map Var Var -- | Counter (for generating new references) [veCounter] :: ValidateEnv model -> Counter data ShouldShrink MustShrink :: ShouldShrink DontShrink :: ShouldShrink initValidateEnv :: model Symbolic -> ValidateEnv model runCommands :: (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) runCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => m (StateMachine model cmd m resp) -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) runCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => 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 :: Check CheckEverything :: Check CheckNothing :: Check executeCommands :: (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 cmd m resp. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO () prettyPrintHistory' :: forall model cmd m resp tag. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete), ToExpr tag) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd 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 () -- | Variant of prettyCommands that also prints the tags -- covered by each command. prettyCommands' :: (MonadIO m, ToExpr (model Concrete), ToExpr 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 :: (Show (cmd Symbolic), Show (resp Symbolic)) => FilePath -> Commands cmd resp -> Property -> Property runSavedCommands :: (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 resp. CommandNames cmd => Commands cmd resp -> [(String, Int)] commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String] -- | Fail if some commands have not been executed. coverCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property -- | Print the percentage of each command used. The prefix check is an -- unfortunate remaining for backwards compatibility. checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property showLabelledExamples :: (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 () -- | Show minimal examples for each of the generated tags. showLabelledExamples' :: (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 () -- | This module contains helpers for generating, shrinking, and checking -- parallel programs. -- -- Note that: -- -- module Test.StateMachine.Parallel forAllNParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Int -> (NParallelCommands cmd resp -> prop) -> Property forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property generateNParallelCommands :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp) -- | Generate parallel commands. -- -- Parallel commands are generated as follows. We begin by generating -- sequential commands and then splitting this list in two at some index. -- The first half will be used as the prefix. -- -- The second half will be used to build suffixes. For example, starting -- from the following sequential commands: -- -- 
--   [A, B, C, D, E, F, G, H, I]
--
-- -- We split it in two, giving us the prefix and the rest: -- -- 
--   prefix: [A, B]
--   rest:   [C, D, E, F, G, H, I]
--
-- -- We advance the model with the prefix. -- -- Make a suffix: we take commands from rest as long as -- these are parallel safe (see parallelSafe). This means that the -- pre-conditions (using the 'advanced' model) of each of those commands -- will hold no matter in which order they are executed. -- -- Say this is true for [C, D, E], but not anymore for -- F, maybe because F depends on one of [C, D, -- E]. Then we divide this 'chunk' in two by splitting it in the -- middle, obtaining [C] and [D, E]. These two halves -- of the chunk (stored as a Pair) will later be executed in -- parallel. Together they form one suffix. -- -- Then the model is advanced using the whole chunk [C, D, E]. -- Think of it as a barrier after executing the two halves of the chunk -- in parallel. Then this process of building a chunk/suffix repeats -- itself, starting from Make a suffix using the 'advanced' model. -- -- In the end we might end up with something like this: -- -- 
--           ┌─ [C] ──┐  ┌ [F, G] ┐
--   [A, B] ─┤        ├──┤        │
--           └ [D, E] ┘  └ [H, I] ┘
--
generateParallelCommands :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp) -- | Shrink a parallel program in a pre-condition and scope respecting way. shrinkNParallelCommands :: forall cmd model m resp. Traversable cmd => Foldable resp => StateMachine model cmd m resp -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] -- | Shrink a parallel program in a pre-condition and scope respecting way. shrinkParallelCommands :: forall cmd model m resp. Traversable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] shrinkAndValidateNParallel :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] shrinkAndValidateParallel :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] -- | Shrinks Commands in a way that it has strictly less number of -- commands. shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)] runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] executeParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) -- | Try to linearise a history of a parallel program execution using a -- sequential model. See the *Linearizability: a correctness condition -- for concurrent objects* paper linked to from the README for more info. linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic -- | Draw an ASCII diagram of the history of a parallel program. Useful for -- seeing how a race condition might have occured. toBoxDrawings :: forall cmd resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m () prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => ParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m () -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyParallelCommandsWithOpts :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m () -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m () -- | Apply the transition of some commands to a model. advanceModel :: StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic -- | Print the percentage of each command used. The prefix check is an -- unfortunate remaining for backwards compatibility. checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property -- | Fail if some commands have not been executed. coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> [(String, Int)] -- | The main module for state machine based testing, it contains -- combinators that help you build sequential and parallel properties. module Test.StateMachine forAllCommands :: 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 -- | Generate commands from a list of generators. existsCommands :: forall model cmd m resp 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 runCommands :: (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) runCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => m (StateMachine model cmd m resp) -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m () -- | Variant of prettyCommands that also prints the tags -- covered by each command. prettyCommands' :: (MonadIO m, ToExpr (model Concrete), ToExpr 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 () -- | Print the percentage of each command used. The prefix check is an -- unfortunate remaining for backwards compatibility. checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property -- | Fail if some commands have not been executed. coverCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property commandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [(String, Int)] commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String] saveCommands :: (Show (cmd Symbolic), Show (resp Symbolic)) => FilePath -> Commands cmd resp -> Property -> Property runSavedCommands :: (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) showLabelledExamples :: (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 () -- | Show minimal examples for each of the generated tags. showLabelledExamples' :: (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 () noCleanup :: Monad m => model Concrete -> m () forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property forAllNParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Int -> (NParallelCommands cmd resp -> prop) -> Property runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] runNParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)] prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m () prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => ParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m () -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyParallelCommandsWithOpts :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m () -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m () -- | Print the percentage of each command used. The prefix check is an -- unfortunate remaining for backwards compatibility. checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property -- | Fail if some commands have not been executed. coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> [(String, Int)] data StateMachine model cmd m resp StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Maybe (Gen (cmd Symbolic))) -> (model Symbolic -> cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> (model Concrete -> m ()) -> StateMachine model cmd m resp data Concrete a data Symbolic a data Reference a r concrete :: Reference a Concrete -> a reference :: Typeable a => a -> Reference a Concrete newtype Opaque a Opaque :: a -> Opaque a [unOpaque] :: Opaque a -> a opaque :: Reference (Opaque a) Concrete -> a data Reason Ok :: Reason PreconditionFailed :: String -> Reason PostconditionFailed :: String -> Reason InvariantBroken :: String -> Reason ExceptionThrown :: String -> Reason MockSemanticsMismatch :: String -> Reason data GenSym a genSym :: Typeable a => GenSym (Reference a Symbolic) -- | The names of all possible commands -- -- This is used for things like tagging, coverage checking, etc. class CommandNames (cmd :: k -> Type) -- | Name of this particular command cmdName :: CommandNames cmd => cmd r -> String -- | Name of all possible commands cmdNames :: CommandNames cmd => Proxy (cmd r) -> [String] -- | Name of this particular command cmdName :: (CommandNames cmd, Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String -- | Name of all possible commands cmdNames :: forall r. (CommandNames cmd, CommandNames (Rep1 cmd)) => Proxy (cmd r) -> [String] -- | toExpr converts a Haskell value into untyped Haskell-like -- syntax tree, Expr. -- -- 
--   >>> toExpr ((1, Just 2) :: (Int, Maybe Int))
--   App "_\215_" [App "1" [],App "Just" [App "2" []]]
--
class ToExpr a toExpr :: ToExpr a => a -> Expr module Test.StateMachine.Lockstep.NAry -- | Mock state -- -- The t argument (here and elsewhere) is a type-level tag that -- combines all aspects of the test; it does not need any term-level -- constructors -- -- 
--   data MyTest
--   type instance MockState MyTest = ..
--
type family MockState t :: Type -- | Commands -- -- In Cmd t f hs, hs is the list of real handle types, -- and f is some functor applied to each of them. Two typical -- instantiations are -- -- 
--   Cmd t I              (RealHandles t)   -- for the system under test
--   Cmd t (MockHandle t) (RealHandles t)   -- for the mock
--
data family Cmd t :: (Type -> Type) -> [Type] -> Type -- | Responses -- -- The type arguments are similar to those of Cmd. Two typical -- instances: -- -- 
--   Resp t I              (RealHandles t)  -- for the system under test
--   Resp t (MockHandle t) (RealHandles t)  -- for the mock
--
data family Resp t :: (Type -> Type) -> [Type] -> Type -- | Type-level list of the types of the handles in the system under test -- -- NOTE: If your system under test only requires a single real handle, -- you might consider using Test.StateMachine.Lockstep.Simple -- instead. type family RealHandles t :: [Type] -- | Mock handles -- -- For each real handle a, MockHandle t a is the -- corresponding mock handle. data family MockHandle t a :: Type type family Test (f :: (Type -> Type) -> [Type] -> Type) :: Type -- | Tags -- -- Tags are used when labelling execution runs in prop_sequential, -- as well as when looking for minimal examples with a given label -- (showLabelledExamples). type family Tag t :: Type -- | State machine test -- -- This captures the design patterns sketched in -- https://well-typed.com/blog/2019/01/qsm-in-depth/. data StateMachineTest t m StateMachineTest :: (Cmd t (MockHandle t) (RealHandles t) -> MockState t -> (Resp t (MockHandle t) (RealHandles t), MockState t)) -> (Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))) -> MockState t -> (forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)) -> (Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))) -> (Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]) -> (Model t Concrete -> m ()) -> ([Event t Symbolic] -> [Tag t]) -> StateMachineTest t m [runMock] :: StateMachineTest t m -> Cmd t (MockHandle t) (RealHandles t) -> MockState t -> (Resp t (MockHandle t) (RealHandles t), MockState t) [runReal] :: StateMachineTest t m -> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t)) [initMock] :: StateMachineTest t m -> MockState t [newHandles] :: StateMachineTest t m -> forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t) [generator] :: StateMachineTest t m -> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic)) [shrinker] :: StateMachineTest t m -> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic] [cleanup] :: StateMachineTest t m -> Model t Concrete -> m () [tag] :: StateMachineTest t m -> [Event t Symbolic] -> [Tag t] data Event t r Event :: Model t r -> (Cmd t :@ r) -> Model t r -> Resp t (MockHandle t) (RealHandles t) -> Event t r [before] :: Event t r -> Model t r [cmd] :: Event t r -> Cmd t :@ r [after] :: Event t r -> Model t r [mockResp] :: Event t r -> Resp t (MockHandle t) (RealHandles t) hoistStateMachineTest :: Monad n => (forall a. m a -> n a) -> StateMachineTest t m -> StateMachineTest t n newtype At f r At :: f (FlipRef r) (RealHandles (Test f)) -> At f r [unAt] :: At f r -> f (FlipRef r) (RealHandles (Test f)) type f :@ r = At f r data Model t r Model :: MockState t -> Refss t r -> Model t r [modelState] :: Model t r -> MockState t [modelRefss] :: Model t r -> Refss t r -- | Relation between real and mock references for single handle type -- a newtype Refs t r a Refs :: [(Reference a r, MockHandle t a)] -> Refs t r a [unRefs] :: Refs t r a -> [(Reference a r, MockHandle t a)] -- | Relation between real and mock references for all handle types newtype Refss t r Refss :: NP (Refs t r) (RealHandles t) -> Refss t r [unRefss] :: Refss t r -> NP (Refs t r) (RealHandles t) newtype FlipRef r h FlipRef :: Reference h r -> FlipRef r h [unFlipRef] :: FlipRef r h -> Reference h r -- | Sequential test prop_sequential :: forall t. StateMachineTest t IO -> Maybe Int -> Property -- | Parallel test -- -- NOTE: This currently does not do labelling. prop_parallel :: StateMachineTest t IO -> Maybe Int -> Property -- | Show minimal examples for each of the generated tags. -- -- This is the analogue of showLabelledExamples'. See also -- showLabelledExamples. showLabelledExamples' :: StateMachineTest t m -> Maybe Int -> Int -> (Tag t -> Bool) -> IO () -- | Simplified form of showLabelledExamples' showLabelledExamples :: StateMachineTest t m -> IO () toStateMachine :: StateMachineTest t m -> StateMachine (Model t) (At (Cmd t)) m (At (Resp t)) instance GHC.Generics.Generic (Test.StateMachine.Lockstep.NAry.Refs t r a) instance GHC.Base.Monoid (Test.StateMachine.Lockstep.NAry.Refs t r a) instance GHC.Base.Semigroup (Test.StateMachine.Lockstep.NAry.Refs t r a) instance (Data.Functor.Classes.Show1 r, GHC.Show.Show h) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.FlipRef r h) instance GHC.Generics.Generic (Test.StateMachine.Lockstep.NAry.Model t r) instance (Data.Functor.Classes.Show1 r, GHC.Show.Show a, GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle t a)) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Refs t r a) instance (Test.StateMachine.TreeDiff.Class.ToExpr a, Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle t a)) => Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.Refs t Test.StateMachine.Types.References.Concrete a) instance GHC.Show.Show (f (Test.StateMachine.Lockstep.NAry.FlipRef r) (Test.StateMachine.Lockstep.NAry.RealHandles (Test.StateMachine.Lockstep.NAry.Test f))) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.At f r) instance (Data.Functor.Classes.Show1 r, GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockState t), Data.SOP.Constraint.All (Data.SOP.Constraint.And GHC.Show.Show (Data.SOP.Constraint.Compose GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t)) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Model t r) instance (Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockState t), Data.SOP.Constraint.All (Data.SOP.Constraint.And Test.StateMachine.TreeDiff.Class.ToExpr (Data.SOP.Constraint.Compose Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.Model t Test.StateMachine.Types.References.Concrete) instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Functor (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Cmd t)) instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Foldable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Cmd t)) instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Traversable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Cmd t)) instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Functor (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Resp t)) instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Foldable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Resp t)) instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Traversable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Resp t)) instance (Data.Functor.Classes.Show1 r, Data.SOP.Constraint.All (Data.SOP.Constraint.And GHC.Show.Show (Data.SOP.Constraint.Compose GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t)) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Refss t r) instance Data.SOP.Constraint.All (Data.SOP.Constraint.And Test.StateMachine.TreeDiff.Class.ToExpr (Data.SOP.Constraint.Compose Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t) => Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.Refss t Test.StateMachine.Types.References.Concrete) instance Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t) => GHC.Base.Semigroup (Test.StateMachine.Lockstep.NAry.Refss t r) instance Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t) => GHC.Base.Monoid (Test.StateMachine.Lockstep.NAry.Refss t r) module Test.StateMachine.Lockstep.Simple -- | Mock state -- -- The t argument (here and elsewhere) is a type-level tag that -- combines all aspects of the test; it does not need any term-level -- constructors -- -- 
--   data MyTest
--   type instance MockState MyTest = ..
--
type family MockState t :: Type -- | Commands -- -- In Cmd t h, h is the type of the handle -- -- 
--   Cmd t (RealHandle t)  -- for the system under test
--   Cmd t (MockHandle t)  -- for the mock
--
data family Cmd t :: Type -> Type -- | Responses -- -- In Resp t h, h is the type of the handle -- -- 
--   Resp t (RealHandle t)  -- for the system under test
--   Resp t (MockHandle t)  -- for the mock
--
data family Resp t :: Type -> Type -- | The type of the real handle in the system under test -- -- The key difference between the " simple " lockstep infrastructure and -- the n-ary lockstep infrastructure is that the former only supports a -- single real handle, whereas the latter supports an arbitrary list of -- them. data family RealHandle t :: Type -- | The type of the mock handle -- -- NOTE: In the n-ary infrastructure, MockHandle is a type family -- of two arguments, because we have a mock handle for each real -- handle. Here, however, we only have a single real handle, so -- the " corresponding " real handle is implicitly RealHandle t. data family MockHandle t :: Type type family Test (f :: Type -> Type) :: Type -- | Tags -- -- Tags are used when labelling execution runs in prop_sequential, -- as well as when looking for minimal examples with a given label -- (showLabelledExamples). type family Tag t :: Type -- | State machine test -- -- This captures the design patterns sketched in -- https://well-typed.com/blog/2019/01/qsm-in-depth/ for the case -- where there is exactly one real handle. See -- Test.StateMachine.Lockstep.NAry for the generalization to -- n handles. data StateMachineTest t StateMachineTest :: (Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t)) -> (Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))) -> MockState t -> (forall h. Resp t h -> [h]) -> (Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))) -> (Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]) -> (Model t Concrete -> IO ()) -> ([Event t Symbolic] -> [Tag t]) -> StateMachineTest t [runMock] :: StateMachineTest t -> Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t) [runReal] :: StateMachineTest t -> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t)) [initMock] :: StateMachineTest t -> MockState t [newHandles] :: StateMachineTest t -> forall h. Resp t h -> [h] [generator] :: StateMachineTest t -> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic)) [shrinker] :: StateMachineTest t -> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic] [cleanup] :: StateMachineTest t -> Model t Concrete -> IO () [tag] :: StateMachineTest t -> [Event t Symbolic] -> [Tag t] data Event t r Event :: Model t r -> (Cmd t :@ r) -> Model t r -> Resp t (MockHandle t) -> Event t r [before] :: Event t r -> Model t r [cmd] :: Event t r -> Cmd t :@ r [after] :: Event t r -> Model t r [mockResp] :: Event t r -> Resp t (MockHandle t) newtype At f r At :: f (Reference (RealHandle (Test f)) r) -> At f r [unAt] :: At f r -> f (Reference (RealHandle (Test f)) r) type f :@ r = At f r data Model t r Model :: MockState t -> [(Reference (RealHandle t) r, MockHandle t)] -> Model t r [modelState] :: Model t r -> MockState t [modelRefs] :: Model t r -> [(Reference (RealHandle t) r, MockHandle t)] prop_sequential :: StateMachineTest t -> Maybe Int -> Property prop_parallel :: StateMachineTest t -> Maybe Int -> Property fromSimple :: StateMachineTest t -> StateMachineTest (Simple t) IO instance GHC.Classes.Eq (Test.StateMachine.Lockstep.Simple.MockHandle t) => GHC.Classes.Eq (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.Simple.RealHandle t)) instance GHC.Show.Show (Test.StateMachine.Lockstep.Simple.MockHandle t) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.Simple.RealHandle t)) instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Resp t), GHC.Classes.Eq (Test.StateMachine.Lockstep.Simple.Resp t (Test.StateMachine.Lockstep.Simple.MockHandle t)), GHC.Classes.Eq (Test.StateMachine.Lockstep.Simple.MockHandle t)) => GHC.Classes.Eq (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t)) '[Test.StateMachine.Lockstep.Simple.RealHandle t]) instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Resp t), GHC.Show.Show (Test.StateMachine.Lockstep.Simple.Resp t (Test.StateMachine.Lockstep.Simple.MockHandle t))) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t)) '[Test.StateMachine.Lockstep.Simple.RealHandle t]) instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Resp t), GHC.Show.Show (Test.StateMachine.Lockstep.Simple.Resp t (Test.StateMachine.Types.References.Reference (Test.StateMachine.Lockstep.Simple.RealHandle t) r)), Data.Functor.Classes.Show1 r) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.FlipRef r) '[Test.StateMachine.Lockstep.Simple.RealHandle t]) instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Cmd t), GHC.Show.Show (Test.StateMachine.Lockstep.Simple.Cmd t (Test.StateMachine.Types.References.Reference (Test.StateMachine.Lockstep.Simple.RealHandle t) r)), Data.Functor.Classes.Show1 r) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Cmd (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.FlipRef r) '[Test.StateMachine.Lockstep.Simple.RealHandle t]) instance Data.Traversable.Traversable (Test.StateMachine.Lockstep.Simple.Resp t) => Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t)) instance Data.Traversable.Traversable (Test.StateMachine.Lockstep.Simple.Cmd t) => Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd (Test.StateMachine.Lockstep.Simple.Simple t)) instance Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.Simple.MockHandle t) => Test.StateMachine.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.Simple.RealHandle t)) -- | This module contains Z-inspried combinators for working with -- relations. The idea is that they can be used to define concise and -- showable models. This module is an experiment and will likely change -- or move to its own package. module Test.StateMachine.Z cons :: a -> [a] -> [a] union :: Eq a => [a] -> [a] -> [a] infixr 6 `union` intersect :: Eq a => [a] -> [a] -> [a] infixr 7 `intersect` -- | Subset. -- -- 
--   >>> boolean ([1, 2] `isSubsetOf` [3, 2, 1])
--   True
--
isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic infix 5 `isSubsetOf` -- | Set equality. -- -- 
--   >>> boolean ([1, 1, 2] ~= [2, 1])
--   True
--
(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic infix 5 ~= -- | Relations. type Rel a b = [(a, b)] -- | (Partial) functions. type Fun a b = Rel a b type a :<-> b = Rel a b infixr 1 :<-> type a :-> b = Fun a b infixr 1 :-> type a :/-> b = Fun a b infixr 1 :/-> empty :: Rel a b identity :: [a] -> Rel a a singleton :: a -> b -> Rel a b domain :: Rel a b -> [a] codomain :: Rel a b -> [b] compose :: Eq b => Rel b c -> Rel a b -> Rel a c fcompose :: Eq b => Rel a b -> Rel b c -> Rel a c inverse :: Rel a b -> Rel b a lookupDom :: Eq a => a -> Rel a b -> [b] lookupCod :: Eq b => b -> Rel a b -> [a] -- | Domain restriction. -- -- 
--   >>> ['a'] <| [ ('a', "apa"), ('b', "bepa") ]
--   [('a',"apa")]
--
(<|) :: Eq a => [a] -> Rel a b -> Rel a b infixr 4 <| -- | Codomain restriction. -- -- 
--   >>> [ ('a', "apa"), ('b', "bepa") ] |> ["apa"]
--   [('a',"apa")]
--
(|>) :: Eq b => Rel a b -> [b] -> Rel a b infixl 4 |> -- | Domain substraction. -- -- 
--   >>> ['a'] <-| [ ('a', "apa"), ('b', "bepa") ]
--   [('b',"bepa")]
--
(<-|) :: Eq a => [a] -> Rel a b -> Rel a b infixr 4 <-| -- | Codomain substraction. -- -- 
--   >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"]
--   [('b',"bepa"),('c',"cepa")]
--
-- -- 
--   >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa", "cepa"]
--   [('b',"bepa")]
--
-- -- 
--   >>> [ ('a', "apa"), ('b', "bepa"), ('c', "cepa") ] |-> ["apa"] |-> ["cepa"]
--   [('b',"bepa")]
--
(|->) :: Eq b => Rel a b -> [b] -> Rel a b infixl 4 |-> -- | The image of a relation. image :: Eq a => Rel a b -> [a] -> [b] -- | Overriding. -- -- 
--   >>> [('a', "apa")] <+ [('a', "bepa")]
--   [('a',"bepa")]
--
-- -- 
--   >>> [('a', "apa")] <+ [('b', "bepa")]
--   [('a',"apa"),('b',"bepa")]
--
(<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b infixr 4 <+ -- | Direct product. (<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c) infixl 4 <**> -- | Parallel product. (<||>) :: Rel a c -> Rel b d -> Rel (a, b) (c, d) infixl 4 <||> isTotalRel :: (Eq a, Show a) => Rel a b -> [a] -> Logic isSurjRel :: (Eq b, Show b) => Rel a b -> [b] -> Logic isTotalSurjRel :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic isPartialFun :: (Eq a, Eq b, Show b) => Rel a b -> Logic isTotalFun :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic isPartialInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> Logic isTotalInj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> Logic isPartialSurj :: (Eq a, Eq b, Show b) => Rel a b -> [b] -> Logic isTotalSurj :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic isBijection :: (Eq a, Eq b, Show a, Show b) => Rel a b -> [a] -> [b] -> Logic -- | Application. (!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b (!?) :: Eq a => Fun a b -> a -> Maybe b (.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b infixr 4 .% (.!) :: Rel a b -> a -> (Rel a b, a) infixr 9 .! -- | Assignment. -- -- 
--   >>> singleton 'a' "apa" .! 'a' .= "bepa"
--   [('a',"bepa")]
--
-- -- 
--   >>> singleton 'a' "apa" .! 'b' .= "bepa"
--   [('a',"apa"),('b',"bepa")]
--
(.=) :: (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b infix 4 .=