{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
module Test.StateMachine.Utils
( liftProperty
, whenFailM
, anyP
, suchThatEither
, collects
, Shrunk(..)
, shrinkS
, shrinkListS
, shrinkListS'
, shrinkListS''
, shrinkPairS
, shrinkPairS'
, pickOneReturnRest
, pickOneReturnRest2
, pickOneReturnRestL
, mkModel
)
where
import Prelude
import Data.Bifunctor (second)
import Data.List
(foldl')
import Test.QuickCheck
(Arbitrary, Gen, Property, collect, resize, shrink,
shrinkList, sized, whenFail)
import Test.QuickCheck.Monadic
(PropertyM(MkPropertyM))
import Test.QuickCheck.Property
(property, (.&&.), (.||.))
import Test.StateMachine.Types
liftProperty :: Monad m => Property -> PropertyM m ()
liftProperty :: forall (m :: * -> *). Monad m => Property -> PropertyM m ()
liftProperty Property
prop = forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (\() -> Gen (m Property)
k -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Property
prop forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&.) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> Gen (m Property)
k ())
whenFailM :: Monad m => IO () -> Property -> PropertyM m ()
whenFailM :: forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
whenFailM IO ()
m Property
prop = forall (m :: * -> *). Monad m => Property -> PropertyM m ()
liftProperty (IO ()
m forall prop. Testable prop => IO () -> prop -> Property
`whenFail` Property
prop)
anyP :: (a -> Property) -> [a] -> Property
anyP :: forall a. (a -> Property) -> [a] -> Property
anyP a -> Property
p = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x Property
ih -> a -> Property
p a
x forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. Property
ih) (forall prop. Testable prop => prop -> Property
property Bool
False)
suchThatEither :: forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
Gen a
gen suchThatEither :: forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
`suchThatEither` a -> Bool
p = forall a. (Int -> Gen a) -> Gen a
sized ([a] -> Int -> Int -> Gen (Either [a] a)
try [] Int
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> a -> a
max Int
100)
where
try :: [a] -> Int -> Int -> Gen (Either [a] a)
try :: [a] -> Int -> Int -> Gen (Either [a] a)
try [a]
ces Int
_ Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left (forall a. [a] -> [a]
reverse [a]
ces))
try [a]
ces Int
k Int
n = do
a
x <- forall a. Int -> Gen a -> Gen a
resize (Int
2 forall a. Num a => a -> a -> a
* Int
k forall a. Num a => a -> a -> a
+ Int
n) Gen a
gen
if a -> Bool
p a
x
then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right a
x)
else [a] -> Int -> Int -> Gen (Either [a] a)
try (a
x forall a. a -> [a] -> [a]
: [a]
ces) (Int
k forall a. Num a => a -> a -> a
+ Int
1) (Int
n forall a. Num a => a -> a -> a
- Int
1)
collects :: Show a => [a] -> Property -> Property
collects :: forall a. Show a => [a] -> Property -> Property
collects = forall a b. (a -> b -> b) -> [a] -> b -> b
repeatedly forall a prop. (Show a, Testable prop) => a -> prop -> Property
collect
where
repeatedly :: (a -> b -> b) -> ([a] -> b -> b)
repeatedly :: forall a b. (a -> b -> b) -> [a] -> b -> b
repeatedly = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip
data Shrunk a = Shrunk { forall a. Shrunk a -> Bool
wasShrunk :: Bool, forall a. Shrunk a -> a
shrunk :: a }
deriving stock (Shrunk a -> Shrunk a -> Bool
forall a. Eq a => Shrunk a -> Shrunk a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Shrunk a -> Shrunk a -> Bool
$c/= :: forall a. Eq a => Shrunk a -> Shrunk a -> Bool
== :: Shrunk a -> Shrunk a -> Bool
$c== :: forall a. Eq a => Shrunk a -> Shrunk a -> Bool
Eq, Int -> Shrunk a -> ShowS
forall a. Show a => Int -> Shrunk a -> ShowS
forall a. Show a => [Shrunk a] -> ShowS
forall a. Show a => Shrunk a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Shrunk a] -> ShowS
$cshowList :: forall a. Show a => [Shrunk a] -> ShowS
show :: Shrunk a -> String
$cshow :: forall a. Show a => Shrunk a -> String
showsPrec :: Int -> Shrunk a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Shrunk a -> ShowS
Show, forall a b. a -> Shrunk b -> Shrunk a
forall a b. (a -> b) -> Shrunk a -> Shrunk b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Shrunk b -> Shrunk a
$c<$ :: forall a b. a -> Shrunk b -> Shrunk a
fmap :: forall a b. (a -> b) -> Shrunk a -> Shrunk b
$cfmap :: forall a b. (a -> b) -> Shrunk a -> Shrunk b
Functor)
shrinkS :: Arbitrary a => a -> [Shrunk a]
shrinkS :: forall a. Arbitrary a => a -> [Shrunk a]
shrinkS a
a = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Bool -> a -> Shrunk a
Shrunk Bool
True) (forall a. Arbitrary a => a -> [a]
shrink a
a) forall a. [a] -> [a] -> [a]
++ [forall a. Bool -> a -> Shrunk a
Shrunk Bool
False a
a]
shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS a -> [Shrunk a]
f = \[a]
xs -> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
forall a b. (a -> b) -> [a] -> [b]
map (forall a. Bool -> a -> Shrunk a
Shrunk Bool
True) (forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (forall a b. a -> b -> a
const []) [a]
xs)
, [a] -> [Shrunk [a]]
shrinkOne [a]
xs
, [forall a. Bool -> a -> Shrunk a
Shrunk Bool
False [a]
xs]
]
where
shrinkOne :: [a] -> [Shrunk [a]]
shrinkOne :: [a] -> [Shrunk [a]]
shrinkOne [] = []
shrinkOne (a
x:[a]
xs) = [forall a. Bool -> a -> Shrunk a
Shrunk Bool
True (a
x' forall a. a -> [a] -> [a]
: [a]
xs) | Shrunk Bool
True a
x' <- a -> [Shrunk a]
f a
x]
forall a. [a] -> [a] -> [a]
++ [forall a. Bool -> a -> Shrunk a
Shrunk Bool
True (a
x forall a. a -> [a] -> [a]
: [a]
xs') | Shrunk Bool
True [a]
xs' <- [a] -> [Shrunk [a]]
shrinkOne [a]
xs]
shrinkListS' :: [a] -> [Shrunk [a]]
shrinkListS' :: forall a. [a] -> [Shrunk [a]]
shrinkListS' = forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS (\a
a -> [forall a. Bool -> a -> Shrunk a
Shrunk Bool
False a
a])
shrinkListS'' :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS'' :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS'' a -> [Shrunk a]
f [a]
xs =
let shr :: [Shrunk [a]]
shr = forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS a -> [Shrunk a]
f [a]
xs
len :: Int
len = forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs
in forall a. (a -> Bool) -> [a] -> [a]
filter (\Shrunk [a]
s -> forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Shrunk a -> a
shrunk Shrunk [a]
s) forall a. Eq a => a -> a -> Bool
== Int
len) [Shrunk [a]]
shr
shrinkPairS :: (a -> [Shrunk a])
-> (b -> [Shrunk b])
-> (a, b) -> [Shrunk (a, b)]
shrinkPairS :: forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS a -> [Shrunk a]
f b -> [Shrunk b]
g (a
a, b
b) =
[forall a. Bool -> a -> Shrunk a
Shrunk Bool
True (a
a', b
b) | Shrunk Bool
True a
a' <- a -> [Shrunk a]
f a
a ]
forall a. [a] -> [a] -> [a]
++ [forall a. Bool -> a -> Shrunk a
Shrunk Bool
True (a
a, b
b') | Shrunk Bool
True b
b' <- b -> [Shrunk b]
g b
b ]
forall a. [a] -> [a] -> [a]
++ [forall a. Bool -> a -> Shrunk a
Shrunk Bool
False (a
a, b
b)]
shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
shrinkPairS' :: forall a. (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
shrinkPairS' a -> [Shrunk a]
f = forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS a -> [Shrunk a]
f a -> [Shrunk a]
f
pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a],[a]))]
pickOneReturnRest2 :: forall a. ([a], [a]) -> [(a, ([a], [a]))]
pickOneReturnRest2 ([a]
xs, [a]
ys) =
forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (,[a]
ys)) (forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
xs) forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([a]
xs,)) (forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
ys)
pickOneReturnRest :: [a] -> [(a, [a])]
pickOneReturnRest :: forall a. [a] -> [(a, [a])]
pickOneReturnRest [] = []
pickOneReturnRest (a
x : [a]
xs) = (a
x, [a]
xs) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
x forall a. a -> [a] -> [a]
:)) (forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
xs)
pickOneReturnRestL :: [[a]] -> [(a, [[a]])]
pickOneReturnRestL :: forall a. [[a]] -> [(a, [[a]])]
pickOneReturnRestL [[a]]
ls = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
(\([[a]]
prev, [a]
as, [[a]]
next) -> (\(a
a, [a]
rest) -> (a
a, [[a]]
prev forall a. [a] -> [a] -> [a]
++ [[a]
rest] forall a. [a] -> [a] -> [a]
++ [[a]]
next)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
as)
forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [([a], a, [a])]
splitEach [[a]]
ls
where
splitEach :: [a] -> [([a], a, [a])]
splitEach :: forall a. [a] -> [([a], a, [a])]
splitEach [] = []
splitEach (a
a : [a]
as) = (\([a]
prev, a
a', [a]
next) -> ([a]
prev, a
a', [a]
next)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
go' [([], a
a, [a]
as)] ([], a
a, [a]
as)
where
go' :: [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
go' :: forall a. [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
go' [([a], a, [a])]
acc ([a]
_, a
_, []) = forall a. [a] -> [a]
reverse [([a], a, [a])]
acc
go' [([a], a, [a])]
acc ([a]
prev, a
a', a
b : [a]
next) =
let newElem :: ([a], a, [a])
newElem = (a
a' forall a. a -> [a] -> [a]
: [a]
prev, a
b, [a]
next)
in forall a. [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
go' (([a], a, [a])
newElem forall a. a -> [a] -> [a]
: [([a], a, [a])]
acc) ([a], a, [a])
newElem
mkModel :: StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine {forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition, forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel} =
model Concrete -> [Operation cmd resp] -> model Concrete
go forall (r :: * -> *). model r
initModel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Forest (Operation cmd resp) -> [Operation cmd resp]
operationsPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> Forest (Operation cmd resp)
interleavings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
where
go :: model Concrete -> [Operation cmd resp] -> model Concrete
go model Concrete
m [] = model Concrete
m
go model Concrete
m (Operation cmd Concrete
cmd resp Concrete
resp Pid
_ : [Operation cmd resp]
rest) = model Concrete -> [Operation cmd resp] -> model Concrete
go (forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
m cmd Concrete
cmd resp Concrete
resp) [Operation cmd resp]
rest
go model Concrete
m (Crash {} : [Operation cmd resp]
rest) = model Concrete -> [Operation cmd resp] -> model Concrete
go model Concrete
m [Operation cmd resp]
rest