{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
module Test.StateMachine.Parallel
( forAllNParallelCommands
, forAllParallelCommands
, generateNParallelCommands
, generateParallelCommands
, shrinkNParallelCommands
, shrinkParallelCommands
, shrinkAndValidateNParallel
, shrinkAndValidateParallel
, shrinkCommands'
, runNParallelCommands
, runNParallelCommandsWithSetup
, runParallelCommands
, runParallelCommandsWithSetup
, runParallelCommands'
, runNParallelCommandsNTimes
, runNParallelCommandsNTimesWithSetup
, runParallelCommandsNTimes
, runParallelCommandsNTimesWithSetup
, runNParallelCommandsNTimes'
, runParallelCommandsNTimes'
, executeParallelCommands
, linearise
, toBoxDrawings
, prettyNParallelCommands
, prettyParallelCommands
, prettyParallelCommandsWithOpts
, prettyNParallelCommandsWithOpts
, advanceModel
, checkCommandNamesParallel
, coverCommandNamesParallel
, commandNamesParallel
) where
import Control.Monad
(replicateM, when)
import Control.Monad.Catch
(MonadMask(..), ExitCase(..))
import Control.Monad.State.Strict
(runStateT)
import Data.Bifunctor
(bimap)
import Data.Foldable
(toList)
import Data.List
(find, partition, permutations, foldl')
import qualified Data.Map.Strict as Map
import Data.Maybe
(fromMaybe, mapMaybe)
import Data.Monoid
import Data.Set
(Set)
import qualified Data.Set as S
import Data.Tree
(Tree(Node))
import Prelude
import Test.QuickCheck
(Gen, Property, Testable, choose, forAllShrinkShow,
property, sized)
import Test.QuickCheck.Monadic
(PropertyM, run)
import Text.PrettyPrint.ANSI.Leijen
(Doc)
import Text.Show.Pretty
(ppShow)
import UnliftIO
(MonadIO, MonadUnliftIO, concurrently,
forConcurrently, newTChanIO)
import qualified UnliftIO as UIO
import Test.StateMachine.BoxDrawer
import Test.StateMachine.ConstructorName
import Test.StateMachine.DotDrawing
import Test.StateMachine.Logic
import Test.StateMachine.Sequential
import Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.StateMachine.Utils
import qualified Text.PrettyPrint.ANSI.Leijen as PP
forAllParallelCommands :: Testable prop
=> (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> StateMachine model cmd m resp
-> Maybe Int
-> (ParallelCommands cmd resp -> prop)
-> Property
forAllParallelCommands :: forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(model :: (* -> *) -> *) (m :: * -> *).
(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
forAllParallelCommands StateMachine model cmd m resp
sm Maybe Int
mminSize =
Gen (ParallelCommands cmd resp)
-> (ParallelCommands cmd resp -> [ParallelCommands cmd resp])
-> (ParallelCommands cmd resp -> String)
-> (ParallelCommands cmd resp -> prop)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (StateMachine model cmd m resp
-> Maybe Int -> Gen (ParallelCommands cmd resp)
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)
generateParallelCommands StateMachine model cmd m resp
sm Maybe Int
mminSize) (StateMachine model cmd m resp
-> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkParallelCommands StateMachine model cmd m resp
sm) ParallelCommands cmd resp -> String
forall a. Show a => a -> String
ppShow
forAllNParallelCommands :: Testable prop
=> (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> StateMachine model cmd m resp
-> Int
-> (NParallelCommands cmd resp -> prop)
-> Property
forAllNParallelCommands :: forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(model :: (* -> *) -> *) (m :: * -> *).
(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
forAllNParallelCommands StateMachine model cmd m resp
sm Int
np =
Gen (NParallelCommands cmd resp)
-> (NParallelCommands cmd resp -> [NParallelCommands cmd resp])
-> (NParallelCommands cmd resp -> String)
-> (NParallelCommands cmd resp -> prop)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (StateMachine model cmd m resp
-> Int -> Gen (NParallelCommands cmd resp)
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)
generateNParallelCommands StateMachine model cmd m resp
sm Int
np) (StateMachine model cmd m resp
-> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
shrinkNParallelCommands StateMachine model cmd m resp
sm) NParallelCommands cmd resp -> String
forall a. Show a => a -> String
ppShow
generateParallelCommands :: forall model cmd m resp. Rank2.Foldable resp
=> Show (model Symbolic)
=> (Show (cmd Symbolic), Show (resp Symbolic))
=> StateMachine model cmd m resp
-> Maybe Int
-> Gen (ParallelCommands cmd resp)
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)
generateParallelCommands sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } Maybe Int
mminSize = do
Commands [Command cmd resp]
cmds <- StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands StateMachine model cmd m resp
sm Maybe Int
mminSize
Int
prefixLength <- (Int -> Gen Int) -> Gen Int
forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
3))
let (Commands cmd resp
prefix, Commands cmd resp
rest) = ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp], [Command cmd resp])
-> (Commands cmd resp, Commands cmd resp)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (Int
-> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
prefixLength [Command cmd resp]
cmds)
ParallelCommands cmd resp -> Gen (ParallelCommands cmd resp)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix
(model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
makeSuffixes (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
forall (r :: * -> *). model r
initModel Commands cmd resp
prefix) Commands cmd resp
rest))
where
makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
makeSuffixes model Symbolic
model0 = model Symbolic
-> [Pair (Commands cmd resp)]
-> [Command cmd resp]
-> [Pair (Commands cmd resp)]
go model Symbolic
model0 [] ([Command cmd resp] -> [Pair (Commands cmd resp)])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Pair (Commands cmd resp)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
where
go :: model Symbolic
-> [Pair (Commands cmd resp)]
-> [Command cmd resp]
-> [Pair (Commands cmd resp)]
go model Symbolic
_ [Pair (Commands cmd resp)]
acc [] = [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. [a] -> [a]
reverse [Pair (Commands cmd resp)]
acc
go model Symbolic
model [Pair (Commands cmd resp)]
acc [Command cmd resp]
cmds = model Symbolic
-> [Pair (Commands cmd resp)]
-> [Command cmd resp]
-> [Pair (Commands cmd resp)]
go (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
model ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe))
(Commands cmd resp -> Commands cmd resp -> Pair (Commands cmd resp)
forall a. a -> a -> Pair a
Pair ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe1) ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe2) Pair (Commands cmd resp)
-> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
acc)
[Command cmd resp]
rest
where
([Command cmd resp]
safe, [Command cmd resp]
rest) = StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model [] [Command cmd resp]
cmds
([Command cmd resp]
safe1, [Command cmd resp]
safe2) = Int
-> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp])
forall a. Int -> [a] -> ([a], [a])
splitAt ([Command cmd resp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [Command cmd resp]
safe
spanSafe :: Rank2.Foldable resp
=> StateMachine model cmd m resp
-> model Symbolic -> [Command cmd resp] -> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe :: forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
_ model Symbolic
_ [Command cmd resp]
safe [] = ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
safe, [])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model [Command cmd resp]
safe (Command cmd resp
cmd : [Command cmd resp]
cmds)
| [Command cmd resp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
5
, StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> Bool
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> Bool
parallelSafe StateMachine model cmd m resp
sm model Symbolic
model ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (Command cmd resp
cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
safe))
= StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model (Command cmd resp
cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
safe) [Command cmd resp]
cmds
| Bool
otherwise
= ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
safe, Command cmd resp
cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
cmds)
generateNParallelCommands :: forall model cmd m resp. Rank2.Foldable resp
=> Show (model Symbolic)
=> (Show (cmd Symbolic), Show (resp Symbolic))
=> StateMachine model cmd m resp
-> Int
-> Gen (NParallelCommands cmd resp)
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)
generateNParallelCommands sm :: StateMachine model cmd m resp
sm@StateMachine { 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 } Int
np =
if Int
np Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 then String -> Gen (NParallelCommands cmd resp)
forall a. HasCallStack => String -> a
error String
"number of threads must be positive" else do
Commands [Command cmd resp]
cmds <- StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands StateMachine model cmd m resp
sm Maybe Int
forall a. Maybe a
Nothing
Int
prefixLength <- (Int -> Gen Int) -> Gen Int
forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
3))
let (Commands cmd resp
prefix, Commands cmd resp
rest) = ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp], [Command cmd resp])
-> (Commands cmd resp, Commands cmd resp)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (Int
-> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
prefixLength [Command cmd resp]
cmds)
NParallelCommands cmd resp -> Gen (NParallelCommands cmd resp)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Commands cmd resp
-> [[Commands cmd resp]] -> NParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix
(model Symbolic -> Commands cmd resp -> [[Commands cmd resp]]
makeSuffixes (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
forall (r :: * -> *). model r
initModel Commands cmd resp
prefix) Commands cmd resp
rest))
where
makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]]
makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]]
makeSuffixes model Symbolic
model0 = model Symbolic
-> [[Commands cmd resp]]
-> [Command cmd resp]
-> [[Commands cmd resp]]
go model Symbolic
model0 [] ([Command cmd resp] -> [[Commands cmd resp]])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [[Commands cmd resp]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
where
go :: model Symbolic
-> [[Commands cmd resp]]
-> [Command cmd resp]
-> [[Commands cmd resp]]
go :: model Symbolic
-> [[Commands cmd resp]]
-> [Command cmd resp]
-> [[Commands cmd resp]]
go model Symbolic
_ [[Commands cmd resp]]
acc [] = [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. [a] -> [a]
reverse [[Commands cmd resp]]
acc
go model Symbolic
model [[Commands cmd resp]]
acc [Command cmd resp]
cmds = model Symbolic
-> [[Commands cmd resp]]
-> [Command cmd resp]
-> [[Commands cmd resp]]
go (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
model ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe))
([Commands cmd resp]
safes [Commands cmd resp]
-> [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
acc)
[Command cmd resp]
rest
where
([Command cmd resp]
safe, [Command cmd resp]
rest) = StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model [] [Command cmd resp]
cmds
safes :: [Commands cmd resp]
safes = [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands ([Command cmd resp] -> Commands cmd resp)
-> [[Command cmd resp]] -> [Commands cmd resp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Int -> [Command cmd resp] -> [[Command cmd resp]]
forall a. Int -> Int -> [a] -> [[a]]
chunksOf Int
np ([Command cmd resp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
np) [Command cmd resp]
safe
chunksOf :: Int -> Int -> [a] -> [[a]]
chunksOf :: forall a. Int -> Int -> [a] -> [[a]]
chunksOf Int
1 Int
_ [a]
xs = [[a]
xs]
chunksOf Int
n Int
len [a]
xs = [a]
as [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> Int -> [a] -> [[a]]
forall a. Int -> Int -> [a] -> [[a]]
chunksOf (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
len [a]
bs
where ([a]
as, [a]
bs) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
len [a]
xs
parallelSafe :: Rank2.Foldable resp
=> StateMachine model cmd m resp -> model Symbolic
-> Commands cmd resp -> Bool
parallelSafe :: forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> Bool
parallelSafe StateMachine { model Symbolic -> cmd Symbolic -> Logic
precondition :: model Symbolic -> cmd Symbolic -> Logic
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition, 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 (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock } model Symbolic
model0
= ([Command cmd resp] -> Bool) -> [[Command cmd resp]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (model Symbolic -> [Command cmd resp] -> Bool
preconditionsHold model Symbolic
model0)
([[Command cmd resp]] -> Bool)
-> (Commands cmd resp -> [[Command cmd resp]])
-> Commands cmd resp
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Command cmd resp] -> [[Command cmd resp]]
forall a. [a] -> [[a]]
permutations
([Command cmd resp] -> [[Command cmd resp]])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [[Command cmd resp]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
where
preconditionsHold :: model Symbolic -> [Command cmd resp] -> Bool
preconditionsHold model Symbolic
_ [] = Bool
True
preconditionsHold model Symbolic
model (Command cmd Symbolic
cmd resp Symbolic
resp [Var]
vars : [Command cmd resp]
cmds) =
Logic -> Bool
boolean (model Symbolic -> cmd Symbolic -> Logic
precondition model Symbolic
model cmd Symbolic
cmd) Bool -> Bool -> Bool
&&
model Symbolic -> [Command cmd resp] -> Bool
preconditionsHold (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
cmd resp Symbolic
resp) [Command cmd resp]
cmds Bool -> Bool -> Bool
&&
[Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (resp Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars (resp Symbolic -> [Var]) -> resp Symbolic -> [Var]
forall a b. (a -> b) -> a -> b
$ (resp Symbolic, Counter) -> resp Symbolic
forall a b. (a, b) -> a
fst ((resp Symbolic, Counter) -> resp Symbolic)
-> (resp Symbolic, Counter) -> resp Symbolic
forall a b. (a -> b) -> a -> b
$ GenSym (resp Symbolic) -> Counter -> (resp Symbolic, Counter)
forall a. GenSym a -> Counter -> (a, Counter)
runGenSym (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock model Symbolic
model cmd Symbolic
cmd) Counter
newCounter)
advanceModel :: StateMachine model cmd m resp
-> model Symbolic
-> Commands cmd resp
-> model Symbolic
advanceModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel 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 } model Symbolic
model0 =
model Symbolic -> [Command cmd resp] -> model Symbolic
go model Symbolic
model0 ([Command cmd resp] -> model Symbolic)
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> model Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
where
go :: model Symbolic -> [Command cmd resp] -> model Symbolic
go model Symbolic
model [] = model Symbolic
model
go model Symbolic
model (Command cmd Symbolic
cmd resp Symbolic
resp [Var]
_vars : [Command cmd resp]
cmds) =
model Symbolic -> [Command cmd resp] -> model Symbolic
go (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
cmd resp Symbolic
resp) [Command cmd resp]
cmds
shrinkParallelCommands
:: forall cmd model m resp. Rank2.Traversable cmd
=> Rank2.Foldable resp
=> StateMachine model cmd m resp
-> (ParallelCommands cmd resp -> [ParallelCommands cmd resp])
shrinkParallelCommands :: forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkParallelCommands StateMachine model cmd m resp
sm (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes)
= (Shrunk (ParallelCommandsF Pair cmd resp)
-> [ParallelCommandsF Pair cmd resp])
-> [Shrunk (ParallelCommandsF Pair cmd resp)]
-> [ParallelCommandsF Pair cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk (ParallelCommandsF Pair cmd resp)
-> [ParallelCommandsF Pair cmd resp]
go
[ Bool
-> ParallelCommandsF Pair cmd resp
-> Shrunk (ParallelCommandsF Pair cmd resp)
forall a. Bool -> a -> Shrunk a
Shrunk Bool
s (Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommandsF Pair cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' (((Commands cmd resp, Commands cmd resp)
-> Pair (Commands cmd resp))
-> [(Commands cmd resp, Commands cmd resp)]
-> [Pair (Commands cmd resp)]
forall a b. (a -> b) -> [a] -> [b]
map (Commands cmd resp, Commands cmd resp) -> Pair (Commands cmd resp)
forall a. (a, a) -> Pair a
toPair [(Commands cmd resp, Commands cmd resp)]
suffixes'))
| Shrunk Bool
s (Commands cmd resp
prefix', [(Commands cmd resp, Commands cmd resp)]
suffixes') <- (Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> ([(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]])
-> (Commands cmd resp, [(Commands cmd resp, Commands cmd resp)])
-> [Shrunk
(Commands cmd resp, [(Commands cmd resp, Commands cmd resp)])]
forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' [(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
shrinkSuffixes
(Commands cmd resp
prefix, (Pair (Commands cmd resp)
-> (Commands cmd resp, Commands cmd resp))
-> [Pair (Commands cmd resp)]
-> [(Commands cmd resp, Commands cmd resp)]
forall a b. (a -> b) -> [a] -> [b]
map Pair (Commands cmd resp) -> (Commands cmd resp, Commands cmd resp)
forall a. Pair a -> (a, a)
fromPair [Pair (Commands cmd resp)]
suffixes)
]
[ParallelCommandsF Pair cmd resp]
-> [ParallelCommandsF Pair cmd resp]
-> [ParallelCommandsF Pair cmd resp]
forall a. [a] -> [a] -> [a]
++
[ParallelCommandsF Pair cmd resp]
shrinkMoveSuffixToPrefix
where
go :: Shrunk (ParallelCommands cmd resp) -> [ParallelCommands cmd resp]
go :: Shrunk (ParallelCommandsF Pair cmd resp)
-> [ParallelCommandsF Pair cmd resp]
go (Shrunk Bool
shrunk ParallelCommandsF Pair cmd resp
cmds) =
StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommandsF Pair cmd resp
-> [ParallelCommandsF Pair cmd resp]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommands cmd resp
-> [ParallelCommands cmd resp]
shrinkAndValidateParallel StateMachine model cmd m resp
sm
(if Bool
shrunk then ShouldShrink
DontShrink else ShouldShrink
MustShrink)
ParallelCommandsF Pair cmd resp
cmds
shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
shrinkSuffixes = ((Commands cmd resp, Commands cmd resp)
-> [Shrunk (Commands cmd resp, Commands cmd resp)])
-> [(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS ((Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> (Commands cmd resp, Commands cmd resp)
-> [Shrunk (Commands cmd resp, Commands cmd resp)]
forall a. (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
shrinkPairS' Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands')
shrinkMoveSuffixToPrefix :: [ParallelCommands cmd resp]
shrinkMoveSuffixToPrefix :: [ParallelCommandsF Pair cmd resp]
shrinkMoveSuffixToPrefix = case [Pair (Commands cmd resp)]
suffixes of
[] -> []
(Pair (Commands cmd resp)
suffix : [Pair (Commands cmd resp)]
suffixes') ->
[ Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommandsF Pair cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands (Commands cmd resp
prefix Commands cmd resp -> Commands cmd resp -> Commands cmd resp
forall a. Semigroup a => a -> a -> a
<> [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp
prefix'])
(([Command cmd resp] -> Commands cmd resp)
-> Pair [Command cmd resp] -> Pair (Commands cmd resp)
forall a b. (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (([Command cmd resp], [Command cmd resp]) -> Pair [Command cmd resp]
forall a. (a, a) -> Pair a
toPair ([Command cmd resp], [Command cmd resp])
suffix') Pair (Commands cmd resp)
-> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
suffixes')
| (Command cmd resp
prefix', ([Command cmd resp], [Command cmd resp])
suffix') <- ([Command cmd resp], [Command cmd resp])
-> [(Command cmd resp, ([Command cmd resp], [Command cmd resp]))]
forall a. ([a], [a]) -> [(a, ([a], [a]))]
pickOneReturnRest2 (Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (Pair (Commands cmd resp) -> Commands cmd resp
forall a. Pair a -> a
proj1 Pair (Commands cmd resp)
suffix),
Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (Pair (Commands cmd resp) -> Commands cmd resp
forall a. Pair a -> a
proj2 Pair (Commands cmd resp)
suffix))
]
shrinkNParallelCommands
:: forall cmd model m resp. Rank2.Traversable cmd
=> Rank2.Foldable resp
=> StateMachine model cmd m resp
-> (NParallelCommands cmd resp -> [NParallelCommands cmd resp])
shrinkNParallelCommands :: forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
shrinkNParallelCommands StateMachine model cmd m resp
sm (ParallelCommands Commands cmd resp
prefix [[Commands cmd resp]]
suffixes)
= (Shrunk (ParallelCommandsF [] cmd resp)
-> [ParallelCommandsF [] cmd resp])
-> [Shrunk (ParallelCommandsF [] cmd resp)]
-> [ParallelCommandsF [] cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk (ParallelCommandsF [] cmd resp)
-> [ParallelCommandsF [] cmd resp]
go
[ Bool
-> ParallelCommandsF [] cmd resp
-> Shrunk (ParallelCommandsF [] cmd resp)
forall a. Bool -> a -> Shrunk a
Shrunk Bool
s (Commands cmd resp
-> [[Commands cmd resp]] -> ParallelCommandsF [] cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' [[Commands cmd resp]]
suffixes')
| Shrunk Bool
s (Commands cmd resp
prefix', [[Commands cmd resp]]
suffixes') <- (Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> ([[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]])
-> (Commands cmd resp, [[Commands cmd resp]])
-> [Shrunk (Commands cmd resp, [[Commands cmd resp]])]
forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]]
shrinkSuffixes
(Commands cmd resp
prefix, [[Commands cmd resp]]
suffixes)
]
[ParallelCommandsF [] cmd resp]
-> [ParallelCommandsF [] cmd resp]
-> [ParallelCommandsF [] cmd resp]
forall a. [a] -> [a] -> [a]
++
[ParallelCommandsF [] cmd resp]
shrinkMoveSuffixToPrefix
where
go :: Shrunk (NParallelCommands cmd resp) -> [NParallelCommands cmd resp]
go :: Shrunk (ParallelCommandsF [] cmd resp)
-> [ParallelCommandsF [] cmd resp]
go (Shrunk Bool
shrunk ParallelCommandsF [] cmd resp
cmds) =
StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommandsF [] cmd resp
-> [ParallelCommandsF [] cmd resp]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> NParallelCommands cmd resp
-> [NParallelCommands cmd resp]
shrinkAndValidateNParallel StateMachine model cmd m resp
sm
(if Bool
shrunk then ShouldShrink
DontShrink else ShouldShrink
MustShrink)
ParallelCommandsF [] cmd resp
cmds
shrinkSuffixes :: [[Commands cmd resp]]
-> [Shrunk [[Commands cmd resp]]]
shrinkSuffixes :: [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]]
shrinkSuffixes = ([Commands cmd resp] -> [Shrunk [Commands cmd resp]])
-> [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS ((Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> [Commands cmd resp] -> [Shrunk [Commands cmd resp]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS'' Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands')
shrinkMoveSuffixToPrefix :: [NParallelCommands cmd resp]
shrinkMoveSuffixToPrefix :: [ParallelCommandsF [] cmd resp]
shrinkMoveSuffixToPrefix = case [[Commands cmd resp]]
suffixes of
[] -> []
([Commands cmd resp]
suffix : [[Commands cmd resp]]
suffixes') ->
[ Commands cmd resp
-> [[Commands cmd resp]] -> ParallelCommandsF [] cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands (Commands cmd resp
prefix Commands cmd resp -> Commands cmd resp -> Commands cmd resp
forall a. Semigroup a => a -> a -> a
<> [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp
prefix'])
(([Command cmd resp] -> Commands cmd resp)
-> [[Command cmd resp]] -> [Commands cmd resp]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [[Command cmd resp]]
suffix' [Commands cmd resp]
-> [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
suffixes')
| (Command cmd resp
prefix', [[Command cmd resp]]
suffix') <- [[Command cmd resp]] -> [(Command cmd resp, [[Command cmd resp]])]
forall a. [[a]] -> [(a, [[a]])]
pickOneReturnRestL (Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (Commands cmd resp -> [Command cmd resp])
-> [Commands cmd resp] -> [[Command cmd resp]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Commands cmd resp]
suffix)
]
shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' = (Shrunk [Command cmd resp] -> Shrunk (Commands cmd resp))
-> [Shrunk [Command cmd resp]] -> [Shrunk (Commands cmd resp)]
forall a b. (a -> b) -> [a] -> [b]
map (([Command cmd resp] -> Commands cmd resp)
-> Shrunk [Command cmd resp] -> Shrunk (Commands cmd resp)
forall a b. (a -> b) -> Shrunk a -> Shrunk b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands) ([Shrunk [Command cmd resp]] -> [Shrunk (Commands cmd resp)])
-> (Commands cmd resp -> [Shrunk [Command cmd resp]])
-> Commands cmd resp
-> [Shrunk (Commands cmd resp)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Command cmd resp] -> [Shrunk [Command cmd resp]]
forall a. [a] -> [Shrunk [a]]
shrinkListS' ([Command cmd resp] -> [Shrunk [Command cmd resp]])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Shrunk [Command cmd resp]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
shrinkAndValidateParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
=> StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommands cmd resp
-> [ParallelCommands cmd resp]
shrinkAndValidateParallel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommands cmd resp
-> [ParallelCommands cmd resp]
shrinkAndValidateParallel sm :: StateMachine model cmd m resp
sm@StateMachine { 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 } = \ShouldShrink
shouldShrink (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes) ->
let env :: ValidateEnv model
env = model Symbolic -> ValidateEnv model
forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv model Symbolic
forall (r :: * -> *). model r
initModel
curryGo :: ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
shouldShrink' (ValidateEnv model
env', Commands cmd resp
prefix') = Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go Commands cmd resp
prefix' ValidateEnv model
env' ShouldShrink
shouldShrink' [Pair (Commands cmd resp)]
suffixes in
case ShouldShrink
shouldShrink of
ShouldShrink
DontShrink -> ((ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [ParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
prefix)
ShouldShrink
MustShrink -> ((ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [ParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
MustShrink ValidateEnv model
env Commands cmd resp
prefix)
[ParallelCommands cmd resp]
-> [ParallelCommands cmd resp] -> [ParallelCommands cmd resp]
forall a. [a] -> [a] -> [a]
++ ((ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [ParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
MustShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
prefix)
where
go :: Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go :: Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go Commands cmd resp
prefix' = [Pair (Commands cmd resp)]
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go' []
where
go' :: [Pair (Commands cmd resp)]
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go' :: [Pair (Commands cmd resp)]
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go' [Pair (Commands cmd resp)]
_ ValidateEnv model
_ ShouldShrink
MustShrink [] = []
go' [Pair (Commands cmd resp)]
acc ValidateEnv model
_ ShouldShrink
DontShrink [] = [Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' ([Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. [a] -> [a]
reverse [Pair (Commands cmd resp)]
acc)]
go' [Pair (Commands cmd resp)]
acc ValidateEnv model
env ShouldShrink
shouldShrink (Pair Commands cmd resp
l Commands cmd resp
r : [Pair (Commands cmd resp)]
suffixes) = do
((ShouldShrink
shrinkL, ShouldShrink
shrinkR), ShouldShrink
shrinkRest) <- [((ShouldShrink, ShouldShrink), ShouldShrink)]
shrinkOpts
(ValidateEnv model
envL, Commands cmd resp
l') <- StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
shrinkL ValidateEnv model
env Commands cmd resp
l
(ValidateEnv model
envR, Commands cmd resp
r') <- StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
shrinkR (ValidateEnv model
env ValidateEnv model -> ValidateEnv model -> ValidateEnv model
forall (model :: (* -> *) -> *).
ValidateEnv model -> ValidateEnv model -> ValidateEnv model
`withCounterFrom` ValidateEnv model
envL) Commands cmd resp
r
[Pair (Commands cmd resp)]
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go' (Commands cmd resp -> Commands cmd resp -> Pair (Commands cmd resp)
forall a. a -> a -> Pair a
Pair Commands cmd resp
l' Commands cmd resp
r' Pair (Commands cmd resp)
-> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
acc) (StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
combineEnv StateMachine model cmd m resp
sm ValidateEnv model
envL ValidateEnv model
envR Commands cmd resp
r') ShouldShrink
shrinkRest [Pair (Commands cmd resp)]
suffixes
where
shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)]
shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)]
shrinkOpts =
case ShouldShrink
shouldShrink of
ShouldShrink
DontShrink -> [ ((ShouldShrink
DontShrink, ShouldShrink
DontShrink), ShouldShrink
DontShrink) ]
ShouldShrink
MustShrink -> [ ((ShouldShrink
MustShrink, ShouldShrink
DontShrink), ShouldShrink
DontShrink)
, ((ShouldShrink
DontShrink, ShouldShrink
MustShrink), ShouldShrink
DontShrink)
, ((ShouldShrink
DontShrink, ShouldShrink
DontShrink), ShouldShrink
MustShrink) ]
combineEnv :: StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
combineEnv :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
combineEnv StateMachine model cmd m resp
sm ValidateEnv model
envL ValidateEnv model
envR Commands cmd resp
cmds = ValidateEnv {
veModel :: model Symbolic
veModel = StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm (ValidateEnv model -> model Symbolic
forall (model :: (* -> *) -> *).
ValidateEnv model -> model Symbolic
veModel ValidateEnv model
envL) Commands cmd resp
cmds
, veScope :: Map Var Var
veScope = Map Var Var -> Map Var Var -> Map Var Var
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (ValidateEnv model -> Map Var Var
forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope ValidateEnv model
envL) (ValidateEnv model -> Map Var Var
forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope ValidateEnv model
envR)
, veCounter :: Counter
veCounter = ValidateEnv model -> Counter
forall (model :: (* -> *) -> *). ValidateEnv model -> Counter
veCounter ValidateEnv model
envR
}
withCounterFrom :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model
withCounterFrom :: forall (model :: (* -> *) -> *).
ValidateEnv model -> ValidateEnv model -> ValidateEnv model
withCounterFrom ValidateEnv model
e ValidateEnv model
e' = ValidateEnv model
e { veCounter = veCounter e' }
shrinkAndValidateNParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
=> StateMachine model cmd m resp
-> ShouldShrink
-> NParallelCommands cmd resp
-> [NParallelCommands cmd resp]
shrinkAndValidateNParallel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> NParallelCommands cmd resp
-> [NParallelCommands cmd resp]
shrinkAndValidateNParallel StateMachine model cmd m resp
sm = \ShouldShrink
shouldShrink (ParallelCommands Commands cmd resp
prefix [[Commands cmd resp]]
suffixes) ->
let env :: ValidateEnv model
env = model Symbolic -> ValidateEnv model
forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv (model Symbolic -> ValidateEnv model)
-> model Symbolic -> ValidateEnv model
forall a b. (a -> b) -> a -> b
$ StateMachine model cmd m resp -> forall (r :: * -> *). model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel StateMachine model cmd m resp
sm
curryGo :: ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
shouldShrink' (ValidateEnv model
env', Commands cmd resp
prefix') = Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go Commands cmd resp
prefix' ValidateEnv model
env' ShouldShrink
shouldShrink' [[Commands cmd resp]]
suffixes in
case ShouldShrink
shouldShrink of
ShouldShrink
DontShrink -> ((ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [NParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
prefix)
ShouldShrink
MustShrink -> ((ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [NParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
MustShrink ValidateEnv model
env Commands cmd resp
prefix)
[NParallelCommands cmd resp]
-> [NParallelCommands cmd resp] -> [NParallelCommands cmd resp]
forall a. [a] -> [a] -> [a]
++ ((ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [NParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
MustShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
prefix)
where
go :: Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go :: Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go Commands cmd resp
prefix' = [[Commands cmd resp]]
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go' []
where
go' :: [[Commands cmd resp]]
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go' :: [[Commands cmd resp]]
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go' [[Commands cmd resp]]
_ ValidateEnv model
_ ShouldShrink
MustShrink [] = []
go' [[Commands cmd resp]]
acc ValidateEnv model
_ ShouldShrink
DontShrink [] = [Commands cmd resp
-> [[Commands cmd resp]] -> NParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' ([[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. [a] -> [a]
reverse [[Commands cmd resp]]
acc)]
go' [[Commands cmd resp]]
acc ValidateEnv model
env ShouldShrink
shouldShrink ([Commands cmd resp]
suffix : [[Commands cmd resp]]
suffixes) = do
([(ShouldShrink, Commands cmd resp)]
suffixWithShrinks, ShouldShrink
shrinkRest) <- [Commands cmd resp]
-> [([(ShouldShrink, Commands cmd resp)], ShouldShrink)]
forall a. [a] -> [([(ShouldShrink, a)], ShouldShrink)]
shrinkOpts [Commands cmd resp]
suffix
(ValidateEnv model
envFinal, [Commands cmd resp]
suffix') <- (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> [(ValidateEnv model, [Commands cmd resp])]
forall a b. (a, b) -> b
snd ((Bool, [(ValidateEnv model, [Commands cmd resp])])
-> [(ValidateEnv model, [Commands cmd resp])])
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> [(ValidateEnv model, [Commands cmd resp])]
forall a b. (a -> b) -> a -> b
$ ((Bool, [(ValidateEnv model, [Commands cmd resp])])
-> (ShouldShrink, Commands cmd resp)
-> (Bool, [(ValidateEnv model, [Commands cmd resp])]))
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> [(ShouldShrink, Commands cmd resp)]
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> (ShouldShrink, Commands cmd resp)
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
f (Bool
True, [(ValidateEnv model
env,[])]) [(ShouldShrink, Commands cmd resp)]
suffixWithShrinks
[[Commands cmd resp]]
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go' ([Commands cmd resp] -> [Commands cmd resp]
forall a. [a] -> [a]
reverse [Commands cmd resp]
suffix' [Commands cmd resp]
-> [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
acc) ValidateEnv model
envFinal ShouldShrink
shrinkRest [[Commands cmd resp]]
suffixes
where
f :: (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> (ShouldShrink, Commands cmd resp)
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
f :: (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> (ShouldShrink, Commands cmd resp)
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
f (Bool
firstCall, [(ValidateEnv model, [Commands cmd resp])]
acc') (ShouldShrink
shrink, Commands cmd resp
cmds) = (Bool
False, [(ValidateEnv model, [Commands cmd resp])]
acc'')
where
acc'' :: [(ValidateEnv model, [Commands cmd resp])]
acc'' = do
(ValidateEnv model
envPrev, [Commands cmd resp]
cmdsPrev) <- [(ValidateEnv model, [Commands cmd resp])]
acc'
let envUsed :: ValidateEnv model
envUsed = if Bool
firstCall then ValidateEnv model
env else ValidateEnv model
env ValidateEnv model -> ValidateEnv model -> ValidateEnv model
forall (model :: (* -> *) -> *).
ValidateEnv model -> ValidateEnv model -> ValidateEnv model
`withCounterFrom` ValidateEnv model
envPrev
(ValidateEnv model
env', Commands cmd resp
cmd') <- StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
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)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
shrink ValidateEnv model
envUsed Commands cmd resp
cmds
let env'' :: ValidateEnv model
env'' = if Bool
firstCall then ValidateEnv model
env' else
StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
combineEnv StateMachine model cmd m resp
sm ValidateEnv model
envPrev ValidateEnv model
env' Commands cmd resp
cmd'
(ValidateEnv model, [Commands cmd resp])
-> [(ValidateEnv model, [Commands cmd resp])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (ValidateEnv model
env'', Commands cmd resp
cmd' Commands cmd resp -> [Commands cmd resp] -> [Commands cmd resp]
forall a. a -> [a] -> [a]
: [Commands cmd resp]
cmdsPrev)
shrinkOpts :: [a] -> [([(ShouldShrink, a)], ShouldShrink)]
shrinkOpts :: forall a. [a] -> [([(ShouldShrink, a)], ShouldShrink)]
shrinkOpts [a]
ls =
let len :: Int
len = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ls
dontShrink :: [ShouldShrink]
dontShrink = Int -> ShouldShrink -> [ShouldShrink]
forall a. Int -> a -> [a]
replicate Int
len ShouldShrink
DontShrink
shrinks :: [[ShouldShrink]]
shrinks = if Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
then String -> [[ShouldShrink]]
forall a. HasCallStack => String -> a
error String
"Invariant violation! A suffix should never be an empty list"
else ((Int -> [ShouldShrink]) -> [Int] -> [[ShouldShrink]])
-> [Int] -> (Int -> [ShouldShrink]) -> [[ShouldShrink]]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int -> [ShouldShrink]) -> [Int] -> [[ShouldShrink]]
forall a b. (a -> b) -> [a] -> [b]
map [Int
1..Int
len] ((Int -> [ShouldShrink]) -> [[ShouldShrink]])
-> (Int -> [ShouldShrink]) -> [[ShouldShrink]]
forall a b. (a -> b) -> a -> b
$ \Int
n ->
Int -> ShouldShrink -> [ShouldShrink]
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ShouldShrink
DontShrink [ShouldShrink] -> [ShouldShrink] -> [ShouldShrink]
forall a. [a] -> [a] -> [a]
++ [ShouldShrink
MustShrink] [ShouldShrink] -> [ShouldShrink] -> [ShouldShrink]
forall a. [a] -> [a] -> [a]
++ Int -> ShouldShrink -> [ShouldShrink]
forall a. Int -> a -> [a]
replicate (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) ShouldShrink
DontShrink
in case ShouldShrink
shouldShrink of
ShouldShrink
DontShrink -> [([ShouldShrink] -> [a] -> [(ShouldShrink, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
dontShrink [a]
ls, ShouldShrink
DontShrink)]
ShouldShrink
MustShrink -> ([ShouldShrink] -> ([(ShouldShrink, a)], ShouldShrink))
-> [[ShouldShrink]] -> [([(ShouldShrink, a)], ShouldShrink)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[ShouldShrink]
shrinkLs -> ([ShouldShrink] -> [a] -> [(ShouldShrink, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
shrinkLs [a]
ls, ShouldShrink
DontShrink)) [[ShouldShrink]]
shrinks
[([(ShouldShrink, a)], ShouldShrink)]
-> [([(ShouldShrink, a)], ShouldShrink)]
-> [([(ShouldShrink, a)], ShouldShrink)]
forall a. [a] -> [a] -> [a]
++ [([ShouldShrink] -> [a] -> [(ShouldShrink, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
dontShrink [a]
ls, ShouldShrink
MustShrink)]
runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommands = Int
-> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsNTimes Int
10
runParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsWithSetup = Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsNTimesWithSetup Int
10
runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.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)]
runParallelCommands' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommands' = Int
-> m (StateMachine model cmd m resp)
-> (cmd Concrete -> resp Concrete)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsNTimes' Int
10
runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommands = Int
-> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommandsNTimes Int
10
runNParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommandsWithSetup = Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommandsNTimesWithSetup Int
10
runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> Int
-> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsNTimes Int
n StateMachine model cmd m resp
sm = Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsNTimesWithSetup Int
n (StateMachine model cmd m resp -> m (StateMachine model cmd m resp)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StateMachine model cmd m resp
sm)
runParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimesWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsNTimesWithSetup Int
n m (StateMachine model cmd m resp)
msm ParallelCommands cmd resp
cmds =
Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
((History cmd resp
hist, model Concrete
model, Reason
reason1, Reason
reason2), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
(((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
-> ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> m ())
-> (StateMachine model cmd m resp
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
m (StateMachine model cmd m resp)
msm
(\StateMachine model cmd m resp
sm' ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
ec -> case ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
ec of
ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason, Reason)
-> ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason, Reason)
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)
executeParallelCommands StateMachine model cmd m resp
sm' ParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
(History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, Reason -> Logic
logicReason ([Reason] -> Reason
combineReasons [Reason
reason1, Reason
reason2]) Logic -> Logic -> Logic
.&& StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
hist)
runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.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)]
runParallelCommandsNTimes' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runParallelCommandsNTimes' Int
n m (StateMachine model cmd m resp)
msm cmd Concrete -> resp Concrete
complete ParallelCommands cmd resp
cmds =
Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
((History cmd resp
hist, model Concrete
model, Reason
_, Reason
_), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
(((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
-> ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
-> m ())
-> (StateMachine model cmd m resp
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp),
())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
m (StateMachine model cmd m resp)
msm
(\StateMachine model cmd m resp
sm' ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
ec -> case ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
ec of
ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
ExitCase
((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason, Reason)
-> ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason, Reason)
-> m ((History cmd resp, model Concrete, Reason, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)
executeParallelCommands StateMachine model cmd m resp
sm' ParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
let hist' :: History cmd resp
hist' = (cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist
(History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist', model Concrete
model, StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
hist')
runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> Int
-> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommandsNTimes Int
n StateMachine model cmd m resp
sm = Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommandsNTimesWithSetup Int
n (StateMachine model cmd m resp -> m (StateMachine model cmd m resp)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StateMachine model cmd m resp
sm)
runNParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimesWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommandsNTimesWithSetup Int
n m (StateMachine model cmd m resp)
msm NParallelCommands cmd resp
cmds =
Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
((History cmd resp
hist, model Concrete
model, Reason
reason), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
(((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
-> ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> m ())
-> (StateMachine model cmd m resp
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
m (StateMachine model cmd m resp)
msm
(\StateMachine model cmd m resp
sm' ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
ec -> case ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
ec of
ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason)
-> ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason)
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Traversable cmd, Show (cmd Concrete), Foldable resp,
Show (resp Concrete), MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands StateMachine model cmd m resp
sm' NParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
(History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, Reason -> Logic
logicReason Reason
reason Logic -> Logic -> Logic
.&& StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
hist)
runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.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)]
runNParallelCommandsNTimes' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)]
runNParallelCommandsNTimes' Int
n m (StateMachine model cmd m resp)
msm cmd Concrete -> resp Concrete
complete NParallelCommands cmd resp
cmds =
Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
((History cmd resp
hist, model Concrete
model, Reason
_reason), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> PropertyM
m
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
(((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
-> ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
-> ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
-> m ())
-> (StateMachine model cmd m resp
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp),
())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
m (StateMachine model cmd m resp)
msm
(\StateMachine model cmd m resp
sm' ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
ec -> case ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
ec of
ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
ExitCase
((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason)
-> ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason)
-> m ((History cmd resp, model Concrete, Reason),
StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Traversable cmd, Show (cmd Concrete), Foldable resp,
Show (resp Concrete), MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands StateMachine model cmd m resp
sm' NParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
let hist' :: History cmd resp
hist' = (cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist
(History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
hist')
executeParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadUnliftIO m)
=> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> UIO.TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
executeParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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)
executeParallelCommands sm :: StateMachine model cmd m resp
sm@StateMachine{ 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 } (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes) TChan (Pid, HistoryEvent cmd resp)
hchan Bool
stopOnError = do
(Reason
reason0, (Environment
env0, model Symbolic
_smodel, Counter
_counter, model Concrete
cmodel)) <- StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
0) Check
CheckEverything Commands cmd resp
prefix)
(Environment
emptyEnvironment, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
if Reason
reason0 Reason -> Reason -> Bool
forall a. Eq a => a -> a -> Bool
/= Reason
Ok
then do
[(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
(History cmd resp, model Concrete, Reason, Reason)
-> m (History cmd resp, model Concrete, Reason, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, Reason
reason0, Reason
reason0)
else do
(Reason
reason1, Reason
reason2, Environment
_) <- (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go (Reason
Ok, Reason
Ok, Environment
env0) [Pair (Commands cmd resp)]
suffixes
[(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
(History cmd resp, model Concrete, Reason, Reason)
-> m (History cmd resp, model Concrete, Reason, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, Reason
reason1, Reason
reason2)
where
go :: (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go (Reason
res1, Reason
res2, Environment
env) [] = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason
res1, Reason
res2, Environment
env)
go (Reason
Ok, Reason
Ok, Environment
env) (Pair Commands cmd resp
cmds1 Commands cmd resp
cmds2 : [Pair (Commands cmd resp)]
pairs) = do
((Reason
reason1, (Environment
env1, model Symbolic
_, Counter
_, model Concrete
_)), (Reason
reason2, (Environment
env2, model Symbolic
_, Counter
_, model Concrete
_))) <- m (Reason, (Environment, model Symbolic, Counter, model Concrete))
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
-> m ((Reason,
(Environment, model Symbolic, Counter, model Concrete)),
(Reason, (Environment, model Symbolic, Counter, model Concrete)))
forall (m :: * -> *) a b. MonadUnliftIO m => m a -> m b -> m (a, b)
concurrently
(StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
1) Check
CheckNothing Commands cmd resp
cmds1) (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel))
(StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
2) Check
CheckNothing Commands cmd resp
cmds2) (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel))
case (Reason -> Bool
isOK (Reason -> Bool) -> Reason -> Bool
forall a b. (a -> b) -> a -> b
$ [Reason] -> Reason
combineReasons [Reason
reason1, Reason
reason2], Bool
stopOnError) of
(Bool
False, Bool
True) -> (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason
reason1, Reason
reason2, Environment
env1 Environment -> Environment -> Environment
forall a. Semigroup a => a -> a -> a
<> Environment
env2)
(Bool, Bool)
_ -> (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go ( Reason
reason1
, Reason
reason2
, Environment
env1 Environment -> Environment -> Environment
forall a. Semigroup a => a -> a -> a
<> Environment
env2
) [Pair (Commands cmd resp)]
pairs
go (Reason
Ok, ExceptionThrown String
e, Environment
env) (Pair Commands cmd resp
cmds1 Commands cmd resp
_cmds2 : [Pair (Commands cmd resp)]
pairs) = do
(Reason
reason1, (Environment
env1, model Symbolic
_, Counter
_, model Concrete
_)) <- StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
1) Check
CheckPrecondition Commands cmd resp
cmds1)
(Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
(Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go ( Reason
reason1
, String -> Reason
ExceptionThrown String
e
, Environment
env1
) [Pair (Commands cmd resp)]
pairs
go (ExceptionThrown String
e, Reason
Ok, Environment
env) (Pair Commands cmd resp
_cmds1 Commands cmd resp
cmds2 : [Pair (Commands cmd resp)]
pairs) = do
(Reason
reason2, (Environment
env2, model Symbolic
_, Counter
_, model Concrete
_)) <- StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
2) Check
CheckPrecondition Commands cmd resp
cmds2)
(Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
(Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go ( String -> Reason
ExceptionThrown String
e
, Reason
reason2
, Environment
env2
) [Pair (Commands cmd resp)]
pairs
go out :: (Reason, Reason, Environment)
out@(ExceptionThrown String
_, ExceptionThrown String
_, Environment
_env) (Pair (Commands cmd resp)
_ : [Pair (Commands cmd resp)]
_) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason, Reason, Environment)
out
go out :: (Reason, Reason, Environment)
out@(PreconditionFailed {}, ExceptionThrown String
_, Environment
_env) (Pair (Commands cmd resp)
_ : [Pair (Commands cmd resp)]
_) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason, Reason, Environment)
out
go out :: (Reason, Reason, Environment)
out@(ExceptionThrown String
_, PreconditionFailed {}, Environment
_env) (Pair (Commands cmd resp)
_ : [Pair (Commands cmd resp)]
_) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason, Reason, Environment)
out
go (Reason
res1, Reason
res2, Environment
_env) (Pair Commands cmd resp
_cmds1 Commands cmd resp
_cmds2 : [Pair (Commands cmd resp)]
_pairs) =
String -> m (Reason, Reason, Environment)
forall a. HasCallStack => String -> a
error (String
"executeParallelCommands, unexpected result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Reason, Reason) -> String
forall a. Show a => a -> String
show (Reason
res1, Reason
res2))
logicReason :: Reason -> Logic
logicReason :: Reason -> Logic
logicReason Reason
Ok = Logic
Top
logicReason Reason
r = String -> Logic -> Logic
Annotate (Reason -> String
forall a. Show a => a -> String
show Reason
r) Logic
Bot
executeNParallelCommands :: (Rank2.Traversable cmd, Show (cmd Concrete), Rank2.Foldable resp)
=> Show (resp Concrete)
=> (MonadMask m, MonadUnliftIO m)
=> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> UIO.TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Traversable cmd, Show (cmd Concrete), Foldable resp,
Show (resp Concrete), MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands sm :: StateMachine model cmd m resp
sm@StateMachine{ 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 } (ParallelCommands Commands cmd resp
prefix [[Commands cmd resp]]
suffixes) TChan (Pid, HistoryEvent cmd resp)
hchan Bool
stopOnError = do
(Reason
reason0, (Environment
env0, model Symbolic
_smodel, Counter
_counter, model Concrete
cmodel)) <- StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
0) Check
CheckEverything Commands cmd resp
prefix)
(Environment
emptyEnvironment, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
if Reason
reason0 Reason -> Reason -> Bool
forall a. Eq a => a -> a -> Bool
/= Reason
Ok
then do
[(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
(History cmd resp, model Concrete, Reason)
-> m (History cmd resp, model Concrete, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, Reason
reason0)
else do
(Map Int Reason
errors, Environment
_) <- (Map Int Reason, Environment)
-> [[Commands cmd resp]] -> m (Map Int Reason, Environment)
go (Map Int Reason
forall k a. Map k a
Map.empty, Environment
env0) [[Commands cmd resp]]
suffixes
[(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
(History cmd resp, model Concrete, Reason)
-> m (History cmd resp, model Concrete, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, [Reason] -> Reason
combineReasons ([Reason] -> Reason) -> [Reason] -> Reason
forall a b. (a -> b) -> a -> b
$ Map Int Reason -> [Reason]
forall k a. Map k a -> [a]
Map.elems Map Int Reason
errors)
where
go :: (Map Int Reason, Environment)
-> [[Commands cmd resp]] -> m (Map Int Reason, Environment)
go (Map Int Reason, Environment)
res [] = (Map Int Reason, Environment) -> m (Map Int Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Reason, Environment)
res
go (Map Int Reason
previousErrors, Environment
env) ([Commands cmd resp]
suffix : [[Commands cmd resp]]
rest) = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Reason] -> Bool
isInvalid ([Reason] -> Bool) -> [Reason] -> Bool
forall a b. (a -> b) -> a -> b
$ Map Int Reason -> [Reason]
forall k a. Map k a -> [a]
Map.elems Map Int Reason
previousErrors) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
String -> m ()
forall a. HasCallStack => String -> a
error (String
"executeNParallelCommands, unexpected result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Map Int Reason -> String
forall a. Show a => a -> String
show Map Int Reason
previousErrors)
let noError :: Bool
noError = Map Int Reason -> Bool
forall k a. Map k a -> Bool
Map.null Map Int Reason
previousErrors
check :: Check
check = if Bool
noError then Check
CheckNothing else Check
CheckPrecondition
[(Maybe (Int, Reason), Environment)]
res <- [(Int, Commands cmd resp)]
-> ((Int, Commands cmd resp)
-> m (Maybe (Int, Reason), Environment))
-> m [(Maybe (Int, Reason), Environment)]
forall (m :: * -> *) (t :: * -> *) a b.
(MonadUnliftIO m, Traversable t) =>
t a -> (a -> m b) -> m (t b)
forConcurrently ([Int] -> [Commands cmd resp] -> [(Int, Commands cmd resp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Commands cmd resp]
suffix) (((Int, Commands cmd resp) -> m (Maybe (Int, Reason), Environment))
-> m [(Maybe (Int, Reason), Environment)])
-> ((Int, Commands cmd resp)
-> m (Maybe (Int, Reason), Environment))
-> m [(Maybe (Int, Reason), Environment)]
forall a b. (a -> b) -> a -> b
$ \(Int
i, Commands cmd resp
cmds) ->
case Int -> Map Int Reason -> Maybe Reason
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int Reason
previousErrors of
Maybe Reason
Nothing -> do
(Reason
reason, (Environment
env', model Symbolic
_, Counter
_, model Concrete
_)) <- StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
(Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(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
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
i) Check
check Commands cmd resp
cmds) (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
(Maybe (Int, Reason), Environment)
-> m (Maybe (Int, Reason), Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Reason -> Bool
isOK Reason
reason then Maybe (Int, Reason)
forall a. Maybe a
Nothing else (Int, Reason) -> Maybe (Int, Reason)
forall a. a -> Maybe a
Just (Int
i, Reason
reason), Environment
env')
Just Reason
_ -> (Maybe (Int, Reason), Environment)
-> m (Maybe (Int, Reason), Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Int, Reason)
forall a. Maybe a
Nothing, Environment
env)
let newErrors :: Map Int Reason
newErrors = [(Int, Reason)] -> Map Int Reason
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Reason)] -> Map Int Reason)
-> [(Int, Reason)] -> Map Int Reason
forall a b. (a -> b) -> a -> b
$ ((Maybe (Int, Reason), Environment) -> Maybe (Int, Reason))
-> [(Maybe (Int, Reason), Environment)] -> [(Int, Reason)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Int, Reason), Environment) -> Maybe (Int, Reason)
forall a b. (a, b) -> a
fst [(Maybe (Int, Reason), Environment)]
res
errors :: Map Int Reason
errors = Map Int Reason -> Map Int Reason -> Map Int Reason
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Int Reason
previousErrors Map Int Reason
newErrors
newEnv :: Environment
newEnv = [Environment] -> Environment
forall a. Monoid a => [a] -> a
mconcat ([Environment] -> Environment) -> [Environment] -> Environment
forall a b. (a -> b) -> a -> b
$ (Maybe (Int, Reason), Environment) -> Environment
forall a b. (a, b) -> b
snd ((Maybe (Int, Reason), Environment) -> Environment)
-> [(Maybe (Int, Reason), Environment)] -> [Environment]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe (Int, Reason), Environment)]
res
case (Bool
stopOnError, Map Int Reason -> Bool
forall k a. Map k a -> Bool
Map.null Map Int Reason
errors) of
(Bool
True, Bool
False) -> (Map Int Reason, Environment) -> m (Map Int Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Reason
errors, Environment
newEnv)
(Bool, Bool)
_ -> (Map Int Reason, Environment)
-> [[Commands cmd resp]] -> m (Map Int Reason, Environment)
go (Map Int Reason
errors, Environment
newEnv) [[Commands cmd resp]]
rest
combineReasons :: [Reason] -> Reason
combineReasons :: [Reason] -> Reason
combineReasons [Reason]
ls = Reason -> Maybe Reason -> Reason
forall a. a -> Maybe a -> a
fromMaybe Reason
Ok ((Reason -> Bool) -> [Reason] -> Maybe Reason
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Reason -> Reason -> Bool
forall a. Eq a => a -> a -> Bool
/= Reason
Ok) [Reason]
ls)
isInvalid :: [Reason] -> Bool
isInvalid :: [Reason] -> Bool
isInvalid [Reason]
ls = (Reason -> Bool) -> [Reason] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Reason -> Bool
isPreconditionFailed [Reason]
ls Bool -> Bool -> Bool
&&
(Reason -> Bool) -> [Reason] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Reason -> Bool
notException [Reason]
ls
where
notException :: Reason -> Bool
notException (ExceptionThrown String
_) = Bool
False
notException Reason
_ = Bool
True
isPreconditionFailed :: Reason -> Bool
isPreconditionFailed :: Reason -> Bool
isPreconditionFailed PreconditionFailed {} = Bool
True
isPreconditionFailed Reason
_ = Bool
False
linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete))
=> StateMachine model cmd m resp -> History cmd resp -> Logic
linearise :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise 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, model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition, 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 } = [(Pid, HistoryEvent cmd resp)] -> Logic
go ([(Pid, HistoryEvent cmd resp)] -> Logic)
-> (History cmd resp -> [(Pid, HistoryEvent cmd resp)])
-> History cmd resp
-> Logic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History cmd resp -> [(Pid, HistoryEvent cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
where
go :: [(Pid, HistoryEvent cmd resp)] -> Logic
go :: [(Pid, HistoryEvent cmd resp)] -> Logic
go [] = Logic
Top
go [(Pid, HistoryEvent cmd resp)]
es = [Tree (Operation cmd resp)]
-> (Tree (Operation cmd resp) -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
exists ([(Pid, HistoryEvent cmd resp)] -> [Tree (Operation cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> Forest (Operation cmd resp)
interleavings [(Pid, HistoryEvent cmd resp)]
es) (model Concrete -> Tree (Operation cmd resp) -> Logic
step model Concrete
forall (r :: * -> *). model r
initModel)
step :: model Concrete -> Tree (Operation cmd resp) -> Logic
step :: model Concrete -> Tree (Operation cmd resp) -> Logic
step model Concrete
_model (Node (Crash cmd Concrete
_cmd String
_err Pid
_pid) [Tree (Operation cmd resp)]
_roses) =
String -> Logic
forall a. HasCallStack => String -> a
error String
"Not implemented yet, see issue #162 for more details."
step model Concrete
model (Node (Operation cmd Concrete
cmd resp Concrete
resp Pid
_) [Tree (Operation cmd resp)]
roses) =
model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition model Concrete
model cmd Concrete
cmd resp Concrete
resp Logic -> Logic -> Logic
.&&
[Tree (Operation cmd resp)]
-> (Tree (Operation cmd resp) -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
exists' [Tree (Operation cmd resp)]
roses (model Concrete -> Tree (Operation cmd resp) -> Logic
step (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
model cmd Concrete
cmd resp Concrete
resp))
exists' :: Show a => [a] -> (a -> Logic) -> Logic
exists' :: forall a. Show a => [a] -> (a -> Logic) -> Logic
exists' [] a -> Logic
_ = Logic
Top
exists' [a]
xs a -> Logic
p = [a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
exists [a]
xs a -> Logic
p
prettyParallelCommandsWithOpts :: (MonadIO m, Rank2.Foldable cmd)
=> (Show (cmd Concrete), Show (resp Concrete))
=> ParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyParallelCommandsWithOpts :: forall (m :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
a.
(MonadIO m, Foldable cmd, Show (cmd Concrete),
Show (resp Concrete)) =>
ParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyParallelCommandsWithOpts ParallelCommands cmd resp
cmds Maybe GraphOptions
mGraphOptions [(History cmd resp, a, Logic)]
histories = do
((History cmd resp, a, Logic) -> PropertyM m ())
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(History cmd resp
h, a
_, Logic
l) -> History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
h (Logic -> Value
logic Logic
l) IO () -> Property -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` Bool -> Property
forall prop. Testable prop => prop -> Property
property (Logic -> Bool
boolean Logic
l)) [(History cmd resp, a, Logic)]
histories
where
printCounterexample :: History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
hist' (VFalse Counterexample
ce) = do
Doc -> IO ()
PP.putDoc (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$
[Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
[ Doc
PP.line
, String -> Doc
PP.string (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ ParallelCommands cmd resp -> History cmd resp -> Doc
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) =>
ParallelCommands cmd resp -> History cmd resp -> Doc
toBoxDrawings ParallelCommands cmd resp
cmds History cmd resp
hist')
, String -> Doc
PP.string (Counterexample -> String
forall a. Show a => a -> String
show (Counterexample -> String) -> Counterexample -> String
forall a b. (a -> b) -> a -> b
$ Counterexample -> Counterexample
simplify Counterexample
ce)
, Doc
PP.line
, Doc
PP.line
, String -> Doc
PP.string (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Logic -> Bool
boolean Logic
l | (History cmd resp
_, a
_, Logic
l) <- [(History cmd resp, a, Logic)]
histories]
then String
"However, some repetitions of this sequence of commands passed. Maybe there is a race condition?"
else String
"And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently"
, Doc
PP.line
]
case Maybe GraphOptions
mGraphOptions of
Maybe GraphOptions
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just GraphOptions
gOptions -> ParallelCommands cmd resp
-> GraphOptions -> History cmd resp -> IO ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(t :: * -> *).
(Foldable t, Foldable cmd, Show (cmd Concrete),
Show (resp Concrete)) =>
ParallelCommandsF t cmd resp
-> GraphOptions -> History cmd resp -> IO ()
createAndPrintDot ParallelCommands cmd resp
cmds GraphOptions
gOptions History cmd resp
hist'
printCounterexample History cmd resp
_hist Value
_
= String -> IO ()
forall a. HasCallStack => String -> a
error String
"prettyParallelCommands: impossible, because `boolean l` was False."
simplify :: Counterexample -> Counterexample
simplify :: Counterexample -> Counterexample
simplify (Fst ce :: Counterexample
ce@(AnnotateC String
_ Counterexample
BotC)) = Counterexample
ce
simplify (Snd Counterexample
ce) = Counterexample -> Counterexample
simplify Counterexample
ce
simplify (ExistsC [] []) = Counterexample
BotC
simplify (ExistsC [a]
_ [Fst Counterexample
ce]) = Counterexample
ce
simplify (ExistsC [a]
x (Fst Counterexample
ce : [Counterexample]
ces)) = Counterexample
ce Counterexample -> Counterexample -> Counterexample
`EitherC` Counterexample -> Counterexample
simplify ([a] -> [Counterexample] -> Counterexample
forall a. Show a => [a] -> [Counterexample] -> Counterexample
ExistsC [a]
x [Counterexample]
ces)
simplify (ExistsC [a]
_ (Snd Counterexample
ce : [Counterexample]
_)) = Counterexample -> Counterexample
simplify Counterexample
ce
simplify Counterexample
_ = String -> Counterexample
forall a. HasCallStack => String -> a
error String
"simplify: impossible,\
\ because of the structure of linearise."
prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
=> MonadIO m
=> Rank2.Foldable cmd
=> ParallelCommands cmd resp
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
Foldable cmd) =>
ParallelCommands cmd resp
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyParallelCommands ParallelCommands cmd resp
cmds = ParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
forall (m :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
a.
(MonadIO m, Foldable cmd, Show (cmd Concrete),
Show (resp Concrete)) =>
ParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyParallelCommandsWithOpts ParallelCommands cmd resp
cmds Maybe GraphOptions
forall a. Maybe a
Nothing
prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete))
=> MonadIO m
=> Rank2.Foldable cmd
=> NParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyNParallelCommandsWithOpts :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
Foldable cmd) =>
NParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyNParallelCommandsWithOpts NParallelCommands cmd resp
cmds Maybe GraphOptions
mGraphOptions [(History cmd resp, a, Logic)]
histories =
((History cmd resp, a, Logic) -> PropertyM m ())
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(History cmd resp
h, a
_, Logic
l) -> History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
h (Logic -> Value
logic Logic
l) IO () -> Property -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` Bool -> Property
forall prop. Testable prop => prop -> Property
property (Logic -> Bool
boolean Logic
l)) [(History cmd resp, a, Logic)]
histories
where
printCounterexample :: History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
hist' (VFalse Counterexample
ce) = do
Doc -> IO ()
PP.putDoc (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$
[Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
[ Doc
PP.line
, String -> Doc
PP.string (Counterexample -> String
forall a. Show a => a -> String
show (Counterexample -> String) -> Counterexample -> String
forall a b. (a -> b) -> a -> b
$ Counterexample -> Counterexample
simplify Counterexample
ce)
, Doc
PP.line
, Doc
PP.line
, String -> Doc
PP.string (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Logic -> Bool
boolean Logic
l | (History cmd resp
_, a
_, Logic
l) <- [(History cmd resp, a, Logic)]
histories]
then String
"However, some repetitions of this sequence of commands passed. Maybe there is a race condition?"
else String
"And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently"
, Doc
PP.line
]
case Maybe GraphOptions
mGraphOptions of
Maybe GraphOptions
Nothing -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just GraphOptions
gOptions -> NParallelCommands cmd resp
-> GraphOptions -> History cmd resp -> IO ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(t :: * -> *).
(Foldable t, Foldable cmd, Show (cmd Concrete),
Show (resp Concrete)) =>
ParallelCommandsF t cmd resp
-> GraphOptions -> History cmd resp -> IO ()
createAndPrintDot NParallelCommands cmd resp
cmds GraphOptions
gOptions History cmd resp
hist'
printCounterexample History cmd resp
_hist Value
_
= String -> IO ()
forall a. HasCallStack => String -> a
error String
"prettyNParallelCommands: impossible, because `boolean l` was False."
prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
=> MonadIO m
=> Rank2.Foldable cmd
=> NParallelCommands cmd resp
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
Foldable cmd) =>
NParallelCommands cmd resp
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyNParallelCommands NParallelCommands cmd resp
cmds = NParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
Foldable cmd) =>
NParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyNParallelCommandsWithOpts NParallelCommands cmd resp
cmds Maybe GraphOptions
forall a. Maybe a
Nothing
toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd
=> (Show (cmd Concrete), Show (resp Concrete))
=> ParallelCommands cmd resp -> History cmd resp -> Doc
toBoxDrawings :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) =>
ParallelCommands cmd resp -> History cmd resp -> Doc
toBoxDrawings (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes) = Set Var -> History cmd resp -> Doc
toBoxDrawings'' Set Var
allVars
where
allVars :: Set Var
allVars = Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars Commands cmd resp
prefix Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.union`
(Pair (Commands cmd resp) -> Set Var)
-> [Pair (Commands cmd resp)] -> Set Var
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Commands cmd resp -> Set Var)
-> Pair (Commands cmd resp) -> Set Var
forall m a. Monoid m => (a -> m) -> Pair a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars) [Pair (Commands cmd resp)]
suffixes
toBoxDrawings'' :: Set Var -> History cmd resp -> Doc
toBoxDrawings'' :: Set Var -> History cmd resp -> Doc
toBoxDrawings'' Set Var
knownVars (History History' cmd resp
h) = [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
([ [(EventType, Pid)] -> Fork [String] -> Doc
exec [(EventType, Pid)]
evT (((Pid, HistoryEvent cmd resp) -> String)
-> History' cmd resp -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HistoryEvent cmd resp -> String
out (HistoryEvent cmd resp -> String)
-> ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp
forall a b. (a, b) -> b
snd) (History' cmd resp -> [String])
-> Fork (History' cmd resp) -> Fork [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> History' cmd resp
-> History' cmd resp
-> History' cmd resp
-> Fork (History' cmd resp)
forall a. a -> a -> a -> Fork a
Fork History' cmd resp
l History' cmd resp
p History' cmd resp
r)
, Doc
PP.line
, Doc
PP.line
]
[Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Int, String) -> Doc) -> [(Int, String)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String) -> Doc
ppException [(Int, String)]
exceptions
)
where
(Int
_, [(Int, String)]
exceptions, History' cmd resp
h'') = ((Int, [(Int, String)], History' cmd resp)
-> (Pid, HistoryEvent cmd resp)
-> (Int, [(Int, String)], History' cmd resp))
-> (Int, [(Int, String)], History' cmd resp)
-> History' cmd resp
-> (Int, [(Int, String)], History' cmd resp)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
(\(Int
i, [(Int, String)]
excs, History' cmd resp
evs) (Pid
pid, HistoryEvent cmd resp
ev) ->
case HistoryEvent cmd resp
ev of
Exception String
err -> (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, [(Int, String)]
excs [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [(Int
i, String
err)], History' cmd resp
evs History' cmd resp -> History' cmd resp -> History' cmd resp
forall a. [a] -> [a] -> [a]
++ [(Pid
pid, String -> HistoryEvent cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
String -> HistoryEvent cmd resp
Exception (String -> HistoryEvent cmd resp)
-> String -> HistoryEvent cmd resp
forall a b. (a -> b) -> a -> b
$ String
"Exception " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)])
HistoryEvent cmd resp
_ -> (Int
i, [(Int, String)]
excs, History' cmd resp
evs History' cmd resp -> History' cmd resp -> History' cmd resp
forall a. [a] -> [a] -> [a]
++ [(Pid
pid, HistoryEvent cmd resp
ev)])
)
(Int
0 :: Int, [], [])
History' cmd resp
h
(History' cmd resp
p, History' cmd resp
h') = ((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> (History' cmd resp, History' cmd resp)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> Pid -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Pid
Pid Int
0) History' cmd resp
h''
(History' cmd resp
l, History' cmd resp
r) = ((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> (History' cmd resp, History' cmd resp)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> Pid -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Pid
Pid Int
1) History' cmd resp
h'
out :: HistoryEvent cmd resp -> String
out :: HistoryEvent cmd resp -> String
out (Invocation cmd Concrete
cmd Set Var
vars)
| Set Var
vars Set Var -> Set Var -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Var
knownVars = [Var] -> String
forall a. Show a => a -> String
show (Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
vars) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ← " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
| Bool
otherwise = cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
out (Response resp Concrete
resp) = resp Concrete -> String
forall a. Show a => a -> String
show resp Concrete
resp
out (Exception String
err) = String
err
toEventType :: History' cmd resp -> [(EventType, Pid)]
toEventType :: History' cmd resp -> [(EventType, Pid)]
toEventType = ((Pid, HistoryEvent cmd resp) -> (EventType, Pid))
-> History' cmd resp -> [(EventType, Pid)]
forall a b. (a -> b) -> [a] -> [b]
map (Pid, HistoryEvent cmd resp) -> (EventType, Pid)
forall {b} {cmd :: (* -> *) -> *} {resp :: (* -> *) -> *}.
(b, HistoryEvent cmd resp) -> (EventType, b)
go
where
go :: (b, HistoryEvent cmd resp) -> (EventType, b)
go (b, HistoryEvent cmd resp)
e = case (b, HistoryEvent cmd resp)
e of
(b
pid, Invocation cmd Concrete
_ Set Var
_) -> (EventType
Open, b
pid)
(b
pid, Response resp Concrete
_) -> (EventType
Close, b
pid)
(b
pid, Exception String
_) -> (EventType
Close, b
pid)
evT :: [(EventType, Pid)]
evT :: [(EventType, Pid)]
evT = History' cmd resp -> [(EventType, Pid)]
toEventType (((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> History' cmd resp
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> [Pid] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`Prelude.elem` (Int -> Pid) -> [Int] -> [Pid]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Pid
Pid [Int
1, Int
2]) History' cmd resp
h)
ppException :: (Int, String) -> Doc
ppException :: (Int, String) -> Doc
ppException (Int
idx, String
err) = [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
[ String -> Doc
PP.string (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Exception " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
idx String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
":"
, Doc
PP.line
, Int -> Doc -> Doc
PP.indent Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
PP.string String
err
, Doc
PP.line
, Doc
PP.line
]
createAndPrintDot :: forall cmd resp t. Foldable t => Rank2.Foldable cmd
=> (Show (cmd Concrete), Show (resp Concrete))
=> ParallelCommandsF t cmd resp
-> GraphOptions
-> History cmd resp
-> IO ()
createAndPrintDot :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(t :: * -> *).
(Foldable t, Foldable cmd, Show (cmd Concrete),
Show (resp Concrete)) =>
ParallelCommandsF t cmd resp
-> GraphOptions -> History cmd resp -> IO ()
createAndPrintDot (ParallelCommands Commands cmd resp
prefix [t (Commands cmd resp)]
suffixes) GraphOptions
gOptions = Set Var -> History cmd resp -> IO ()
toDotGraph Set Var
allVars
where
allVars :: Set Var
allVars = Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars Commands cmd resp
prefix Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.union`
(t (Commands cmd resp) -> Set Var)
-> [t (Commands cmd resp)] -> Set Var
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Commands cmd resp -> Set Var) -> t (Commands cmd resp) -> Set Var
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars) [t (Commands cmd resp)]
suffixes
toDotGraph :: Set Var -> History cmd resp -> IO ()
toDotGraph :: Set Var -> History cmd resp -> IO ()
toDotGraph Set Var
knownVars (History History' cmd resp
h) = GraphOptions -> Rose [String] -> IO ()
printDotGraph GraphOptions
gOptions (Rose [String] -> IO ()) -> Rose [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ (HistoryEvent cmd resp -> String)
-> [HistoryEvent cmd resp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HistoryEvent cmd resp -> String
out ([HistoryEvent cmd resp] -> [String])
-> Rose [HistoryEvent cmd resp] -> Rose [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HistoryEvent cmd resp]
-> Map Pid [HistoryEvent cmd resp] -> Rose [HistoryEvent cmd resp]
forall a. a -> Map Pid a -> Rose a
Rose ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp
forall a b. (a, b) -> b
snd ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp)
-> History' cmd resp -> [HistoryEvent cmd resp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> History' cmd resp
prefixMessages) Map Pid [HistoryEvent cmd resp]
groupByPid
where
(History' cmd resp
prefixMessages, History' cmd resp
h') = ((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> (History' cmd resp, History' cmd resp)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> Pid -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Pid
Pid Int
0) History' cmd resp
h
alterF :: a -> Maybe [a] -> Maybe [a]
alterF a
a Maybe [a]
Nothing = [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
a]
alterF a
a (Just [a]
ls) = [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ls
groupByPid :: Map Pid [HistoryEvent cmd resp]
groupByPid = ((Pid, HistoryEvent cmd resp)
-> Map Pid [HistoryEvent cmd resp]
-> Map Pid [HistoryEvent cmd resp])
-> Map Pid [HistoryEvent cmd resp]
-> History' cmd resp
-> Map Pid [HistoryEvent cmd resp]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Pid
p,HistoryEvent cmd resp
e) Map Pid [HistoryEvent cmd resp]
m -> (Maybe [HistoryEvent cmd resp] -> Maybe [HistoryEvent cmd resp])
-> Pid
-> Map Pid [HistoryEvent cmd resp]
-> Map Pid [HistoryEvent cmd resp]
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter (HistoryEvent cmd resp
-> Maybe [HistoryEvent cmd resp] -> Maybe [HistoryEvent cmd resp]
forall {a}. a -> Maybe [a] -> Maybe [a]
alterF HistoryEvent cmd resp
e) Pid
p Map Pid [HistoryEvent cmd resp]
m) Map Pid [HistoryEvent cmd resp]
forall k a. Map k a
Map.empty History' cmd resp
h'
out :: HistoryEvent cmd resp -> String
out :: HistoryEvent cmd resp -> String
out (Invocation cmd Concrete
cmd Set Var
vars)
| Set Var
vars Set Var -> Set Var -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Var
knownVars = [Var] -> String
forall a. Show a => a -> String
show (Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
vars) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ← " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
| Bool
otherwise = cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
out (Response resp Concrete
resp) = String
" → " String -> String -> String
forall a. [a] -> [a] -> [a]
++ resp Concrete -> String
forall a. Show a => a -> String
show resp Concrete
resp
out (Exception String
err) = String
" → " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err
getAllUsedVars :: Rank2.Foldable cmd => Commands cmd resp -> Set Var
getAllUsedVars :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars = [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList ([Var] -> Set Var)
-> (Commands cmd resp -> [Var]) -> Commands cmd resp -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Command cmd resp -> [Var]) -> [Command cmd resp] -> [Var]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Command cmd Symbolic
cmd resp Symbolic
_ [Var]
_) -> cmd Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars cmd Symbolic
cmd) ([Command cmd resp] -> [Var])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd
=> ParallelCommandsF t cmd resp -> Property -> Property
checkCommandNamesParallel :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(t :: * -> *).
(Foldable t, CommandNames cmd) =>
ParallelCommandsF t cmd resp -> Property -> Property
checkCommandNamesParallel ParallelCommandsF t cmd resp
cmds = Commands cmd resp -> Property -> Property
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
checkCommandNames (Commands cmd resp -> Property -> Property)
-> Commands cmd resp -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential ParallelCommandsF t cmd resp
cmds
coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd
=> ParallelCommandsF t cmd resp -> Property -> Property
coverCommandNamesParallel :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(t :: * -> *).
(Foldable t, CommandNames cmd) =>
ParallelCommandsF t cmd resp -> Property -> Property
coverCommandNamesParallel ParallelCommandsF t cmd resp
cmds = Commands cmd resp -> Property -> Property
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
coverCommandNames (Commands cmd resp -> Property -> Property)
-> Commands cmd resp -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential ParallelCommandsF t cmd resp
cmds
commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd
=> ParallelCommandsF t cmd resp -> [(String, Int)]
commandNamesParallel :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
(t :: * -> *).
(Foldable t, CommandNames cmd) =>
ParallelCommandsF t cmd resp -> [(String, Int)]
commandNamesParallel = Commands cmd resp -> [(String, Int)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames (Commands cmd resp -> [(String, Int)])
-> (ParallelCommandsF t cmd resp -> Commands cmd resp)
-> ParallelCommandsF t cmd resp
-> [(String, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential
toSequential :: Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential :: forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential ParallelCommandsF t cmd resp
cmds = ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
ParallelCommandsF t cmd resp -> Commands cmd resp
prefix ParallelCommandsF t cmd resp
cmds Commands cmd resp -> Commands cmd resp -> Commands cmd resp
forall a. Semigroup a => a -> a -> a
<> [Commands cmd resp] -> Commands cmd resp
forall a. Monoid a => [a] -> a
mconcat ((t (Commands cmd resp) -> [Commands cmd resp])
-> [t (Commands cmd resp)] -> [Commands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap t (Commands cmd resp) -> [Commands cmd resp]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (ParallelCommandsF t cmd resp -> [t (Commands cmd resp)]
forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
ParallelCommandsF t cmd resp -> [t (Commands cmd resp)]
suffixes ParallelCommandsF t cmd resp
cmds))