{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DerivingStrategies  #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE ScopedTypeVariables #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Utils
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH, Li-yao Xia
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module exports some QuickCheck utility functions. Some of these should
-- perhaps be upstreamed.
--
-----------------------------------------------------------------------------

module Test.StateMachine.Utils
  ( liftProperty
  , whenFailM
  , anyP
  , suchThatEither
  , collects
  , Shrunk(..)
  , shrinkS
  , shrinkListS
  , shrinkListS'
  , shrinkListS''
  , shrinkPairS
  , shrinkPairS'
  , pickOneReturnRest
  , pickOneReturnRest2
  , pickOneReturnRestL
  , mkModel
  )
  where

import           Prelude

import           Control.Arrow
                   ((***))
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

------------------------------------------------------------------------

-- | Lifts a plain property into a monadic property.
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 ())

-- | Lifts 'whenFail' to 'PropertyM'.
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)

-- | Lifts 'Prelude.any' to properties.
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

-----------------------------------------------------------------------------

-- | 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 { 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]

-- | Shrink list without shrinking elements.
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])

-- | Shrink list by only shrinking elements.
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 ([], []) == []
-- >    pickOneReturnRest2 ([1,2], [3,4])
-- > == [ (1,([2],[3,4])), (2,([1],[3,4])), (3,([1,2],[4])), (4,([1,2],[3])) ]
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 a. a -> a
id forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) [a]
ys) (forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
xs) forall a. [a] -> [a] -> [a]
++
  forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> a
id forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
***      (,) [a]
xs) (forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
ys)

-- >    pickOneReturnRest []     == []
-- >    pickOneReturnRest [1]    == [ (1,[]) ]
-- >    pickOneReturnRest [1..3] == [ (1,[2,3]), (2,[1,3]), (3,[1,2]) ]
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 a. a -> a
id forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (a
x forall a. a -> [a] -> [a]
:)) (forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
xs)

-- >    pickOneReturnRestL [[]] == []
-- >    pickOneReturnRestL [[1]] == [(1,[[]])]
-- >    pickOneReturnRestL [[1],[],[]] == [(1,[[],[],[]])]
-- >    pickOneReturnRestL [[1,2]] == [(1,[[2]]), (2,[[1]])]
-- >    pickOneReturnRestL [[1,2], [3,4]]
-- > == [ (1,[[2],[3,4]]), (2,[[1],[3,4]]), (3,[[1,2],[4]]), (4,[[1,2],[3]]) ]
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) -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
a, [a]
rest) -> (a
a, [[a]]
prev forall a. [a] -> [a] -> [a]
++ [[a]
rest] forall a. [a] -> [a] -> [a]
++ [[a]]
next)) forall a b. (a -> b) -> a -> 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) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\([a]
prev, a
a', [a]
next) -> ([a]
prev, a
a', [a]
next)) forall a b. (a -> b) -> a -> 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 cmd Concrete
_ String
_ Pid
_ : [Operation cmd resp]
rest) = model Concrete -> [Operation cmd resp] -> model Concrete
go model Concrete
m [Operation cmd resp]
rest