{-# 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)
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
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 =
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (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) (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) 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 =
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (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) (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) 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 (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } Maybe Int
mminSize = do
Commands [Command cmd resp]
cmds <- 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 <- forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
k forall a. Integral a => a -> a -> a
`div` Int
3))
let (Commands cmd resp
prefix, Commands cmd resp
rest) = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (forall a. Int -> [a] -> ([a], [a])
splitAt Int
prefixLength [Command cmd resp]
cmds)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 (forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm 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 [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 [] = 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 (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 (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe))
(forall a. a -> a -> Pair a
Pair (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe1) (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe2) forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
acc)
[Command cmd resp]
rest
where
([Command cmd resp]
safe, [Command cmd resp]
rest) = 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) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe 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 [] = (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)
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe forall a. Ord a => a -> a -> Bool
<= Int
5
, 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 (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (Command cmd resp
cmd forall a. a -> [a] -> [a]
: [Command cmd resp]
safe))
= 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 forall a. a -> [a] -> [a]
: [Command cmd resp]
safe) [Command cmd resp]
cmds
| Bool
otherwise
= (forall a. [a] -> [a]
reverse [Command cmd resp]
safe, Command cmd resp
cmd 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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } Int
np =
if Int
np forall a. Ord a => a -> a -> Bool
<= Int
0 then forall a. HasCallStack => String -> a
error String
"number of threads must be positive" else do
Commands [Command cmd resp]
cmds <- 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 forall a. Maybe a
Nothing
Int
prefixLength <- forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
k forall a. Integral a => a -> a -> a
`div` Int
3))
let (Commands cmd resp
prefix, Commands cmd resp
rest) = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (forall a. Int -> [a] -> ([a], [a])
splitAt Int
prefixLength [Command cmd resp]
cmds)
forall (m :: * -> *) a. Monad m => a -> m a
return (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 (forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm 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 [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 [] = 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 (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 (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe))
([Commands cmd resp]
safes forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
acc)
[Command cmd resp]
rest
where
([Command cmd resp]
safe, [Command cmd resp]
rest) = 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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Int -> [a] -> [[a]]
chunksOf Int
np (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe 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 forall a. a -> [a] -> [a]
: forall a. Int -> Int -> [a] -> [[a]]
chunksOf (Int
nforall a. Num a => a -> a -> a
-Int
1) Int
len [a]
bs
where ([a]
as, [a]
bs) = 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 :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition :: model Symbolic -> cmd Symbolic -> Logic
precondition, 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 -> 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 -> cmd Symbolic -> GenSym (resp Symbolic)
mock } model Symbolic
model0
= forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (model Symbolic -> [Command cmd resp] -> Bool
preconditionsHold model Symbolic
model0)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [[a]]
permutations
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (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
&&
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vars forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ 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 (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
model0 =
model Symbolic -> [Command cmd resp] -> model Symbolic
go model Symbolic
model0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (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)
= forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk (ParallelCommandsF Pair cmd resp)
-> [ParallelCommandsF Pair cmd resp]
go
[ forall a. Bool -> a -> Shrunk a
Shrunk Bool
s (forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' (forall a b. (a -> b) -> [a] -> [b]
map 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') <- forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS 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, forall a b. (a -> b) -> [a] -> [b]
map forall a. Pair a -> (a, a)
fromPair [Pair (Commands cmd resp)]
suffixes)
]
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) =
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 = forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS (forall a. (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
shrinkPairS' 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') ->
[ forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands (Commands cmd resp
prefix forall a. Semigroup a => a -> a -> a
<> forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp
prefix'])
(forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (forall a. (a, a) -> Pair a
toPair ([Command cmd resp], [Command cmd resp])
suffix') forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
suffixes')
| (Command cmd resp
prefix', ([Command cmd resp], [Command cmd resp])
suffix') <- forall a. ([a], [a]) -> [(a, ([a], [a]))]
pickOneReturnRest2 (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (forall a. Pair a -> a
proj1 Pair (Commands cmd resp)
suffix),
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (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)
= forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk (ParallelCommandsF [] cmd resp)
-> [ParallelCommandsF [] cmd resp]
go
[ forall a. Bool -> a -> Shrunk a
Shrunk Bool
s (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') <- forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS 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)
]
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) =
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 = forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS (forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS'' 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') ->
[ forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands (Commands cmd resp
prefix forall a. Semigroup a => a -> a -> a
<> forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp
prefix'])
(forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [[Command cmd resp]]
suffix' forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
suffixes')
| (Command cmd resp
prefix', [[Command cmd resp]]
suffix') <- forall a. [[a]] -> [(a, [[a]])]
pickOneReturnRestL (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands 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' = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [Shrunk [a]]
shrinkListS' forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } = \ShouldShrink
shouldShrink (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes) ->
let env :: ValidateEnv model
env = forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv 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 -> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (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 -> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (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)
forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
MustShrink) (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 [] = [forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' (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') <- 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') <- 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 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' (forall a. a -> a -> Pair a
Pair Commands cmd resp
l' Commands cmd resp
r' forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
acc) (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 = forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm (forall (model :: (* -> *) -> *).
ValidateEnv model -> model Symbolic
veModel ValidateEnv model
envL) Commands cmd resp
cmds
, veScope :: Map Var Var
veScope = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope ValidateEnv model
envL) (forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope ValidateEnv model
envR)
, veCounter :: Counter
veCounter = 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 :: Counter
veCounter = forall (model :: (* -> *) -> *). ValidateEnv model -> Counter
veCounter ValidateEnv model
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 = forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv forall a b. (a -> b) -> a -> b
$ 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 -> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (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 -> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (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)
forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
MustShrink) (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 [] = [forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' (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) <- forall a. [a] -> [([(ShouldShrink, a)], ShouldShrink)]
shrinkOpts [Commands cmd resp]
suffix
(ValidateEnv model
envFinal, [Commands cmd resp]
suffix') <- forall a b. (a, b) -> b
snd forall a b. (a -> 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' ((forall a. [a] -> [a]
reverse [Commands cmd resp]
suffix') 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 forall (model :: (* -> *) -> *).
ValidateEnv model -> ValidateEnv model -> ValidateEnv model
`withCounterFrom` ValidateEnv model
envPrev
(ValidateEnv model
env', Commands cmd resp
cmd') <- 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
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'
forall (m :: * -> *) a. Monad m => a -> m a
return (ValidateEnv model
env'', Commands cmd resp
cmd' 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ls
dontShrink :: [ShouldShrink]
dontShrink = forall a. Int -> a -> [a]
replicate Int
len ShouldShrink
DontShrink
shrinks :: [[ShouldShrink]]
shrinks = if Int
len forall a. Eq a => a -> a -> Bool
== Int
0
then forall a. HasCallStack => String -> a
error String
"Invariant violation! A suffix should never be an empty list"
else forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map [Int
1..Int
len] forall a b. (a -> b) -> a -> b
$ \Int
n ->
(forall a. Int -> a -> [a]
replicate (Int
n forall a. Num a => a -> a -> a
- Int
1) ShouldShrink
DontShrink) forall a. [a] -> [a] -> [a]
++ [ShouldShrink
MustShrink] forall a. [a] -> [a] -> [a]
++ (forall a. Int -> a -> [a]
replicate (Int
len forall a. Num a => a -> a -> a
- Int
n) ShouldShrink
DontShrink)
in case ShouldShrink
shouldShrink of
ShouldShrink
DontShrink -> [(forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
dontShrink [a]
ls, ShouldShrink
DontShrink)]
ShouldShrink
MustShrink -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[ShouldShrink]
shrinkLs -> (forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
shrinkLs [a]
ls, ShouldShrink
DontShrink)) [[ShouldShrink]]
shrinks
forall a. [a] -> [a] -> [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 = 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 = 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' = 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 = 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 = 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 = 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 (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 =
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- 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') <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall a b. (a -> b) -> a -> b
$
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
MonadMask m =>
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
_) -> 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)
_ -> forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)
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
.&& 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 =
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
((History cmd resp
hist, model Concrete
model, Reason
_, Reason
_), StateMachine model cmd m resp
sm') <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall a b. (a -> b) -> a -> b
$
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
MonadMask m =>
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
_) -> 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)
_ -> forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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' = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist', model Concrete
model, 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 = 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 (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 =
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
((History cmd resp
hist, model Concrete
model, Reason
reason), StateMachine model cmd m resp
sm') <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall a b. (a -> b) -> a -> b
$
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
MonadMask m =>
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
_) -> 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)
_ -> forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, Reason -> Logic
logicReason Reason
reason Logic -> Logic -> 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 =
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n forall a b. (a -> b) -> a -> b
$ do
TChan (Pid, HistoryEvent cmd resp)
hchan <- forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
((History cmd resp
hist, model Concrete
model, Reason
_reason), StateMachine model cmd m resp
sm') <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall a b. (a -> b) -> a -> b
$
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
MonadMask m =>
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
_) -> 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)
_ -> forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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' = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, 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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> 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)) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(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, forall (r :: * -> *). model r
initModel, Counter
newCounter, forall (r :: * -> *). model r
initModel)
if Reason
reason0 forall a. Eq a => a -> a -> Bool
/= Reason
Ok
then do
[(Pid, HistoryEvent cmd resp)]
hist <- forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
forall (m :: * -> *) a. Monad m => a -> m a
return (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 <- forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
forall (m :: * -> *) a. Monad m => a -> m a
return (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) [] = 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
_))) <- forall (m :: * -> *) a b. MonadUnliftIO m => m a -> m b -> m (a, b)
concurrently
(forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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, forall (r :: * -> *). model r
initModel, Counter
newCounter, forall (r :: * -> *). model r
initModel))
(forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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, forall (r :: * -> *). model r
initModel, Counter
newCounter, forall (r :: * -> *). model r
initModel))
case (Reason -> Bool
isOK forall a b. (a -> b) -> a -> b
$ [Reason] -> Reason
combineReasons [Reason
reason1, Reason
reason2], Bool
stopOnError) of
(Bool
False, Bool
True) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Reason
reason1, Reason
reason2, Environment
env1 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 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
_)) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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, forall (r :: * -> *). model r
initModel, Counter
newCounter, 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
_)) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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, forall (r :: * -> *). model r
initModel, Counter
newCounter, 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)]
_) = 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)]
_) = 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)]
_) = 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) =
forall a. HasCallStack => String -> a
error (String
"executeParallelCommands, unexpected result: " forall a. [a] -> [a] -> [a]
++ 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 (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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> 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)) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(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, forall (r :: * -> *). model r
initModel, Counter
newCounter, forall (r :: * -> *). model r
initModel)
if Reason
reason0 forall a. Eq a => a -> a -> Bool
/= Reason
Ok
then do
[(Pid, HistoryEvent cmd resp)]
hist <- forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
forall (m :: * -> *) a. Monad m => a -> m a
return (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 (forall k a. Map k a
Map.empty, Environment
env0) [[Commands cmd resp]]
suffixes
[(Pid, HistoryEvent cmd resp)]
hist <- forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, [Reason] -> Reason
combineReasons forall a b. (a -> b) -> a -> b
$ 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 [] = 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
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Reason] -> Bool
isInvalid forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems Map Int Reason
previousErrors) forall a b. (a -> b) -> a -> b
$
forall a. HasCallStack => String -> a
error (String
"executeNParallelCommands, unexpected result: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Map Int Reason
previousErrors)
let noError :: Bool
noError = 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 <- forall (m :: * -> *) (t :: * -> *) a b.
(MonadUnliftIO m, Traversable t) =>
t a -> (a -> m b) -> m (t b)
forConcurrently (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Commands cmd resp]
suffix) forall a b. (a -> b) -> a -> b
$ \(Int
i, Commands cmd resp
cmds) ->
case 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
_)) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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, forall (r :: * -> *). model r
initModel, Counter
newCounter, forall (r :: * -> *). model r
initModel)
forall (m :: * -> *) a. Monad m => a -> m a
return (if Reason -> Bool
isOK Reason
reason then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just (Int
i, Reason
reason), Environment
env')
Just Reason
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, Environment
env)
let newErrors :: Map Int Reason
newErrors = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a b. (a, b) -> a
fst [(Maybe (Int, Reason), Environment)]
res
errors :: Map Int Reason
errors = 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 = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe (Int, Reason), Environment)]
res
case (Bool
stopOnError, forall k a. Map k a -> Bool
Map.null Map Int Reason
errors) of
(Bool
True, Bool
False) -> 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 = forall a. a -> Maybe a -> a
fromMaybe Reason
Ok (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (forall a. Eq a => a -> a -> Bool
/= Reason
Ok) [Reason]
ls)
isInvalid :: [Reason] -> Bool
isInvalid :: [Reason] -> Bool
isInvalid [Reason]
ls = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Reason -> Bool
isPreconditionFailed [Reason]
ls Bool -> Bool -> 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 (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 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 :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition, 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 } = [(Pid, HistoryEvent cmd resp)] -> Logic
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. Show a => [a] -> (a -> Logic) -> Logic
exists (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> Forest (Operation cmd resp)
interleavings [(Pid, HistoryEvent cmd resp)]
es) (model Concrete -> Tree (Operation cmd resp) -> Logic
step 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) =
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
.&&
forall a. Show a => [a] -> (a -> Logic) -> Logic
exists' [Tree (Operation cmd resp)]
roses (model Concrete -> Tree (Operation cmd resp) -> Logic
step (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 = 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
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) forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` 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
String -> IO ()
putStrLn String
""
forall a. Show a => a -> IO ()
print (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 -> IO ()
putStrLn String
""
forall a. Show a => a -> IO ()
print (Counterexample -> Counterexample
simplify Counterexample
ce)
String -> IO ()
putStrLn String
""
case Maybe GraphOptions
mGraphOptions of
Maybe GraphOptions
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just GraphOptions
gOptions -> 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
_
= 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 (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
_ = 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 = 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 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 =
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) forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` 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
String -> IO ()
putStrLn String
""
forall a. Show a => a -> IO ()
print (Counterexample -> Counterexample
simplify Counterexample
ce)
String -> IO ()
putStrLn String
""
case Maybe GraphOptions
mGraphOptions of
Maybe GraphOptions
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just GraphOptions
gOptions -> 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
_
= 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 = 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 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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars Commands cmd resp
prefix forall a. Ord a => Set a -> Set a -> Set a
`S.union`
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap 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) = [(EventType, Pid)] -> Fork [String] -> Doc
exec [(EventType, Pid)]
evT (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HistoryEvent cmd resp -> String
out forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> a -> a -> Fork a
Fork History' cmd resp
l History' cmd resp
p History' cmd resp
r)
where
(History' cmd resp
p, History' cmd resp
h') = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e forall a. Eq a => a -> a -> Bool
== Int -> Pid
Pid Int
0) History' cmd resp
h
(History' cmd resp
l, History' cmd resp
r) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e 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 forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Var
knownVars = forall a. Show a => a -> String
show (forall a. Set a -> [a]
S.toList Set Var
vars) forall a. [a] -> [a] -> [a]
++ String
" ← " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show cmd Concrete
cmd
| Bool
otherwise = forall a. Show a => a -> String
show cmd Concrete
cmd
out (Response resp Concrete
resp) = 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 = forall a b. (a -> b) -> [a] -> [b]
map 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 (forall a. (a -> Bool) -> [a] -> [a]
filter (\(Pid, HistoryEvent cmd resp)
e -> forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`Prelude.elem` forall a b. (a -> b) -> [a] -> [b]
map Int -> Pid
Pid [Int
1, Int
2]) History' cmd resp
h)
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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars Commands cmd resp
prefix forall a. Ord a => Set a -> Set a -> Set a
`S.union`
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap 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 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Map Pid a -> Rose a
Rose (forall a b. (a, b) -> b
snd 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') = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e 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 = forall a. a -> Maybe a
Just [a
a]
alterF a
a (Just [a]
ls) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> [a]
: [a]
ls
groupByPid :: Map Pid [HistoryEvent cmd resp]
groupByPid = 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 -> forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter (forall {a}. a -> Maybe [a] -> Maybe [a]
alterF HistoryEvent cmd resp
e) Pid
p Map Pid [HistoryEvent cmd resp]
m) 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 forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Var
knownVars = forall a. Show a => a -> String
show (forall a. Set a -> [a]
S.toList Set Var
vars) forall a. [a] -> [a] -> [a]
++ String
" ← " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show cmd Concrete
cmd
| Bool
otherwise = forall a. Show a => a -> String
show cmd Concrete
cmd
out (Response resp Concrete
resp) = String
" → " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show resp Concrete
resp
out (Exception String
err) = 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 = forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Command cmd Symbolic
cmd resp Symbolic
_ [Var]
_) -> forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars cmd Symbolic
cmd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
checkCommandNames forall a b. (a -> b) -> a -> b
$ 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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
coverCommandNames forall a b. (a -> b) -> a -> b
$ 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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
ParallelCommandsF t cmd resp -> Commands cmd resp
prefix ParallelCommandsF t cmd resp
cmds forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (forall (t :: * -> *) (cmd :: (* -> *) -> *)
(resp :: (* -> *) -> *).
ParallelCommandsF t cmd resp -> [t (Commands cmd resp)]
suffixes ParallelCommandsF t cmd resp
cmds))