{-# 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 :: Property -> PropertyM m ()
liftProperty Property
prop = ((() -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m ()
forall (m :: * -> *) a.
((a -> Gen (m Property)) -> Gen (m Property)) -> PropertyM m a
MkPropertyM (\() -> Gen (m Property)
k -> (Property -> Property) -> m Property -> m Property
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Property
prop Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&.) (m Property -> m Property) -> Gen (m Property) -> Gen (m 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 :: IO () -> Property -> PropertyM m ()
whenFailM IO ()
m Property
prop = Property -> PropertyM m ()
forall (m :: * -> *). Monad m => Property -> PropertyM m ()
liftProperty (IO ()
m IO () -> Property -> Property
forall prop. Testable prop => IO () -> prop -> Property
`whenFail` Property
prop)

-- | Lifts 'Prelude.any' to properties.
anyP :: (a -> Property) -> [a] -> Property
anyP :: (a -> Property) -> [a] -> Property
anyP a -> Property
p = (a -> Property -> Property) -> Property -> [a] -> Property
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x Property
ih -> a -> Property
p a
x Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. Property
ih) (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False)

suchThatEither :: forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
Gen a
gen suchThatEither :: Gen a -> (a -> Bool) -> Gen (Either [a] a)
`suchThatEither` a -> Bool
p = (Int -> Gen (Either [a] a)) -> Gen (Either [a] a)
forall a. (Int -> Gen a) -> Gen a
sized ([a] -> Int -> Int -> Gen (Either [a] a)
try [] Int
0 (Int -> Gen (Either [a] a))
-> (Int -> Int) -> Int -> Gen (Either [a] a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Int
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 = Either [a] a -> Gen (Either [a] a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> Either [a] a
forall a b. a -> Either a b
Left ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
ces))
    try [a]
ces Int
k Int
n = do
      a
x <- Int -> Gen a -> Gen a
forall a. Int -> Gen a -> Gen a
resize (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Gen a
gen
      if a -> Bool
p a
x
      then Either [a] a -> Gen (Either [a] a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either [a] a
forall a b. b -> Either a b
Right a
x)
      else [a] -> Int -> Int -> Gen (Either [a] a)
try (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ces) (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

collects :: Show a => [a] -> Property -> Property
collects :: [a] -> Property -> Property
collects = (a -> Property -> Property) -> [a] -> Property -> Property
forall a b. (a -> b -> b) -> [a] -> b -> b
repeatedly a -> Property -> Property
forall a prop. (Show a, Testable prop) => a -> prop -> Property
collect
  where
    repeatedly :: (a -> b -> b) -> ([a] -> b -> b)
    repeatedly :: (a -> b -> b) -> [a] -> b -> b
repeatedly = (b -> [a] -> b) -> [a] -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((b -> [a] -> b) -> [a] -> b -> b)
-> ((a -> b -> b) -> b -> [a] -> b)
-> (a -> b -> b)
-> [a]
-> b
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((b -> a -> b) -> b -> [a] -> b)
-> ((a -> b -> b) -> b -> a -> b) -> (a -> b -> b) -> b -> [a] -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> b) -> b -> a -> b
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 { Shrunk a -> Bool
wasShrunk :: Bool, Shrunk a -> a
shrunk :: a }
  deriving stock (Shrunk a -> Shrunk a -> Bool
(Shrunk a -> Shrunk a -> Bool)
-> (Shrunk a -> Shrunk a -> Bool) -> Eq (Shrunk a)
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
[Shrunk a] -> ShowS
Shrunk a -> String
(Int -> Shrunk a -> ShowS)
-> (Shrunk a -> String) -> ([Shrunk a] -> ShowS) -> Show (Shrunk a)
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, a -> Shrunk b -> Shrunk a
(a -> b) -> Shrunk a -> Shrunk b
(forall a b. (a -> b) -> Shrunk a -> Shrunk b)
-> (forall a b. a -> Shrunk b -> Shrunk a) -> Functor Shrunk
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
<$ :: a -> Shrunk b -> Shrunk a
$c<$ :: forall a b. a -> Shrunk b -> Shrunk a
fmap :: (a -> b) -> Shrunk a -> Shrunk b
$cfmap :: forall a b. (a -> b) -> Shrunk a -> Shrunk b
Functor)

shrinkS :: Arbitrary a => a -> [Shrunk a]
shrinkS :: a -> [Shrunk a]
shrinkS a
a = (a -> Shrunk a) -> [a] -> [Shrunk a]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> a -> Shrunk a
forall a. Bool -> a -> Shrunk a
Shrunk Bool
True) (a -> [a]
forall a. Arbitrary a => a -> [a]
shrink a
a) [Shrunk a] -> [Shrunk a] -> [Shrunk a]
forall a. [a] -> [a] -> [a]
++ [Bool -> a -> Shrunk a
forall a. Bool -> a -> Shrunk a
Shrunk Bool
False a
a]

shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS :: (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS a -> [Shrunk a]
f = \[a]
xs -> [[Shrunk [a]]] -> [Shrunk [a]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
      ([a] -> Shrunk [a]) -> [[a]] -> [Shrunk [a]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> [a] -> Shrunk [a]
forall a. Bool -> a -> Shrunk a
Shrunk Bool
True) ((a -> [a]) -> [a] -> [[a]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ([a] -> a -> [a]
forall a b. a -> b -> a
const []) [a]
xs)
    , [a] -> [Shrunk [a]]
shrinkOne [a]
xs
    , [Bool -> [a] -> Shrunk [a]
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) = [Bool -> [a] -> Shrunk [a]
forall a. Bool -> a -> Shrunk a
Shrunk Bool
True (a
x' a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs) | Shrunk Bool
True a
x'  <- a -> [Shrunk a]
f a
x]
                    [Shrunk [a]] -> [Shrunk [a]] -> [Shrunk [a]]
forall a. [a] -> [a] -> [a]
++ [Bool -> [a] -> Shrunk [a]
forall a. Bool -> a -> Shrunk a
Shrunk Bool
True (a
x a -> [a] -> [a]
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' :: [a] -> [Shrunk [a]]
shrinkListS' = (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS (\a
a -> [Bool -> a -> Shrunk 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'' :: (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS'' a -> [Shrunk a]
f [a]
xs =
  let shr :: [Shrunk [a]]
shr = (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS a -> [Shrunk a]
f [a]
xs
      len :: Int
len = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs
  in (Shrunk [a] -> Bool) -> [Shrunk [a]] -> [Shrunk [a]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Shrunk [a]
s -> [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Shrunk [a] -> [a]
forall a. Shrunk a -> a
shrunk Shrunk [a]
s) Int -> Int -> Bool
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 :: (a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS a -> [Shrunk a]
f b -> [Shrunk b]
g (a
a, b
b) =
       [Bool -> (a, b) -> Shrunk (a, 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 ]
    [Shrunk (a, b)] -> [Shrunk (a, b)] -> [Shrunk (a, b)]
forall a. [a] -> [a] -> [a]
++ [Bool -> (a, b) -> Shrunk (a, b)
forall a. Bool -> a -> Shrunk a
Shrunk Bool
True (a
a, b
b') | Shrunk Bool
True b
b' <- b -> [Shrunk b]
g b
b ]
    [Shrunk (a, b)] -> [Shrunk (a, b)] -> [Shrunk (a, b)]
forall a. [a] -> [a] -> [a]
++ [Bool -> (a, b) -> Shrunk (a, b)
forall a. Bool -> a -> Shrunk a
Shrunk Bool
False (a
a, b
b)]

shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
shrinkPairS' a -> [Shrunk a]
f = (a -> [Shrunk a]) -> (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
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 :: ([a], [a]) -> [(a, ([a], [a]))]
pickOneReturnRest2 ([a]
xs, [a]
ys) =
  ((a, [a]) -> (a, ([a], [a]))) -> [(a, [a])] -> [(a, ([a], [a]))]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a
forall a. a -> a
id (a -> a) -> ([a] -> ([a], [a])) -> (a, [a]) -> (a, ([a], [a]))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ([a] -> [a] -> ([a], [a])) -> [a] -> [a] -> ([a], [a])
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) [a]
ys) ([a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
xs) [(a, ([a], [a]))] -> [(a, ([a], [a]))] -> [(a, ([a], [a]))]
forall a. [a] -> [a] -> [a]
++
  ((a, [a]) -> (a, ([a], [a]))) -> [(a, [a])] -> [(a, ([a], [a]))]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a
forall a. a -> a
id (a -> a) -> ([a] -> ([a], [a])) -> (a, [a]) -> (a, ([a], [a]))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
***      (,) [a]
xs) ([a] -> [(a, [a])]
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 :: [a] -> [(a, [a])]
pickOneReturnRest []       = []
pickOneReturnRest (a
x : [a]
xs) = (a
x, [a]
xs) (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: ((a, [a]) -> (a, [a])) -> [(a, [a])] -> [(a, [a])]
forall a b. (a -> b) -> [a] -> [b]
map (a -> a
forall a. a -> a
id (a -> a) -> ([a] -> [a]) -> (a, [a]) -> (a, [a])
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (a
x a -> [a] -> [a]
forall a. a -> [a] -> [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 :: [[a]] -> [(a, [[a]])]
pickOneReturnRestL [[a]]
ls = (([[a]], [a], [[a]]) -> [(a, [[a]])])
-> [([[a]], [a], [[a]])] -> [(a, [[a]])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
  (\([[a]]
prev, [a]
as, [[a]]
next) -> ((a, [a]) -> (a, [[a]])) -> [(a, [a])] -> [(a, [[a]])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(a
a, [a]
rest) -> (a
a, [[a]]
prev [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]
rest] [[a]] -> [[a]] -> [[a]]
forall a. [a] -> [a] -> [a]
++ [[a]]
next)) ([(a, [a])] -> [(a, [[a]])]) -> [(a, [a])] -> [(a, [[a]])]
forall a b. (a -> b) -> a -> b
$ [a] -> [(a, [a])]
forall a. [a] -> [(a, [a])]
pickOneReturnRest [a]
as)
  ([([[a]], [a], [[a]])] -> [(a, [[a]])])
-> [([[a]], [a], [[a]])] -> [(a, [[a]])]
forall a b. (a -> b) -> a -> b
$ [[a]] -> [([[a]], [a], [[a]])]
forall a. [a] -> [([a], a, [a])]
splitEach [[a]]
ls
    where
      splitEach :: [a] -> [([a], a, [a])]
      splitEach :: [a] -> [([a], a, [a])]
splitEach []       = []
      splitEach (a
a : [a]
as) = (([a], a, [a]) -> ([a], a, [a]))
-> [([a], a, [a])] -> [([a], a, [a])]
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)) ([([a], a, [a])] -> [([a], a, [a])])
-> [([a], a, [a])] -> [([a], a, [a])]
forall a b. (a -> b) -> a -> b
$
        [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
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' :: [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
go' [([a], a, [a])]
acc ([a]
_, a
_, []) = [([a], a, [a])] -> [([a], 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' a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
prev, a
b, [a]
next)
              in [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
forall a. [([a], a, [a])] -> ([a], a, [a]) -> [([a], a, [a])]
go' (([a], a, [a])
newElem ([a], a, [a]) -> [([a], a, [a])] -> [([a], a, [a])]
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 :: 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 model Concrete
forall (r :: * -> *). model r
initModel ([Operation cmd resp] -> model Concrete)
-> (History cmd resp -> [Operation cmd resp])
-> History cmd resp
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Forest (Operation cmd resp) -> [Operation cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Forest (Operation cmd resp) -> [Operation cmd resp]
operationsPath (Forest (Operation cmd resp) -> [Operation cmd resp])
-> (History cmd resp -> Forest (Operation cmd resp))
-> History cmd resp
-> [Operation cmd resp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History' cmd resp -> Forest (Operation cmd resp)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> Forest (Operation cmd resp)
interleavings (History' cmd resp -> Forest (Operation cmd resp))
-> (History cmd resp -> History' cmd resp)
-> History cmd resp
-> Forest (Operation cmd resp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History cmd resp -> History' cmd resp
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 (model Concrete -> cmd Concrete -> resp Concrete -> model Concrete
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