{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Parallel -- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH -- License : BSD-style (see the file LICENSE) -- -- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk> -- Stability : provisional -- Portability : non-portable (GHC extensions) -- -- This module contains helpers for generating, shrinking, and checking -- parallel programs. -- ----------------------------------------------------------------------------- module Test.StateMachine.Parallel ( -- forall forAllNParallelCommands , forAllNParallelCommandsNTimes , forAllParallelCommandsNTimes , forAllParallelCommands -- generate , generateNParallelCommands , generateParallelCommands -- shrink , shrinkNParallelCommands , shrinkParallelCommands , shrinkAndValidateNParallel , shrinkAndValidateParallel , shrinkCommands' -- run , runParallelCommands , runParallelCommands' , runNParallelCommands , runNParallelCommands' -- pretty , prettyNParallelCommands , prettyParallelCommands , prettyParallelCommandsWithOpts , prettyNParallelCommandsWithOpts -- misc , advanceModel , checkCommandNamesParallel , coverCommandNamesParallel , commandNamesParallel , linearise , toBoxDrawings , executeParallelCommands ) where import Control.Monad (when) import Control.Monad.Catch (ExitCase(..), MonadMask, generalBracket) import Control.Monad.State.Strict (runStateT) import Data.Bifunctor (bimap) import Data.Foldable (toList) import Data.List (find, foldl', 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 Prettyprinter (Doc) import Test.QuickCheck (Gen, Property, Testable, choose, forAllShrinkShow, property, sized, (.&&.)) import Test.QuickCheck.Monadic (PropertyM, run) import Text.Show.Pretty (ppShow) import UnliftIO (MonadIO, MonadUnliftIO, TChan, concurrently, forConcurrently, newTChanIO) import qualified Prettyprinter as PP import qualified Prettyprinter.Render.Terminal as PP 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 ------------------------------------------------------------------------ forAllParallelCommandsNTimes :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> Int -> (ParallelCommands cmd resp -> prop) -- ^ Predicate. -> Property forAllParallelCommandsNTimes :: 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 -> Int -> (ParallelCommands cmd resp -> prop) -> Property forAllParallelCommandsNTimes StateMachine model cmd m resp sm Maybe Int mminSize Int reps ParallelCommands cmd resp -> prop prop = Gen (ParallelCommands cmd resp) -> (ParallelCommands cmd resp -> [ParallelCommands cmd resp]) -> (ParallelCommands cmd resp -> String) -> (ParallelCommands cmd resp -> Property) -> Property forall prop a. Testable prop => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property forAllShrinkShow (StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp) forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp) generateParallelCommands StateMachine model cmd m resp sm Maybe Int mminSize) (StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] shrinkParallelCommands StateMachine model cmd m resp sm) ParallelCommands cmd resp -> String forall a. Show a => a -> String ppShow (\ParallelCommands cmd resp parCmds -> (Property -> prop -> Property) -> Property -> [prop] -> Property forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl' Property -> prop -> Property forall prop1 prop2. (Testable prop1, Testable prop2) => prop1 -> prop2 -> Property (.&&.) (Bool -> Property forall prop. Testable prop => prop -> Property property Bool True) ([prop] -> Property) -> [prop] -> Property forall a b. (a -> b) -> a -> b $ Int -> prop -> [prop] forall a. Int -> a -> [a] replicate Int reps (prop -> [prop]) -> prop -> [prop] forall a b. (a -> b) -> a -> b $ ParallelCommands cmd resp -> prop prop ParallelCommands cmd resp parCmds) 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) -- ^ Predicate. -> 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 = StateMachine model cmd m resp -> Maybe Int -> Int -> (ParallelCommands cmd resp -> prop) -> Property 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 -> Int -> (ParallelCommands cmd resp -> prop) -> Property forAllParallelCommandsNTimes StateMachine model cmd m resp sm Maybe Int mminSize Int 10 forAllNParallelCommandsNTimes :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Int -- ^ Number of threads -> Int -> (NParallelCommands cmd resp -> prop) -- ^ Predicate. -> Property forAllNParallelCommandsNTimes :: 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 -> Int -> (NParallelCommands cmd resp -> prop) -> Property forAllNParallelCommandsNTimes StateMachine model cmd m resp sm Int np Int reps NParallelCommands cmd resp -> prop prop = Gen (NParallelCommands cmd resp) -> (NParallelCommands cmd resp -> [NParallelCommands cmd resp]) -> (NParallelCommands cmd resp -> String) -> (NParallelCommands cmd resp -> Property) -> Property forall prop a. Testable prop => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property forAllShrinkShow (StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp) forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp) generateNParallelCommands StateMachine model cmd m resp sm Int np) (StateMachine model cmd m resp -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] shrinkNParallelCommands StateMachine model cmd m resp sm) NParallelCommands cmd resp -> String forall a. Show a => a -> String ppShow (\NParallelCommands cmd resp parCmds -> (Property -> prop -> Property) -> Property -> [prop] -> Property forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl' Property -> prop -> Property forall prop1 prop2. (Testable prop1, Testable prop2) => prop1 -> prop2 -> Property (.&&.) (Bool -> Property forall prop. Testable prop => prop -> Property property Bool True) ([prop] -> Property) -> [prop] -> Property forall a b. (a -> b) -> a -> b $ Int -> prop -> [prop] forall a. Int -> a -> [a] replicate Int reps (prop -> [prop]) -> prop -> [prop] forall a b. (a -> b) -> a -> b $ NParallelCommands cmd resp -> prop prop NParallelCommands cmd resp parCmds) forAllNParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Int -- ^ Number of threads -> (NParallelCommands cmd resp -> prop) -- ^ Predicate. -> 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 = StateMachine model cmd m resp -> Int -> Int -> (NParallelCommands cmd resp -> prop) -> Property 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 -> Int -> (NParallelCommands cmd resp -> prop) -> Property forAllNParallelCommandsNTimes StateMachine model cmd m resp sm Int np Int 10 -- | Generate parallel commands. -- -- Parallel commands are generated as follows. We begin by generating -- sequential commands and then splitting this list in two at some index. The -- first half will be used as the prefix. -- -- The second half will be used to build suffixes. For example, starting from -- the following sequential commands: -- -- > [A, B, C, D, E, F, G, H, I] -- -- We split it in two, giving us the prefix and the rest: -- -- > prefix: [A, B] -- > rest: [C, D, E, F, G, H, I] -- -- We advance the model with the prefix. -- -- __Make a suffix__: we take commands from @rest@ as long as these are -- parallel safe (see 'parallelSafe'). This means that the pre-conditions -- (using the \'advanced\' model) of each of those commands will hold no -- matter in which order they are executed. -- -- Say this is true for @[C, D, E]@, but not anymore for @F@, maybe because -- @F@ depends on one of @[C, D, E]@. Then we divide this \'chunk\' in two by -- splitting it in the middle, obtaining @[C]@ and @[D, E]@. These two halves -- of the chunk (stored as a 'Pair') will later be executed in parallel. -- Together they form one suffix. -- -- Then the model is advanced using the whole chunk @[C, D, E]@. Think of it -- as a barrier after executing the two halves of the chunk in parallel. Then -- this process of building a chunk/suffix repeats itself, starting from -- __Make a suffix__ using the \'advanced\' model. -- -- In the end we might end up with something like this: -- -- > ┌─ [C] ──┐ ┌ [F, G] ┐ -- > [A, B] ─┤ ├──┤ │ -- > └ [D, E] ┘ └ [H, I] ┘ -- generateParallelCommands :: forall model cmd m resp. Rank2.Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp) generateParallelCommands :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp) generateParallelCommands sm :: StateMachine model cmd m resp sm@StateMachine { forall (r :: * -> *). model r initModel :: forall (r :: * -> *). model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel } Maybe Int mminSize = do Commands [Command cmd resp] cmds <- StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd resp) forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd resp) generateCommands StateMachine model cmd m resp sm Maybe Int mminSize Int prefixLength <- (Int -> Gen Int) -> Gen Int forall a. (Int -> Gen a) -> Gen a sized (\Int k -> (Int, Int) -> Gen Int forall a. Random a => (a, a) -> Gen a choose (Int 0, Int k Int -> Int -> Int forall a. Integral a => a -> a -> a `div` Int 3)) let (Commands cmd resp prefix, Commands cmd resp rest) = ([Command cmd resp] -> Commands cmd resp) -> ([Command cmd resp] -> Commands cmd resp) -> ([Command cmd resp], [Command cmd resp]) -> (Commands cmd resp, Commands cmd resp) forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d) forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands (Int -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) forall a. Int -> [a] -> ([a], [a]) splitAt Int prefixLength [Command cmd resp] cmds) ParallelCommands cmd resp -> Gen (ParallelCommands cmd resp) forall a. a -> Gen a forall (m :: * -> *) a. Monad m => a -> m a return (Commands cmd resp -> [Pair (Commands cmd resp)] -> ParallelCommands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands Commands cmd resp prefix (model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)] makeSuffixes (StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic advanceModel StateMachine model cmd m resp sm model Symbolic forall (r :: * -> *). model r initModel Commands cmd resp prefix) Commands cmd resp rest)) where makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)] makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)] makeSuffixes model Symbolic model0 = model Symbolic -> [Pair (Commands cmd resp)] -> [Command cmd resp] -> [Pair (Commands cmd resp)] go model Symbolic model0 [] ([Command cmd resp] -> [Pair (Commands cmd resp)]) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> [Pair (Commands cmd resp)] forall b c a. (b -> c) -> (a -> b) -> a -> c . Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands where go :: model Symbolic -> [Pair (Commands cmd resp)] -> [Command cmd resp] -> [Pair (Commands cmd resp)] go model Symbolic _ [Pair (Commands cmd resp)] acc [] = [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)] forall a. [a] -> [a] reverse [Pair (Commands cmd resp)] acc go model Symbolic model [Pair (Commands cmd resp)] acc [Command cmd resp] cmds = model Symbolic -> [Pair (Commands cmd resp)] -> [Command cmd resp] -> [Pair (Commands cmd resp)] go (StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic advanceModel StateMachine model cmd m resp sm model Symbolic model ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp] safe)) (Commands cmd resp -> Commands cmd resp -> Pair (Commands cmd resp) forall a. a -> a -> Pair a Pair ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp] safe1) ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp] safe2) Pair (Commands cmd resp) -> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)] forall a. a -> [a] -> [a] : [Pair (Commands cmd resp)] acc) [Command cmd resp] rest where ([Command cmd resp] safe, [Command cmd resp] rest) = StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). Foldable resp => StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) spanSafe StateMachine model cmd m resp sm model Symbolic model [] [Command cmd resp] cmds ([Command cmd resp] safe1, [Command cmd resp] safe2) = Int -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) forall a. Int -> [a] -> ([a], [a]) splitAt ([Command cmd resp] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [Command cmd resp] safe Int -> Int -> Int forall a. Integral a => a -> a -> a `div` Int 2) [Command cmd resp] safe -- Split the list of commands in two such that the first half is a -- list of commands for which the preconditions of all commands hold -- for permutation of the list, i.e. it is parallel safe. The other -- half is the remainder of the input list. spanSafe :: Rank2.Foldable resp => StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) spanSafe :: forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). Foldable resp => StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) spanSafe StateMachine model cmd m resp _ model Symbolic _ [Command cmd resp] safe [] = ([Command cmd resp] -> [Command cmd resp] forall a. [a] -> [a] reverse [Command cmd resp] safe, []) spanSafe StateMachine model cmd m resp sm model Symbolic model [Command cmd resp] safe (Command cmd resp cmd : [Command cmd resp] cmds) | [Command cmd resp] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [Command cmd resp] safe Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int 5 , StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> Bool forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). Foldable resp => StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> Bool parallelSafe StateMachine model cmd m resp sm model Symbolic model ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands (Command cmd resp cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp] forall a. a -> [a] -> [a] : [Command cmd resp] safe)) = StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). Foldable resp => StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) spanSafe StateMachine model cmd m resp sm model Symbolic model (Command cmd resp cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp] forall a. a -> [a] -> [a] : [Command cmd resp] safe) [Command cmd resp] cmds | Bool otherwise = ([Command cmd resp] -> [Command cmd resp] forall a. [a] -> [a] reverse [Command cmd resp] safe, Command cmd resp cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp] forall a. a -> [a] -> [a] : [Command cmd resp] cmds) -- Generate Parallel commands. The length of each suffix, indicates how many thread can -- concurrently execute the commands safely. generateNParallelCommands :: forall model cmd m resp. Rank2.Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp) generateNParallelCommands :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp) generateNParallelCommands sm :: StateMachine model cmd m resp sm@StateMachine { forall (r :: * -> *). model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel :: forall (r :: * -> *). model r initModel } Int np = if Int np Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int 0 then String -> Gen (NParallelCommands cmd resp) forall a. HasCallStack => String -> a error String "number of threads must be positive" else do Commands [Command cmd resp] cmds <- StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd resp) forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd resp) generateCommands StateMachine model cmd m resp sm Maybe Int forall a. Maybe a Nothing Int prefixLength <- (Int -> Gen Int) -> Gen Int forall a. (Int -> Gen a) -> Gen a sized (\Int k -> (Int, Int) -> Gen Int forall a. Random a => (a, a) -> Gen a choose (Int 0, Int k Int -> Int -> Int forall a. Integral a => a -> a -> a `div` Int 3)) let (Commands cmd resp prefix, Commands cmd resp rest) = ([Command cmd resp] -> Commands cmd resp) -> ([Command cmd resp] -> Commands cmd resp) -> ([Command cmd resp], [Command cmd resp]) -> (Commands cmd resp, Commands cmd resp) forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d) forall (p :: * -> * -> *) a b c d. Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d bimap [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands (Int -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) forall a. Int -> [a] -> ([a], [a]) splitAt Int prefixLength [Command cmd resp] cmds) NParallelCommands cmd resp -> Gen (NParallelCommands cmd resp) forall a. a -> Gen a forall (m :: * -> *) a. Monad m => a -> m a return (Commands cmd resp -> [[Commands cmd resp]] -> NParallelCommands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands Commands cmd resp prefix (model Symbolic -> Commands cmd resp -> [[Commands cmd resp]] makeSuffixes (StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic advanceModel StateMachine model cmd m resp sm model Symbolic forall (r :: * -> *). model r initModel Commands cmd resp prefix) Commands cmd resp rest)) where makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]] makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]] makeSuffixes model Symbolic model0 = model Symbolic -> [[Commands cmd resp]] -> [Command cmd resp] -> [[Commands cmd resp]] go model Symbolic model0 [] ([Command cmd resp] -> [[Commands cmd resp]]) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> [[Commands cmd resp]] forall b c a. (b -> c) -> (a -> b) -> a -> c . Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands where go :: model Symbolic -> [[Commands cmd resp]] -> [Command cmd resp] -> [[Commands cmd resp]] go :: model Symbolic -> [[Commands cmd resp]] -> [Command cmd resp] -> [[Commands cmd resp]] go model Symbolic _ [[Commands cmd resp]] acc [] = [[Commands cmd resp]] -> [[Commands cmd resp]] forall a. [a] -> [a] reverse [[Commands cmd resp]] acc go model Symbolic model [[Commands cmd resp]] acc [Command cmd resp] cmds = model Symbolic -> [[Commands cmd resp]] -> [Command cmd resp] -> [[Commands cmd resp]] go (StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic advanceModel StateMachine model cmd m resp sm model Symbolic model ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp] safe)) ([Commands cmd resp] safes [Commands cmd resp] -> [[Commands cmd resp]] -> [[Commands cmd resp]] forall a. a -> [a] -> [a] : [[Commands cmd resp]] acc) [Command cmd resp] rest where ([Command cmd resp] safe, [Command cmd resp] rest) = StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). Foldable resp => StateMachine model cmd m resp -> model Symbolic -> [Command cmd resp] -> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp]) spanSafe StateMachine model cmd m resp sm model Symbolic model [] [Command cmd resp] cmds safes :: [Commands cmd resp] safes = [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands ([Command cmd resp] -> Commands cmd resp) -> [[Command cmd resp]] -> [Commands cmd resp] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Int -> Int -> [Command cmd resp] -> [[Command cmd resp]] forall a. Int -> Int -> [a] -> [[a]] chunksOf Int np ([Command cmd resp] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [Command cmd resp] safe Int -> Int -> Int forall a. Integral a => a -> a -> a `div` Int np) [Command cmd resp] safe -- Split the list in n sublists, whose concat is the initial list. -- We try to keep the length of each sublist len. -- -- It is important that we miss no elements here or else executeCommands may fail, because -- of missing references. It is also important that the final list has the correct length -- n, or else there will be different number of threads than the user specified. chunksOf :: Int -> Int -> [a] -> [[a]] chunksOf :: forall a. Int -> Int -> [a] -> [[a]] chunksOf Int 1 Int _ [a] xs = [[a] xs] chunksOf Int n Int len [a] xs = [a] as [a] -> [[a]] -> [[a]] forall a. a -> [a] -> [a] : Int -> Int -> [a] -> [[a]] forall a. Int -> Int -> [a] -> [[a]] chunksOf (Int nInt -> Int -> Int forall a. Num a => a -> a -> a -Int 1) Int len [a] bs where ([a] as, [a] bs) = Int -> [a] -> ([a], [a]) forall a. Int -> [a] -> ([a], [a]) splitAt Int len [a] xs -- | A list of commands is parallel safe if the pre-conditions for all commands -- hold in all permutations of the list. parallelSafe :: Rank2.Foldable resp => StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> Bool parallelSafe :: forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *). Foldable resp => StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> Bool parallelSafe StateMachine { model Symbolic -> cmd Symbolic -> Logic precondition :: model Symbolic -> cmd Symbolic -> Logic precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> Logic precondition, forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock } model Symbolic model0 = ([Command cmd resp] -> Bool) -> [[Command cmd resp]] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all (model Symbolic -> [Command cmd resp] -> Bool preconditionsHold model Symbolic model0) ([[Command cmd resp]] -> Bool) -> (Commands cmd resp -> [[Command cmd resp]]) -> Commands cmd resp -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . [Command cmd resp] -> [[Command cmd resp]] forall a. [a] -> [[a]] permutations ([Command cmd resp] -> [[Command cmd resp]]) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> [[Command cmd resp]] forall b c a. (b -> c) -> (a -> b) -> a -> c . Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands where preconditionsHold :: model Symbolic -> [Command cmd resp] -> Bool preconditionsHold model Symbolic _ [] = Bool True preconditionsHold model Symbolic model (Command cmd Symbolic cmd resp Symbolic resp [Var] vars : [Command cmd resp] cmds) = Logic -> Bool boolean (model Symbolic -> cmd Symbolic -> Logic precondition model Symbolic model cmd Symbolic cmd) Bool -> Bool -> Bool && model Symbolic -> [Command cmd resp] -> Bool preconditionsHold (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition model Symbolic model cmd Symbolic cmd resp Symbolic resp) [Command cmd resp] cmds Bool -> Bool -> Bool && -- This makes sure that in all permutations the length of variables created is the same. -- By doing so, we try to avoid MockSemanticsMismatch errors. -- More https://github.com/advancedtelematic/quickcheck-state-machine/pull/348 [Var] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [Var] vars Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == [Var] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length (resp Symbolic -> [Var] forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var] getUsedVars (resp Symbolic -> [Var]) -> resp Symbolic -> [Var] forall a b. (a -> b) -> a -> b $ (resp Symbolic, Counter) -> resp Symbolic forall a b. (a, b) -> a fst ((resp Symbolic, Counter) -> resp Symbolic) -> (resp Symbolic, Counter) -> resp Symbolic forall a b. (a -> b) -> a -> b $ GenSym (resp Symbolic) -> Counter -> (resp Symbolic, Counter) forall a. GenSym a -> Counter -> (a, Counter) runGenSym (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock model Symbolic model cmd Symbolic cmd) Counter newCounter) -- | Apply the transition of some commands to a model. advanceModel :: StateMachine model cmd m resp -> model Symbolic -- ^ The model. -> Commands cmd resp -- ^ The commands. -> model Symbolic advanceModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic advanceModel StateMachine { forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition } model Symbolic model0 = model Symbolic -> [Command cmd resp] -> model Symbolic go model Symbolic model0 ([Command cmd resp] -> model Symbolic) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> model Symbolic forall b c a. (b -> c) -> (a -> b) -> a -> c . Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands where go :: model Symbolic -> [Command cmd resp] -> model Symbolic go model Symbolic model [] = model Symbolic model go model Symbolic model (Command cmd Symbolic cmd resp Symbolic resp [Var] _vars : [Command cmd resp] cmds) = model Symbolic -> [Command cmd resp] -> model Symbolic go (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition model Symbolic model cmd Symbolic cmd resp Symbolic resp) [Command cmd resp] cmds ------------------------------------------------------------------------ -- | Shrink a parallel program in a pre-condition and scope respecting -- way. shrinkParallelCommands :: forall cmd model m resp. Rank2.Traversable cmd => Rank2.Foldable resp => StateMachine model cmd m resp -> (ParallelCommands cmd resp -> [ParallelCommands cmd resp]) shrinkParallelCommands :: forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] shrinkParallelCommands StateMachine model cmd m resp sm (ParallelCommands Commands cmd resp prefix [Pair (Commands cmd resp)] suffixes) = (Shrunk (ParallelCommandsF Pair cmd resp) -> [ParallelCommandsF Pair cmd resp]) -> [Shrunk (ParallelCommandsF Pair cmd resp)] -> [ParallelCommandsF Pair cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap Shrunk (ParallelCommandsF Pair cmd resp) -> [ParallelCommandsF Pair cmd resp] go [ Bool -> ParallelCommandsF Pair cmd resp -> Shrunk (ParallelCommandsF Pair cmd resp) forall a. Bool -> a -> Shrunk a Shrunk Bool s (Commands cmd resp -> [Pair (Commands cmd resp)] -> ParallelCommandsF Pair cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands Commands cmd resp prefix' (((Commands cmd resp, Commands cmd resp) -> Pair (Commands cmd resp)) -> [(Commands cmd resp, Commands cmd resp)] -> [Pair (Commands cmd resp)] forall a b. (a -> b) -> [a] -> [b] map (Commands cmd resp, Commands cmd resp) -> Pair (Commands cmd resp) forall a. (a, a) -> Pair a toPair [(Commands cmd resp, Commands cmd resp)] suffixes')) | Shrunk Bool s (Commands cmd resp prefix', [(Commands cmd resp, Commands cmd resp)] suffixes') <- (Commands cmd resp -> [Shrunk (Commands cmd resp)]) -> ([(Commands cmd resp, Commands cmd resp)] -> [Shrunk [(Commands cmd resp, Commands cmd resp)]]) -> (Commands cmd resp, [(Commands cmd resp, Commands cmd resp)]) -> [Shrunk (Commands cmd resp, [(Commands cmd resp, Commands cmd resp)])] forall a b. (a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)] shrinkPairS Commands cmd resp -> [Shrunk (Commands cmd resp)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Shrunk (Commands cmd resp)] shrinkCommands' [(Commands cmd resp, Commands cmd resp)] -> [Shrunk [(Commands cmd resp, Commands cmd resp)]] shrinkSuffixes (Commands cmd resp prefix, (Pair (Commands cmd resp) -> (Commands cmd resp, Commands cmd resp)) -> [Pair (Commands cmd resp)] -> [(Commands cmd resp, Commands cmd resp)] forall a b. (a -> b) -> [a] -> [b] map Pair (Commands cmd resp) -> (Commands cmd resp, Commands cmd resp) forall a. Pair a -> (a, a) fromPair [Pair (Commands cmd resp)] suffixes) ] [ParallelCommandsF Pair cmd resp] -> [ParallelCommandsF Pair cmd resp] -> [ParallelCommandsF Pair cmd resp] forall a. [a] -> [a] -> [a] ++ [ParallelCommandsF Pair cmd resp] shrinkMoveSuffixToPrefix where go :: Shrunk (ParallelCommands cmd resp) -> [ParallelCommands cmd resp] go :: Shrunk (ParallelCommandsF Pair cmd resp) -> [ParallelCommandsF Pair cmd resp] go (Shrunk Bool shrunk ParallelCommandsF Pair cmd resp cmds) = StateMachine model cmd m resp -> ShouldShrink -> ParallelCommandsF Pair cmd resp -> [ParallelCommandsF Pair cmd resp] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] shrinkAndValidateParallel StateMachine model cmd m resp sm (if Bool shrunk then ShouldShrink DontShrink else ShouldShrink MustShrink) ParallelCommandsF Pair cmd resp cmds shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)] -> [Shrunk [(Commands cmd resp, Commands cmd resp)]] shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)] -> [Shrunk [(Commands cmd resp, Commands cmd resp)]] shrinkSuffixes = ((Commands cmd resp, Commands cmd resp) -> [Shrunk (Commands cmd resp, Commands cmd resp)]) -> [(Commands cmd resp, Commands cmd resp)] -> [Shrunk [(Commands cmd resp, Commands cmd resp)]] forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]] shrinkListS ((Commands cmd resp -> [Shrunk (Commands cmd resp)]) -> (Commands cmd resp, Commands cmd resp) -> [Shrunk (Commands cmd resp, Commands cmd resp)] forall a. (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)] shrinkPairS' Commands cmd resp -> [Shrunk (Commands cmd resp)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Shrunk (Commands cmd resp)] shrinkCommands') -- Moving a command from a suffix to the prefix preserves validity shrinkMoveSuffixToPrefix :: [ParallelCommands cmd resp] shrinkMoveSuffixToPrefix :: [ParallelCommandsF Pair cmd resp] shrinkMoveSuffixToPrefix = case [Pair (Commands cmd resp)] suffixes of [] -> [] (Pair (Commands cmd resp) suffix : [Pair (Commands cmd resp)] suffixes') -> [ Commands cmd resp -> [Pair (Commands cmd resp)] -> ParallelCommandsF Pair cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands (Commands cmd resp prefix Commands cmd resp -> Commands cmd resp -> Commands cmd resp forall a. Semigroup a => a -> a -> a <> [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp prefix']) (([Command cmd resp] -> Commands cmd resp) -> Pair [Command cmd resp] -> Pair (Commands cmd resp) forall a b. (a -> b) -> Pair a -> Pair b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands (([Command cmd resp], [Command cmd resp]) -> Pair [Command cmd resp] forall a. (a, a) -> Pair a toPair ([Command cmd resp], [Command cmd resp]) suffix') Pair (Commands cmd resp) -> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)] forall a. a -> [a] -> [a] : [Pair (Commands cmd resp)] suffixes') | (Command cmd resp prefix', ([Command cmd resp], [Command cmd resp]) suffix') <- ([Command cmd resp], [Command cmd resp]) -> [(Command cmd resp, ([Command cmd resp], [Command cmd resp]))] forall a. ([a], [a]) -> [(a, ([a], [a]))] pickOneReturnRest2 (Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands (Pair (Commands cmd resp) -> Commands cmd resp forall a. Pair a -> a proj1 Pair (Commands cmd resp) suffix), Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands (Pair (Commands cmd resp) -> Commands cmd resp forall a. Pair a -> a proj2 Pair (Commands cmd resp) suffix)) ] -- | Shrink a parallel program in a pre-condition and scope respecting -- way. shrinkNParallelCommands :: forall cmd model m resp. Rank2.Traversable cmd => Rank2.Foldable resp => StateMachine model cmd m resp -> (NParallelCommands cmd resp -> [NParallelCommands cmd resp]) shrinkNParallelCommands :: forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] shrinkNParallelCommands StateMachine model cmd m resp sm (ParallelCommands Commands cmd resp prefix [[Commands cmd resp]] suffixes) = (Shrunk (ParallelCommandsF [] cmd resp) -> [ParallelCommandsF [] cmd resp]) -> [Shrunk (ParallelCommandsF [] cmd resp)] -> [ParallelCommandsF [] cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap Shrunk (ParallelCommandsF [] cmd resp) -> [ParallelCommandsF [] cmd resp] go [ Bool -> ParallelCommandsF [] cmd resp -> Shrunk (ParallelCommandsF [] cmd resp) forall a. Bool -> a -> Shrunk a Shrunk Bool s (Commands cmd resp -> [[Commands cmd resp]] -> ParallelCommandsF [] cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands Commands cmd resp prefix' [[Commands cmd resp]] suffixes') | Shrunk Bool s (Commands cmd resp prefix', [[Commands cmd resp]] suffixes') <- (Commands cmd resp -> [Shrunk (Commands cmd resp)]) -> ([[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]]) -> (Commands cmd resp, [[Commands cmd resp]]) -> [Shrunk (Commands cmd resp, [[Commands cmd resp]])] forall a b. (a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)] shrinkPairS Commands cmd resp -> [Shrunk (Commands cmd resp)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Shrunk (Commands cmd resp)] shrinkCommands' [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]] shrinkSuffixes (Commands cmd resp prefix, [[Commands cmd resp]] suffixes) ] [ParallelCommandsF [] cmd resp] -> [ParallelCommandsF [] cmd resp] -> [ParallelCommandsF [] cmd resp] forall a. [a] -> [a] -> [a] ++ [ParallelCommandsF [] cmd resp] shrinkMoveSuffixToPrefix where go :: Shrunk (NParallelCommands cmd resp) -> [NParallelCommands cmd resp] go :: Shrunk (ParallelCommandsF [] cmd resp) -> [ParallelCommandsF [] cmd resp] go (Shrunk Bool shrunk ParallelCommandsF [] cmd resp cmds) = StateMachine model cmd m resp -> ShouldShrink -> ParallelCommandsF [] cmd resp -> [ParallelCommandsF [] cmd resp] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] shrinkAndValidateNParallel StateMachine model cmd m resp sm (if Bool shrunk then ShouldShrink DontShrink else ShouldShrink MustShrink) ParallelCommandsF [] cmd resp cmds shrinkSuffixes :: [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]] shrinkSuffixes :: [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]] shrinkSuffixes = ([Commands cmd resp] -> [Shrunk [Commands cmd resp]]) -> [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]] forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]] shrinkListS ((Commands cmd resp -> [Shrunk (Commands cmd resp)]) -> [Commands cmd resp] -> [Shrunk [Commands cmd resp]] forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]] shrinkListS'' Commands cmd resp -> [Shrunk (Commands cmd resp)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Shrunk (Commands cmd resp)] shrinkCommands') -- Moving a command from a suffix to the prefix preserves validity shrinkMoveSuffixToPrefix :: [NParallelCommands cmd resp] shrinkMoveSuffixToPrefix :: [ParallelCommandsF [] cmd resp] shrinkMoveSuffixToPrefix = case [[Commands cmd resp]] suffixes of [] -> [] ([Commands cmd resp] suffix : [[Commands cmd resp]] suffixes') -> [ Commands cmd resp -> [[Commands cmd resp]] -> ParallelCommandsF [] cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands (Commands cmd resp prefix Commands cmd resp -> Commands cmd resp -> Commands cmd resp forall a. Semigroup a => a -> a -> a <> [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp prefix']) (([Command cmd resp] -> Commands cmd resp) -> [[Command cmd resp]] -> [Commands cmd resp] forall a b. (a -> b) -> [a] -> [b] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [[Command cmd resp]] suffix' [Commands cmd resp] -> [[Commands cmd resp]] -> [[Commands cmd resp]] forall a. a -> [a] -> [a] : [[Commands cmd resp]] suffixes') | (Command cmd resp prefix', [[Command cmd resp]] suffix') <- [[Command cmd resp]] -> [(Command cmd resp, [[Command cmd resp]])] forall a. [[a]] -> [(a, [[a]])] pickOneReturnRestL (Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands (Commands cmd resp -> [Command cmd resp]) -> [Commands cmd resp] -> [[Command cmd resp]] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [Commands cmd resp] suffix) ] -- | Shrinks Commands in a way that it has strictly less number of commands. shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)] shrinkCommands' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Shrunk (Commands cmd resp)] shrinkCommands' = (Shrunk [Command cmd resp] -> Shrunk (Commands cmd resp)) -> [Shrunk [Command cmd resp]] -> [Shrunk (Commands cmd resp)] forall a b. (a -> b) -> [a] -> [b] map (([Command cmd resp] -> Commands cmd resp) -> Shrunk [Command cmd resp] -> Shrunk (Commands cmd resp) forall a b. (a -> b) -> Shrunk a -> Shrunk b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands) ([Shrunk [Command cmd resp]] -> [Shrunk (Commands cmd resp)]) -> (Commands cmd resp -> [Shrunk [Command cmd resp]]) -> Commands cmd resp -> [Shrunk (Commands cmd resp)] forall b c a. (b -> c) -> (a -> b) -> a -> c . [Command cmd resp] -> [Shrunk [Command cmd resp]] forall a. [a] -> [Shrunk [a]] shrinkListS' ([Command cmd resp] -> [Shrunk [Command cmd resp]]) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> [Shrunk [Command cmd resp]] forall b c a. (b -> c) -> (a -> b) -> a -> c . Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands shrinkAndValidateParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] shrinkAndValidateParallel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ParallelCommands cmd resp -> [ParallelCommands cmd resp] shrinkAndValidateParallel sm :: StateMachine model cmd m resp sm@StateMachine { forall (r :: * -> *). model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel :: forall (r :: * -> *). model r initModel } = \ShouldShrink shouldShrink (ParallelCommands Commands cmd resp prefix [Pair (Commands cmd resp)] suffixes) -> let env :: ValidateEnv model env = model Symbolic -> ValidateEnv model forall (model :: (* -> *) -> *). model Symbolic -> ValidateEnv model initValidateEnv model Symbolic forall (r :: * -> *). model r initModel curryGo :: ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [ParallelCommands cmd resp] curryGo ShouldShrink shouldShrink' (ValidateEnv model env', Commands cmd resp prefix') = Commands cmd resp -> ValidateEnv model -> ShouldShrink -> [Pair (Commands cmd resp)] -> [ParallelCommands cmd resp] go Commands cmd resp prefix' ValidateEnv model env' ShouldShrink shouldShrink' [Pair (Commands cmd resp)] suffixes in case ShouldShrink shouldShrink of ShouldShrink DontShrink -> ((ValidateEnv model, Commands cmd resp) -> [ParallelCommands cmd resp]) -> [(ValidateEnv model, Commands cmd resp)] -> [ParallelCommands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [ParallelCommands cmd resp] curryGo ShouldShrink DontShrink) (StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink DontShrink ValidateEnv model env Commands cmd resp prefix) ShouldShrink MustShrink -> ((ValidateEnv model, Commands cmd resp) -> [ParallelCommands cmd resp]) -> [(ValidateEnv model, Commands cmd resp)] -> [ParallelCommands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [ParallelCommands cmd resp] curryGo ShouldShrink DontShrink) (StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink MustShrink ValidateEnv model env Commands cmd resp prefix) [ParallelCommands cmd resp] -> [ParallelCommands cmd resp] -> [ParallelCommands cmd resp] forall a. [a] -> [a] -> [a] ++ ((ValidateEnv model, Commands cmd resp) -> [ParallelCommands cmd resp]) -> [(ValidateEnv model, Commands cmd resp)] -> [ParallelCommands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [ParallelCommands cmd resp] curryGo ShouldShrink MustShrink) (StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink DontShrink ValidateEnv model env Commands cmd resp prefix) where go :: Commands cmd resp -- validated prefix -> ValidateEnv model -- environment after the prefix -> ShouldShrink -- should we /still/ shrink something? -> [Pair (Commands cmd resp)] -- suffixes to validate -> [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)] -- accumulated validated suffixes (in reverse order) -> ValidateEnv model -- environment after the validated suffixes -> ShouldShrink -- should we /still/ shrink something? -> [Pair (Commands cmd resp)] -- suffixes to validate -> [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 [] = [] -- Failed to shrink something go' [Pair (Commands cmd resp)] acc ValidateEnv model _ ShouldShrink DontShrink [] = [Commands cmd resp -> [Pair (Commands cmd resp)] -> ParallelCommands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands Commands cmd resp prefix' ([Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)] forall a. [a] -> [a] reverse [Pair (Commands cmd resp)] acc)] go' [Pair (Commands cmd resp)] acc ValidateEnv model env ShouldShrink shouldShrink (Pair Commands cmd resp l Commands cmd resp r : [Pair (Commands cmd resp)] suffixes) = do ((ShouldShrink shrinkL, ShouldShrink shrinkR), ShouldShrink shrinkRest) <- [((ShouldShrink, ShouldShrink), ShouldShrink)] shrinkOpts (ValidateEnv model envL, Commands cmd resp l') <- StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink shrinkL ValidateEnv model env Commands cmd resp l (ValidateEnv model envR, Commands cmd resp r') <- StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink shrinkR (ValidateEnv model env ValidateEnv model -> ValidateEnv model -> ValidateEnv model forall (model :: (* -> *) -> *). ValidateEnv model -> ValidateEnv model -> ValidateEnv model `withCounterFrom` ValidateEnv model envL) Commands cmd resp r [Pair (Commands cmd resp)] -> ValidateEnv model -> ShouldShrink -> [Pair (Commands cmd resp)] -> [ParallelCommands cmd resp] go' (Commands cmd resp -> Commands cmd resp -> Pair (Commands cmd resp) forall a. a -> a -> Pair a Pair Commands cmd resp l' Commands cmd resp r' Pair (Commands cmd resp) -> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)] forall a. a -> [a] -> [a] : [Pair (Commands cmd resp)] acc) (StateMachine model cmd m resp -> ValidateEnv model -> ValidateEnv model -> Commands cmd resp -> ValidateEnv model forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> ValidateEnv model -> ValidateEnv model -> Commands cmd resp -> ValidateEnv model combineEnv StateMachine model cmd m resp sm ValidateEnv model envL ValidateEnv model envR Commands cmd resp r') ShouldShrink shrinkRest [Pair (Commands cmd resp)] suffixes where shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)] shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)] shrinkOpts = case ShouldShrink shouldShrink of ShouldShrink DontShrink -> [ ((ShouldShrink DontShrink, ShouldShrink DontShrink), ShouldShrink DontShrink) ] ShouldShrink MustShrink -> [ ((ShouldShrink MustShrink, ShouldShrink DontShrink), ShouldShrink DontShrink) , ((ShouldShrink DontShrink, ShouldShrink MustShrink), ShouldShrink DontShrink) , ((ShouldShrink DontShrink, ShouldShrink DontShrink), ShouldShrink MustShrink) ] combineEnv :: StateMachine model cmd m resp -> ValidateEnv model -> ValidateEnv model -> Commands cmd resp -> ValidateEnv model combineEnv :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> ValidateEnv model -> ValidateEnv model -> Commands cmd resp -> ValidateEnv model combineEnv StateMachine model cmd m resp sm ValidateEnv model envL ValidateEnv model envR Commands cmd resp cmds = ValidateEnv { veModel :: model Symbolic veModel = StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic advanceModel StateMachine model cmd m resp sm (ValidateEnv model -> model Symbolic forall (model :: (* -> *) -> *). ValidateEnv model -> model Symbolic veModel ValidateEnv model envL) Commands cmd resp cmds , veScope :: Map Var Var veScope = Map Var Var -> Map Var Var -> Map Var Var forall k a. Ord k => Map k a -> Map k a -> Map k a Map.union (ValidateEnv model -> Map Var Var forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var veScope ValidateEnv model envL) (ValidateEnv model -> Map Var Var forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var veScope ValidateEnv model envR) , veCounter :: Counter veCounter = ValidateEnv model -> Counter forall (model :: (* -> *) -> *). ValidateEnv model -> Counter veCounter ValidateEnv model envR } withCounterFrom :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model withCounterFrom :: forall (model :: (* -> *) -> *). ValidateEnv model -> ValidateEnv model -> ValidateEnv model withCounterFrom ValidateEnv model e ValidateEnv model e' = ValidateEnv model e { veCounter = veCounter e' } shrinkAndValidateNParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] shrinkAndValidateNParallel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> NParallelCommands cmd resp -> [NParallelCommands cmd resp] shrinkAndValidateNParallel StateMachine model cmd m resp sm = \ShouldShrink shouldShrink (ParallelCommands Commands cmd resp prefix [[Commands cmd resp]] suffixes) -> let env :: ValidateEnv model env = model Symbolic -> ValidateEnv model forall (model :: (* -> *) -> *). model Symbolic -> ValidateEnv model initValidateEnv (model Symbolic -> ValidateEnv model) -> model Symbolic -> ValidateEnv model forall a b. (a -> b) -> a -> b $ StateMachine model cmd m resp -> forall (r :: * -> *). model r forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel StateMachine model cmd m resp sm curryGo :: ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [NParallelCommands cmd resp] curryGo ShouldShrink shouldShrink' (ValidateEnv model env', Commands cmd resp prefix') = Commands cmd resp -> ValidateEnv model -> ShouldShrink -> [[Commands cmd resp]] -> [NParallelCommands cmd resp] go Commands cmd resp prefix' ValidateEnv model env' ShouldShrink shouldShrink' [[Commands cmd resp]] suffixes in case ShouldShrink shouldShrink of ShouldShrink DontShrink -> ((ValidateEnv model, Commands cmd resp) -> [NParallelCommands cmd resp]) -> [(ValidateEnv model, Commands cmd resp)] -> [NParallelCommands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [NParallelCommands cmd resp] curryGo ShouldShrink DontShrink) (StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink DontShrink ValidateEnv model env Commands cmd resp prefix) ShouldShrink MustShrink -> ((ValidateEnv model, Commands cmd resp) -> [NParallelCommands cmd resp]) -> [(ValidateEnv model, Commands cmd resp)] -> [NParallelCommands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [NParallelCommands cmd resp] curryGo ShouldShrink DontShrink) (StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink MustShrink ValidateEnv model env Commands cmd resp prefix) [NParallelCommands cmd resp] -> [NParallelCommands cmd resp] -> [NParallelCommands cmd resp] forall a. [a] -> [a] -> [a] ++ ((ValidateEnv model, Commands cmd resp) -> [NParallelCommands cmd resp]) -> [(ValidateEnv model, Commands cmd resp)] -> [NParallelCommands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap (ShouldShrink -> (ValidateEnv model, Commands cmd resp) -> [NParallelCommands cmd resp] curryGo ShouldShrink MustShrink) (StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink DontShrink ValidateEnv model env Commands cmd resp prefix) where go :: Commands cmd resp -- validated prefix -> ValidateEnv model -- environment after the prefix -> ShouldShrink -- should we /still/ shrink something? -> [[Commands cmd resp]] -- suffixes to validate -> [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]] -- accumulated validated suffixes (in reverse order) -> ValidateEnv model -- environment after the validated suffixes -> ShouldShrink -- should we /still/ shrink something? -> [[Commands cmd resp]] -- suffixes to validate -> [NParallelCommands cmd resp] go' :: [[Commands cmd resp]] -> ValidateEnv model -> ShouldShrink -> [[Commands cmd resp]] -> [NParallelCommands cmd resp] go' [[Commands cmd resp]] _ ValidateEnv model _ ShouldShrink MustShrink [] = [] -- Failed to shrink something go' [[Commands cmd resp]] acc ValidateEnv model _ ShouldShrink DontShrink [] = [Commands cmd resp -> [[Commands cmd resp]] -> NParallelCommands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp ParallelCommands Commands cmd resp prefix' ([[Commands cmd resp]] -> [[Commands cmd resp]] forall a. [a] -> [a] reverse [[Commands cmd resp]] acc)] go' [[Commands cmd resp]] acc ValidateEnv model env ShouldShrink shouldShrink ([Commands cmd resp] suffix : [[Commands cmd resp]] suffixes) = do ([(ShouldShrink, Commands cmd resp)] suffixWithShrinks, ShouldShrink shrinkRest) <- [Commands cmd resp] -> [([(ShouldShrink, Commands cmd resp)], ShouldShrink)] forall a. [a] -> [([(ShouldShrink, a)], ShouldShrink)] shrinkOpts [Commands cmd resp] suffix (ValidateEnv model envFinal, [Commands cmd resp] suffix') <- (Bool, [(ValidateEnv model, [Commands cmd resp])]) -> [(ValidateEnv model, [Commands cmd resp])] forall a b. (a, b) -> b snd ((Bool, [(ValidateEnv model, [Commands cmd resp])]) -> [(ValidateEnv model, [Commands cmd resp])]) -> (Bool, [(ValidateEnv model, [Commands cmd resp])]) -> [(ValidateEnv model, [Commands cmd resp])] forall a b. (a -> b) -> a -> b $ ((Bool, [(ValidateEnv model, [Commands cmd resp])]) -> (ShouldShrink, Commands cmd resp) -> (Bool, [(ValidateEnv model, [Commands cmd resp])])) -> (Bool, [(ValidateEnv model, [Commands cmd resp])]) -> [(ShouldShrink, Commands cmd resp)] -> (Bool, [(ValidateEnv model, [Commands cmd resp])]) forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl (Bool, [(ValidateEnv model, [Commands cmd resp])]) -> (ShouldShrink, Commands cmd resp) -> (Bool, [(ValidateEnv model, [Commands cmd resp])]) f (Bool True, [(ValidateEnv model env,[])]) [(ShouldShrink, Commands cmd resp)] suffixWithShrinks [[Commands cmd resp]] -> ValidateEnv model -> ShouldShrink -> [[Commands cmd resp]] -> [NParallelCommands cmd resp] go' ([Commands cmd resp] -> [Commands cmd resp] forall a. [a] -> [a] reverse [Commands cmd resp] suffix' [Commands cmd resp] -> [[Commands cmd resp]] -> [[Commands cmd resp]] forall a. a -> [a] -> [a] : [[Commands cmd resp]] acc) ValidateEnv model envFinal ShouldShrink shrinkRest [[Commands cmd resp]] suffixes where f :: (Bool, [(ValidateEnv model, [Commands cmd resp])]) -> (ShouldShrink, Commands cmd resp) -> (Bool, [(ValidateEnv model, [Commands cmd resp])]) f :: (Bool, [(ValidateEnv model, [Commands cmd resp])]) -> (ShouldShrink, Commands cmd resp) -> (Bool, [(ValidateEnv model, [Commands cmd resp])]) f (Bool firstCall, [(ValidateEnv model, [Commands cmd resp])] acc') (ShouldShrink shrink, Commands cmd resp cmds) = (Bool False, [(ValidateEnv model, [Commands cmd resp])] acc'') where acc'' :: [(ValidateEnv model, [Commands cmd resp])] acc'' = do (ValidateEnv model envPrev, [Commands cmd resp] cmdsPrev) <- [(ValidateEnv model, [Commands cmd resp])] acc' let envUsed :: ValidateEnv model envUsed = if Bool firstCall then ValidateEnv model env else ValidateEnv model env ValidateEnv model -> ValidateEnv model -> ValidateEnv model forall (model :: (* -> *) -> *). ValidateEnv model -> ValidateEnv model -> ValidateEnv model `withCounterFrom` ValidateEnv model envPrev (ValidateEnv model env', Commands cmd resp cmd') <- StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate StateMachine model cmd m resp sm ShouldShrink shrink ValidateEnv model envUsed Commands cmd resp cmds let env'' :: ValidateEnv model env'' = if Bool firstCall then ValidateEnv model env' else StateMachine model cmd m resp -> ValidateEnv model -> ValidateEnv model -> Commands cmd resp -> ValidateEnv model forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> ValidateEnv model -> ValidateEnv model -> Commands cmd resp -> ValidateEnv model combineEnv StateMachine model cmd m resp sm ValidateEnv model envPrev ValidateEnv model env' Commands cmd resp cmd' (ValidateEnv model, [Commands cmd resp]) -> [(ValidateEnv model, [Commands cmd resp])] forall a. a -> [a] forall (m :: * -> *) a. Monad m => a -> m a return (ValidateEnv model env'', Commands cmd resp cmd' Commands cmd resp -> [Commands cmd resp] -> [Commands cmd resp] forall a. a -> [a] -> [a] : [Commands cmd resp] cmdsPrev) shrinkOpts :: [a] -> [([(ShouldShrink, a)], ShouldShrink)] shrinkOpts :: forall a. [a] -> [([(ShouldShrink, a)], ShouldShrink)] shrinkOpts [a] ls = let len :: Int len = [a] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [a] ls dontShrink :: [ShouldShrink] dontShrink = Int -> ShouldShrink -> [ShouldShrink] forall a. Int -> a -> [a] replicate Int len ShouldShrink DontShrink shrinks :: [[ShouldShrink]] shrinks = if Int len Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int 0 then String -> [[ShouldShrink]] forall a. HasCallStack => String -> a error String "Invariant violation! A suffix should never be an empty list" else ((Int -> [ShouldShrink]) -> [Int] -> [[ShouldShrink]]) -> [Int] -> (Int -> [ShouldShrink]) -> [[ShouldShrink]] forall a b c. (a -> b -> c) -> b -> a -> c flip (Int -> [ShouldShrink]) -> [Int] -> [[ShouldShrink]] forall a b. (a -> b) -> [a] -> [b] map [Int 1..Int len] ((Int -> [ShouldShrink]) -> [[ShouldShrink]]) -> (Int -> [ShouldShrink]) -> [[ShouldShrink]] forall a b. (a -> b) -> a -> b $ \Int n -> Int -> ShouldShrink -> [ShouldShrink] forall a. Int -> a -> [a] replicate (Int n Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1) ShouldShrink DontShrink [ShouldShrink] -> [ShouldShrink] -> [ShouldShrink] forall a. [a] -> [a] -> [a] ++ [ShouldShrink MustShrink] [ShouldShrink] -> [ShouldShrink] -> [ShouldShrink] forall a. [a] -> [a] -> [a] ++ Int -> ShouldShrink -> [ShouldShrink] forall a. Int -> a -> [a] replicate (Int len Int -> Int -> Int forall a. Num a => a -> a -> a - Int n) ShouldShrink DontShrink in case ShouldShrink shouldShrink of ShouldShrink DontShrink -> [([ShouldShrink] -> [a] -> [(ShouldShrink, a)] forall a b. [a] -> [b] -> [(a, b)] zip [ShouldShrink] dontShrink [a] ls, ShouldShrink DontShrink)] ShouldShrink MustShrink -> ([ShouldShrink] -> ([(ShouldShrink, a)], ShouldShrink)) -> [[ShouldShrink]] -> [([(ShouldShrink, a)], ShouldShrink)] forall a b. (a -> b) -> [a] -> [b] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (\[ShouldShrink] shrinkLs -> ([ShouldShrink] -> [a] -> [(ShouldShrink, a)] forall a b. [a] -> [b] -> [(a, b)] zip [ShouldShrink] shrinkLs [a] ls, ShouldShrink DontShrink)) [[ShouldShrink]] shrinks [([(ShouldShrink, a)], ShouldShrink)] -> [([(ShouldShrink, a)], ShouldShrink)] -> [([(ShouldShrink, a)], ShouldShrink)] forall a. [a] -> [a] -> [a] ++ [([ShouldShrink] -> [a] -> [(ShouldShrink, a)] forall a b. [a] -> [b] -> [(a, b)] zip [ShouldShrink] dontShrink [a] ls, ShouldShrink MustShrink)] ------------------------------------------------------------------------ runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) runParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) runParallelCommands StateMachine model cmd m resp sm ParallelCommands cmd resp cmds = do TChan (Pid, HistoryEvent cmd resp) hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp)) forall (m :: * -> *) a. MonadIO m => m (TChan a) newTChanIO ((History cmd resp hist, model Concrete model, Reason reason1, Reason reason2), ()) <- m ((History cmd resp, model Concrete, Reason, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason, Reason), ()) forall (m :: * -> *) a. Monad m => m a -> PropertyM m a run (m ((History cmd resp, model Concrete, Reason, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason, Reason), ())) -> m ((History cmd resp, model Concrete, Reason, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason, Reason), ()) forall a b. (a -> b) -> a -> b $ (((History cmd resp, model Concrete, Reason, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason, Reason), ()) forall a b. (a, b) -> a fst ((((History cmd resp, model Concrete, Reason, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason, Reason), ())) -> m (((History cmd resp, model Concrete, Reason, Reason), ()), ()) -> m ((History cmd resp, model Concrete, Reason, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> m () -> (() -> ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) -> m ()) -> (() -> m ((History cmd resp, model Concrete, Reason, Reason), ())) -> m (((History cmd resp, model Concrete, Reason, Reason), ()), ()) forall a b c. HasCallStack => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) forall (m :: * -> *) a b c. (MonadMask m, HasCallStack) => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) generalBracket (() -> m () forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure ()) (\() _ ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) ec -> case ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) ec of ExitCaseSuccess ((History cmd resp _, model Concrete model, Reason _, Reason _), () _) -> StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm model Concrete model ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) _ -> TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan m [(Pid, HistoryEvent cmd resp)] -> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m () forall a b. m a -> (a -> m b) -> m b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm (model Concrete -> m ()) -> ([(Pid, HistoryEvent cmd resp)] -> model Concrete) -> [(Pid, HistoryEvent cmd resp)] -> m () forall b c a. (b -> c) -> (a -> b) -> a -> c . StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp) -> [(Pid, HistoryEvent cmd resp)] -> model Concrete forall b c a. (b -> c) -> (a -> b) -> a -> c . [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History ) (\() _ -> (,()) ((History cmd resp, model Concrete, Reason, Reason) -> ((History cmd resp, model Concrete, Reason, Reason), ())) -> m (History cmd resp, model Concrete, Reason, Reason) -> m ((History cmd resp, model Concrete, Reason, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) executeParallelCommands StateMachine model cmd m resp sm ParallelCommands cmd resp cmds TChan (Pid, HistoryEvent cmd resp) hchan Bool True) (History cmd resp, model Concrete, Logic) -> PropertyM m (History cmd resp, model Concrete, Logic) forall a. a -> PropertyM m a forall (m :: * -> *) a. Monad m => a -> m a return (History cmd resp hist, model Concrete model, Reason -> Logic logicReason ([Reason] -> Reason combineReasons [Reason reason1, Reason reason2]) Logic -> Logic -> Logic .&& StateMachine model cmd m resp -> History cmd resp -> Logic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic linearise StateMachine model cmd m resp sm History cmd resp hist) runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO 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) => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) runParallelCommands' StateMachine model cmd m resp sm cmd Concrete -> resp Concrete complete ParallelCommands cmd resp cmds = do TChan (Pid, HistoryEvent cmd resp) hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp)) forall (m :: * -> *) a. MonadIO m => m (TChan a) newTChanIO ((History cmd resp hist, model Concrete model, Reason _reason1, Reason _reason2), ()) <- m ((History cmd resp, model Concrete, Reason, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason, Reason), ()) forall (m :: * -> *) a. Monad m => m a -> PropertyM m a run (m ((History cmd resp, model Concrete, Reason, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason, Reason), ())) -> m ((History cmd resp, model Concrete, Reason, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason, Reason), ()) forall a b. (a -> b) -> a -> b $ (((History cmd resp, model Concrete, Reason, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason, Reason), ()) forall a b. (a, b) -> a fst ((((History cmd resp, model Concrete, Reason, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason, Reason), ())) -> m (((History cmd resp, model Concrete, Reason, Reason), ()), ()) -> m ((History cmd resp, model Concrete, Reason, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> m () -> (() -> ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) -> m ()) -> (() -> m ((History cmd resp, model Concrete, Reason, Reason), ())) -> m (((History cmd resp, model Concrete, Reason, Reason), ()), ()) forall a b c. HasCallStack => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) forall (m :: * -> *) a b c. (MonadMask m, HasCallStack) => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) generalBracket (() -> m () forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure ()) (\() _ ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) ec -> case ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) ec of ExitCaseSuccess ((History cmd resp _, model Concrete model, Reason _, Reason _), () _) -> StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm model Concrete model ExitCase ((History cmd resp, model Concrete, Reason, Reason), ()) _ -> TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan m [(Pid, HistoryEvent cmd resp)] -> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m () forall a b. m a -> (a -> m b) -> m b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm (model Concrete -> m ()) -> ([(Pid, HistoryEvent cmd resp)] -> model Concrete) -> [(Pid, HistoryEvent cmd resp)] -> m () forall b c a. (b -> c) -> (a -> b) -> a -> c . StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp) -> [(Pid, HistoryEvent cmd resp)] -> model Concrete forall b c a. (b -> c) -> (a -> b) -> a -> c . [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History ) (\() _ -> (,()) ((History cmd resp, model Concrete, Reason, Reason) -> ((History cmd resp, model Concrete, Reason, Reason), ())) -> m (History cmd resp, model Concrete, Reason, Reason) -> m ((History cmd resp, model Concrete, Reason, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) executeParallelCommands StateMachine model cmd m resp sm ParallelCommands cmd resp cmds TChan (Pid, HistoryEvent cmd resp) hchan Bool True) let hist' :: History cmd resp hist' = (cmd Concrete -> resp Concrete) -> History cmd resp -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). (cmd Concrete -> resp Concrete) -> History cmd resp -> History cmd resp completeHistory cmd Concrete -> resp Concrete complete History cmd resp hist (History cmd resp, model Concrete, Logic) -> PropertyM m (History cmd resp, model Concrete, Logic) forall a. a -> PropertyM m a forall (m :: * -> *) a. Monad m => a -> m a return (History cmd resp hist', model Concrete model, StateMachine model cmd m resp -> History cmd resp -> Logic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic linearise StateMachine model cmd m resp sm History cmd resp hist') 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 -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) executeParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason) executeParallelCommands sm :: StateMachine model cmd m resp sm@StateMachine{ forall (r :: * -> *). model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel :: forall (r :: * -> *). model r initModel } (ParallelCommands Commands cmd resp prefix [Pair (Commands cmd resp)] suffixes) TChan (Pid, HistoryEvent cmd resp) hchan Bool stopOnError = do (Reason reason0, (Environment env0, model Symbolic _smodel, Counter _counter, model Concrete _cmodel)) <- StateT (Environment, model Symbolic, Counter, model Concrete) m Reason -> (Environment, model Symbolic, Counter, model Concrete) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason executeCommands StateMachine model cmd m resp sm TChan (Pid, HistoryEvent cmd resp) hchan (Int -> Pid Pid Int 0) Check CheckEverything Commands cmd resp prefix) (Environment emptyEnvironment, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel) if Reason reason0 Reason -> Reason -> Bool forall a. Eq a => a -> a -> Bool /= Reason Ok then do [(Pid, HistoryEvent cmd resp)] hist <- TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan let model :: model Concrete model = StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> History cmd resp -> model Concrete forall a b. (a -> b) -> a -> b $ [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist (History cmd resp, model Concrete, Reason, Reason) -> m (History cmd resp, model Concrete, Reason, Reason) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist, model Concrete model, Reason reason0, Reason reason0) else do (Reason reason1, Reason reason2, Environment _) <- (Reason, Reason, Environment) -> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment) go (Reason Ok, Reason Ok, Environment env0) [Pair (Commands cmd resp)] suffixes [(Pid, HistoryEvent cmd resp)] hist <- TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan let model :: model Concrete model = StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> History cmd resp -> model Concrete forall a b. (a -> b) -> a -> b $ [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist (History cmd resp, model Concrete, Reason, Reason) -> m (History cmd resp, model Concrete, Reason, Reason) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist, model Concrete model, Reason reason1, Reason reason2) where go :: (Reason, Reason, Environment) -> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment) go (Reason res1, Reason res2, Environment env) [] = (Reason, Reason, Environment) -> m (Reason, Reason, Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Reason res1, Reason res2, Environment env) go (Reason Ok, Reason Ok, Environment env) (Pair Commands cmd resp cmds1 Commands cmd resp cmds2 : [Pair (Commands cmd resp)] pairs) = do ((Reason reason1, (Environment env1, model Symbolic _, Counter _, model Concrete _)), (Reason reason2, (Environment env2, model Symbolic _, Counter _, model Concrete _))) <- m (Reason, (Environment, model Symbolic, Counter, model Concrete)) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) -> m ((Reason, (Environment, model Symbolic, Counter, model Concrete)), (Reason, (Environment, model Symbolic, Counter, model Concrete))) forall (m :: * -> *) a b. MonadUnliftIO m => m a -> m b -> m (a, b) concurrently -- XXX: Post-conditions not checked, so we can pass in initModel here... -- It would be better if we made executeCommands take a Maybe Environment -- instead of the Check... (StateT (Environment, model Symbolic, Counter, model Concrete) m Reason -> (Environment, model Symbolic, Counter, model Concrete) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason executeCommands StateMachine model cmd m resp sm TChan (Pid, HistoryEvent cmd resp) hchan (Int -> Pid Pid Int 1) Check CheckNothing Commands cmd resp cmds1) (Environment env, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel)) (StateT (Environment, model Symbolic, Counter, model Concrete) m Reason -> (Environment, model Symbolic, Counter, model Concrete) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason executeCommands StateMachine model cmd m resp sm TChan (Pid, HistoryEvent cmd resp) hchan (Int -> Pid Pid Int 2) Check CheckNothing Commands cmd resp cmds2) (Environment env, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel)) case (Reason -> Bool isOK (Reason -> Bool) -> Reason -> Bool forall a b. (a -> b) -> a -> b $ [Reason] -> Reason combineReasons [Reason reason1, Reason reason2], Bool stopOnError) of (Bool False, Bool True) -> (Reason, Reason, Environment) -> m (Reason, Reason, Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Reason reason1, Reason reason2, Environment env1 Environment -> Environment -> Environment forall a. Semigroup a => a -> a -> a <> Environment env2) (Bool, Bool) _ -> (Reason, Reason, Environment) -> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment) go ( Reason reason1 , Reason reason2 , Environment env1 Environment -> Environment -> Environment forall a. Semigroup a => a -> a -> a <> Environment env2 ) [Pair (Commands cmd resp)] pairs go (Reason Ok, ExceptionThrown String e, Environment env) (Pair Commands cmd resp cmds1 Commands cmd resp _cmds2 : [Pair (Commands cmd resp)] pairs) = do -- XXX: It's possible that pre-conditions fail at this point, because -- commands may depend on references that never got created in the crashed -- process. For example, consider: -- -- x <- Create -- ------------+---------- -- Write 1 x | Write 2 x -- y <- Create | -- ------------+---------- -- Write 3 x | Write 4 y -- | Read x -- -- If the @Write 1 x@ fails, @y@ will never be created and the -- pre-condition for @Write 4 y@ will fail. This also means that @Read x@ -- will never get executed, and so there could be a bug in @Write@ that -- never gets discovered. Not sure if we can do something better here? -- (Reason reason1, (Environment env1, model Symbolic _, Counter _, model Concrete _)) <- StateT (Environment, model Symbolic, Counter, model Concrete) m Reason -> (Environment, model Symbolic, Counter, model Concrete) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason executeCommands StateMachine model cmd m resp sm TChan (Pid, HistoryEvent cmd resp) hchan (Int -> Pid Pid Int 1) Check CheckPrecondition Commands cmd resp cmds1) (Environment env, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel) (Reason, Reason, Environment) -> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment) go ( Reason reason1 , String -> Reason ExceptionThrown String e , Environment env1 ) [Pair (Commands cmd resp)] pairs go (ExceptionThrown String e, Reason Ok, Environment env) (Pair Commands cmd resp _cmds1 Commands cmd resp cmds2 : [Pair (Commands cmd resp)] pairs) = do (Reason reason2, (Environment env2, model Symbolic _, Counter _, model Concrete _)) <- StateT (Environment, model Symbolic, Counter, model Concrete) m Reason -> (Environment, model Symbolic, Counter, model Concrete) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason executeCommands StateMachine model cmd m resp sm TChan (Pid, HistoryEvent cmd resp) hchan (Int -> Pid Pid Int 2) Check CheckPrecondition Commands cmd resp cmds2) (Environment env, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel) (Reason, Reason, Environment) -> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment) go ( String -> Reason ExceptionThrown String e , Reason reason2 , Environment env2 ) [Pair (Commands cmd resp)] pairs go out :: (Reason, Reason, Environment) out@(ExceptionThrown String _, ExceptionThrown String _, Environment _env) (Pair (Commands cmd resp) _ : [Pair (Commands cmd resp)] _) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Reason, Reason, Environment) out go out :: (Reason, Reason, Environment) out@(PreconditionFailed {}, ExceptionThrown String _, Environment _env) (Pair (Commands cmd resp) _ : [Pair (Commands cmd resp)] _) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Reason, Reason, Environment) out go out :: (Reason, Reason, Environment) out@(ExceptionThrown String _, PreconditionFailed {}, Environment _env) (Pair (Commands cmd resp) _ : [Pair (Commands cmd resp)] _) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Reason, Reason, Environment) out go (Reason res1, Reason res2, Environment _env) (Pair Commands cmd resp _cmds1 Commands cmd resp _cmds2 : [Pair (Commands cmd resp)] _pairs) = String -> m (Reason, Reason, Environment) forall a. HasCallStack => String -> a error (String "executeParallelCommands, unexpected result: " String -> String -> String forall a. [a] -> [a] -> [a] ++ (Reason, Reason) -> String forall a. Show a => a -> String show (Reason res1, Reason res2)) logicReason :: Reason -> Logic logicReason :: Reason -> Logic logicReason Reason Ok = Logic Top logicReason Reason r = String -> Logic -> Logic Annotate (Reason -> String forall a. Show a => a -> String show Reason r) Logic Bot 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 StateMachine model cmd m resp sm NParallelCommands cmd resp cmds = do TChan (Pid, HistoryEvent cmd resp) hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp)) forall (m :: * -> *) a. MonadIO m => m (TChan a) newTChanIO ((History cmd resp hist, model Concrete model, Reason reason), ()) <- m ((History cmd resp, model Concrete, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason), ()) forall (m :: * -> *) a. Monad m => m a -> PropertyM m a run (m ((History cmd resp, model Concrete, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason), ())) -> m ((History cmd resp, model Concrete, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason), ()) forall a b. (a -> b) -> a -> b $ (((History cmd resp, model Concrete, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason), ()) forall a b. (a, b) -> a fst ((((History cmd resp, model Concrete, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason), ())) -> m (((History cmd resp, model Concrete, Reason), ()), ()) -> m ((History cmd resp, model Concrete, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> m () -> (() -> ExitCase ((History cmd resp, model Concrete, Reason), ()) -> m ()) -> (() -> m ((History cmd resp, model Concrete, Reason), ())) -> m (((History cmd resp, model Concrete, Reason), ()), ()) forall a b c. HasCallStack => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) forall (m :: * -> *) a b c. (MonadMask m, HasCallStack) => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) generalBracket (() -> m () forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure ()) (\() _ ExitCase ((History cmd resp, model Concrete, Reason), ()) ec -> case ExitCase ((History cmd resp, model Concrete, Reason), ()) ec of ExitCaseSuccess ((History cmd resp _, model Concrete model, Reason _), () _) -> StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm model Concrete model ExitCase ((History cmd resp, model Concrete, Reason), ()) _ -> TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan m [(Pid, HistoryEvent cmd resp)] -> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m () forall a b. m a -> (a -> m b) -> m b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm (model Concrete -> m ()) -> ([(Pid, HistoryEvent cmd resp)] -> model Concrete) -> [(Pid, HistoryEvent cmd resp)] -> m () forall b c a. (b -> c) -> (a -> b) -> a -> c . StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp) -> [(Pid, HistoryEvent cmd resp)] -> model Concrete forall b c a. (b -> c) -> (a -> b) -> a -> c . [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History ) (\() _ -> (,()) ((History cmd resp, model Concrete, Reason) -> ((History cmd resp, model Concrete, Reason), ())) -> m (History cmd resp, model Concrete, Reason) -> m ((History cmd resp, model Concrete, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StateMachine model cmd m resp -> NParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason) forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Traversable cmd, Show (cmd Concrete), Foldable resp, Show (resp Concrete), MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason) executeNParallelCommands StateMachine model cmd m resp sm NParallelCommands cmd resp cmds TChan (Pid, HistoryEvent cmd resp) hchan Bool True) (History cmd resp, model Concrete, Logic) -> PropertyM m (History cmd resp, model Concrete, Logic) forall a. a -> PropertyM m a forall (m :: * -> *) a. Monad m => a -> m a return (History cmd resp hist, model Concrete model, Reason -> Logic logicReason Reason reason Logic -> Logic -> Logic .&& StateMachine model cmd m resp -> History cmd resp -> Logic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic linearise StateMachine model cmd m resp sm History cmd resp hist) runNParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> (cmd Concrete -> resp Concrete) -> 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 -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m (History cmd resp, model Concrete, Logic) runNParallelCommands' StateMachine model cmd m resp sm cmd Concrete -> resp Concrete complete NParallelCommands cmd resp cmds = do TChan (Pid, HistoryEvent cmd resp) hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp)) forall (m :: * -> *) a. MonadIO m => m (TChan a) newTChanIO ((History cmd resp hist, model Concrete model, Reason _reason), ()) <- m ((History cmd resp, model Concrete, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason), ()) forall (m :: * -> *) a. Monad m => m a -> PropertyM m a run (m ((History cmd resp, model Concrete, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason), ())) -> m ((History cmd resp, model Concrete, Reason), ()) -> PropertyM m ((History cmd resp, model Concrete, Reason), ()) forall a b. (a -> b) -> a -> b $ (((History cmd resp, model Concrete, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason), ()) forall a b. (a, b) -> a fst ((((History cmd resp, model Concrete, Reason), ()), ()) -> ((History cmd resp, model Concrete, Reason), ())) -> m (((History cmd resp, model Concrete, Reason), ()), ()) -> m ((History cmd resp, model Concrete, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> m () -> (() -> ExitCase ((History cmd resp, model Concrete, Reason), ()) -> m ()) -> (() -> m ((History cmd resp, model Concrete, Reason), ())) -> m (((History cmd resp, model Concrete, Reason), ()), ()) forall a b c. HasCallStack => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) forall (m :: * -> *) a b c. (MonadMask m, HasCallStack) => m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c) generalBracket (() -> m () forall a. a -> m a forall (f :: * -> *) a. Applicative f => a -> f a pure ()) (\() _ ExitCase ((History cmd resp, model Concrete, Reason), ()) ec -> case ExitCase ((History cmd resp, model Concrete, Reason), ()) ec of ExitCaseSuccess ((History cmd resp _, model Concrete model, Reason _), () _) -> StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm model Concrete model ExitCase ((History cmd resp, model Concrete, Reason), ()) _ -> TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan m [(Pid, HistoryEvent cmd resp)] -> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m () forall a b. m a -> (a -> m b) -> m b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= StateMachine model cmd m resp -> model Concrete -> m () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup StateMachine model cmd m resp sm (model Concrete -> m ()) -> ([(Pid, HistoryEvent cmd resp)] -> model Concrete) -> [(Pid, HistoryEvent cmd resp)] -> m () forall b c a. (b -> c) -> (a -> b) -> a -> c . StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp) -> [(Pid, HistoryEvent cmd resp)] -> model Concrete forall b c a. (b -> c) -> (a -> b) -> a -> c . [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History ) (\() _ -> (,()) ((History cmd resp, model Concrete, Reason) -> ((History cmd resp, model Concrete, Reason), ())) -> m (History cmd resp, model Concrete, Reason) -> m ((History cmd resp, model Concrete, Reason), ()) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StateMachine model cmd m resp -> NParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason) forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Traversable cmd, Show (cmd Concrete), Foldable resp, Show (resp Concrete), MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason) executeNParallelCommands StateMachine model cmd m resp sm NParallelCommands cmd resp cmds TChan (Pid, HistoryEvent cmd resp) hchan Bool True) let hist' :: History cmd resp hist' = (cmd Concrete -> resp Concrete) -> History cmd resp -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). (cmd Concrete -> resp Concrete) -> History cmd resp -> History cmd resp completeHistory cmd Concrete -> resp Concrete complete History cmd resp hist (History cmd resp, model Concrete, Logic) -> PropertyM m (History cmd resp, model Concrete, Logic) forall a. a -> PropertyM m a forall (m :: * -> *) a. Monad m => a -> m a return (History cmd resp hist, model Concrete model, StateMachine model cmd m resp -> History cmd resp -> Logic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic linearise StateMachine model cmd m resp sm History cmd resp hist') 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 -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason) executeNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Traversable cmd, Show (cmd Concrete), Foldable resp, Show (resp Concrete), MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason) executeNParallelCommands sm :: StateMachine model cmd m resp sm@StateMachine{ forall (r :: * -> *). model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel :: forall (r :: * -> *). model r initModel } (ParallelCommands Commands cmd resp prefix [[Commands cmd resp]] suffixes) TChan (Pid, HistoryEvent cmd resp) hchan Bool stopOnError = do (Reason reason0, (Environment env0, model Symbolic _smodel, Counter _counter, model Concrete _cmodel)) <- StateT (Environment, model Symbolic, Counter, model Concrete) m Reason -> (Environment, model Symbolic, Counter, model Concrete) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason executeCommands StateMachine model cmd m resp sm TChan (Pid, HistoryEvent cmd resp) hchan (Int -> Pid Pid Int 0) Check CheckEverything Commands cmd resp prefix) (Environment emptyEnvironment, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel) if Reason reason0 Reason -> Reason -> Bool forall a. Eq a => a -> a -> Bool /= Reason Ok then do [(Pid, HistoryEvent cmd resp)] hist <- TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan let model :: model Concrete model = StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> History cmd resp -> model Concrete forall a b. (a -> b) -> a -> b $ [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist (History cmd resp, model Concrete, Reason) -> m (History cmd resp, model Concrete, Reason) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist, model Concrete model, Reason reason0) else do (Map Int Reason errors, Environment _) <- (Map Int Reason, Environment) -> [[Commands cmd resp]] -> m (Map Int Reason, Environment) go (Map Int Reason forall k a. Map k a Map.empty, Environment env0) [[Commands cmd resp]] suffixes [(Pid, HistoryEvent cmd resp)] hist <- TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan let model :: model Concrete model = StateMachine model cmd m resp -> History cmd resp -> model Concrete forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> History cmd resp -> model Concrete mkModel StateMachine model cmd m resp sm (History cmd resp -> model Concrete) -> History cmd resp -> model Concrete forall a b. (a -> b) -> a -> b $ [(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist (History cmd resp, model Concrete, Reason) -> m (History cmd resp, model Concrete, Reason) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist, model Concrete model, [Reason] -> Reason combineReasons ([Reason] -> Reason) -> [Reason] -> Reason forall a b. (a -> b) -> a -> b $ Map Int Reason -> [Reason] forall k a. Map k a -> [a] Map.elems Map Int Reason errors) where go :: (Map Int Reason, Environment) -> [[Commands cmd resp]] -> m (Map Int Reason, Environment) go (Map Int Reason, Environment) res [] = (Map Int Reason, Environment) -> m (Map Int Reason, Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Map Int Reason, Environment) res go (Map Int Reason previousErrors, Environment env) ([Commands cmd resp] suffix : [[Commands cmd resp]] rest) = do Bool -> m () -> m () forall (f :: * -> *). Applicative f => Bool -> f () -> f () when ([Reason] -> Bool isInvalid ([Reason] -> Bool) -> [Reason] -> Bool forall a b. (a -> b) -> a -> b $ Map Int Reason -> [Reason] forall k a. Map k a -> [a] Map.elems Map Int Reason previousErrors) (m () -> m ()) -> m () -> m () forall a b. (a -> b) -> a -> b $ String -> m () forall a. HasCallStack => String -> a error (String "executeNParallelCommands, unexpected result: " String -> String -> String forall a. [a] -> [a] -> [a] ++ Map Int Reason -> String forall a. Show a => a -> String show Map Int Reason previousErrors) let noError :: Bool noError = Map Int Reason -> Bool forall k a. Map k a -> Bool Map.null Map Int Reason previousErrors check :: Check check = if Bool noError then Check CheckNothing else Check CheckPrecondition [(Maybe (Int, Reason), Environment)] res <- [(Int, Commands cmd resp)] -> ((Int, Commands cmd resp) -> m (Maybe (Int, Reason), Environment)) -> m [(Maybe (Int, Reason), Environment)] forall (m :: * -> *) (t :: * -> *) a b. (MonadUnliftIO m, Traversable t) => t a -> (a -> m b) -> m (t b) forConcurrently ([Int] -> [Commands cmd resp] -> [(Int, Commands cmd resp)] forall a b. [a] -> [b] -> [(a, b)] zip [Int 1..] [Commands cmd resp] suffix) (((Int, Commands cmd resp) -> m (Maybe (Int, Reason), Environment)) -> m [(Maybe (Int, Reason), Environment)]) -> ((Int, Commands cmd resp) -> m (Maybe (Int, Reason), Environment)) -> m [(Maybe (Int, Reason), Environment)] forall a b. (a -> b) -> a -> b $ \(Int i, Commands cmd resp cmds) -> case Int -> Map Int Reason -> Maybe Reason forall k a. Ord k => k -> Map k a -> Maybe a Map.lookup Int i Map Int Reason previousErrors of Maybe Reason Nothing -> do (Reason reason, (Environment env', model Symbolic _, Counter _, model Concrete _)) <- StateT (Environment, model Symbolic, Counter, model Concrete) m Reason -> (Environment, model Symbolic, Counter, model Concrete) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s) runStateT (StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason executeCommands StateMachine model cmd m resp sm TChan (Pid, HistoryEvent cmd resp) hchan (Int -> Pid Pid Int i) Check check Commands cmd resp cmds) (Environment env, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel) (Maybe (Int, Reason), Environment) -> m (Maybe (Int, Reason), Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (if Reason -> Bool isOK Reason reason then Maybe (Int, Reason) forall a. Maybe a Nothing else (Int, Reason) -> Maybe (Int, Reason) forall a. a -> Maybe a Just (Int i, Reason reason), Environment env') Just Reason _ -> (Maybe (Int, Reason), Environment) -> m (Maybe (Int, Reason), Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Maybe (Int, Reason) forall a. Maybe a Nothing, Environment env) let newErrors :: Map Int Reason newErrors = [(Int, Reason)] -> Map Int Reason forall k a. Ord k => [(k, a)] -> Map k a Map.fromList ([(Int, Reason)] -> Map Int Reason) -> [(Int, Reason)] -> Map Int Reason forall a b. (a -> b) -> a -> b $ ((Maybe (Int, Reason), Environment) -> Maybe (Int, Reason)) -> [(Maybe (Int, Reason), Environment)] -> [(Int, Reason)] forall a b. (a -> Maybe b) -> [a] -> [b] mapMaybe (Maybe (Int, Reason), Environment) -> Maybe (Int, Reason) forall a b. (a, b) -> a fst [(Maybe (Int, Reason), Environment)] res errors :: Map Int Reason errors = Map Int Reason -> Map Int Reason -> Map Int Reason forall k a. Ord k => Map k a -> Map k a -> Map k a Map.union Map Int Reason previousErrors Map Int Reason newErrors newEnv :: Environment newEnv = [Environment] -> Environment forall a. Monoid a => [a] -> a mconcat ([Environment] -> Environment) -> [Environment] -> Environment forall a b. (a -> b) -> a -> b $ (Maybe (Int, Reason), Environment) -> Environment forall a b. (a, b) -> b snd ((Maybe (Int, Reason), Environment) -> Environment) -> [(Maybe (Int, Reason), Environment)] -> [Environment] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [(Maybe (Int, Reason), Environment)] res case (Bool stopOnError, Map Int Reason -> Bool forall k a. Map k a -> Bool Map.null Map Int Reason errors) of (Bool True, Bool False) -> (Map Int Reason, Environment) -> m (Map Int Reason, Environment) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (Map Int Reason errors, Environment newEnv) (Bool, Bool) _ -> (Map Int Reason, Environment) -> [[Commands cmd resp]] -> m (Map Int Reason, Environment) go (Map Int Reason errors, Environment newEnv) [[Commands cmd resp]] rest combineReasons :: [Reason] -> Reason combineReasons :: [Reason] -> Reason combineReasons [Reason] ls = Reason -> Maybe Reason -> Reason forall a. a -> Maybe a -> a fromMaybe Reason Ok ((Reason -> Bool) -> [Reason] -> Maybe Reason forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a find (Reason -> Reason -> Bool forall a. Eq a => a -> a -> Bool /= Reason Ok) [Reason] ls) isInvalid :: [Reason] -> Bool isInvalid :: [Reason] -> Bool isInvalid [Reason] ls = (Reason -> Bool) -> [Reason] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool any Reason -> Bool isPreconditionFailed [Reason] ls Bool -> Bool -> Bool && (Reason -> Bool) -> [Reason] -> Bool forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool all Reason -> Bool notException [Reason] ls where notException :: Reason -> Bool notException (ExceptionThrown String _) = Bool False notException Reason _ = Bool True isPreconditionFailed :: Reason -> Bool isPreconditionFailed :: Reason -> Bool isPreconditionFailed PreconditionFailed {} = Bool True isPreconditionFailed Reason _ = Bool False ------------------------------------------------------------------------ -- | Try to linearise a history of a parallel program execution using a -- sequential model. See the *Linearizability: a correctness condition for -- concurrent objects* paper linked to from the README for more info. linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic linearise :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic linearise StateMachine { forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition, model Concrete -> cmd Concrete -> resp Concrete -> Logic postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic postcondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> cmd Concrete -> resp Concrete -> Logic postcondition, forall (r :: * -> *). model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel :: forall (r :: * -> *). model r initModel } = [(Pid, HistoryEvent cmd resp)] -> Logic go ([(Pid, HistoryEvent cmd resp)] -> Logic) -> (History cmd resp -> [(Pid, HistoryEvent cmd resp)]) -> History cmd resp -> Logic forall b c a. (b -> c) -> (a -> b) -> a -> c . History cmd resp -> [(Pid, HistoryEvent cmd resp)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History cmd resp -> History' cmd resp unHistory where go :: [(Pid, HistoryEvent cmd resp)] -> Logic go :: [(Pid, HistoryEvent cmd resp)] -> Logic go [] = Logic Top go [(Pid, HistoryEvent cmd resp)] es = [Tree (Operation cmd resp)] -> (Tree (Operation cmd resp) -> Logic) -> Logic forall a. Show a => [a] -> (a -> Logic) -> Logic exists ([(Pid, HistoryEvent cmd resp)] -> [Tree (Operation cmd resp)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> Forest (Operation cmd resp) interleavings [(Pid, HistoryEvent cmd resp)] es) (model Concrete -> Tree (Operation cmd resp) -> Logic step model Concrete forall (r :: * -> *). model r initModel) step :: model Concrete -> Tree (Operation cmd resp) -> Logic step :: model Concrete -> Tree (Operation cmd resp) -> Logic step model Concrete _model (Node (Crash cmd Concrete _cmd String _err Pid _pid) [Tree (Operation cmd resp)] _roses) = String -> Logic forall a. HasCallStack => String -> a error String "Not implemented yet, see issue #162 for more details." step model Concrete model (Node (Operation cmd Concrete cmd resp Concrete resp Pid _) [Tree (Operation cmd resp)] roses) = model Concrete -> cmd Concrete -> resp Concrete -> Logic postcondition model Concrete model cmd Concrete cmd resp Concrete resp Logic -> Logic -> Logic .&& [Tree (Operation cmd resp)] -> (Tree (Operation cmd resp) -> Logic) -> Logic forall a. Show a => [a] -> (a -> Logic) -> Logic exists' [Tree (Operation cmd resp)] roses (model Concrete -> Tree (Operation cmd resp) -> Logic step (model Concrete -> cmd Concrete -> resp Concrete -> model Concrete forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition model Concrete model cmd Concrete cmd resp Concrete resp)) exists' :: Show a => [a] -> (a -> Logic) -> Logic exists' :: forall a. Show a => [a] -> (a -> Logic) -> Logic exists' [] a -> Logic _ = Logic Top exists' [a] xs a -> Logic p = [a] -> (a -> Logic) -> Logic forall a. Show a => [a] -> (a -> Logic) -> Logic exists [a] xs a -> Logic p ------------------------------------------------------------------------ -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyParallelCommandsWithOpts :: (MonadIO m, Rank2.Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runParallelCommands'. -> PropertyM m () prettyParallelCommandsWithOpts :: forall (m :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (model :: (* -> *) -> *). (MonadIO m, Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m () prettyParallelCommandsWithOpts ParallelCommands cmd resp cmds Maybe GraphOptions mGraphOptions (History cmd resp h, model Concrete _, Logic l) = do History cmd resp -> Value -> IO () printCounterexample History cmd resp h (Logic -> Value logic Logic l) IO () -> Property -> PropertyM m () forall (m :: * -> *). Monad m => IO () -> Property -> PropertyM m () `whenFailM` Bool -> Property forall prop. Testable prop => prop -> Property property (Logic -> Bool boolean Logic l) where printCounterexample :: History cmd resp -> Value -> IO () printCounterexample History cmd resp hist' (VFalse Counterexample ce) = do Doc AnsiStyle -> IO () PP.putDoc (Doc AnsiStyle -> IO ()) -> Doc AnsiStyle -> IO () forall a b. (a -> b) -> a -> b $ [Doc AnsiStyle] -> Doc AnsiStyle forall a. Monoid a => [a] -> a mconcat [ Doc AnsiStyle forall ann. Doc ann PP.line , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (Doc Any -> String forall a. Show a => a -> String show (Doc Any -> String) -> Doc Any -> String forall a b. (a -> b) -> a -> b $ ParallelCommands cmd resp -> History cmd resp -> Doc Any forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) ann. (Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc ann toBoxDrawings ParallelCommands cmd resp cmds History cmd resp hist') , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (Counterexample -> String forall a. Show a => a -> String show (Counterexample -> String) -> Counterexample -> String forall a b. (a -> b) -> a -> b $ Counterexample -> Counterexample simplify Counterexample ce) , Doc AnsiStyle forall ann. Doc ann PP.line ] case Maybe GraphOptions mGraphOptions of Maybe GraphOptions Nothing -> () -> IO () forall a. a -> IO a forall (m :: * -> *) a. Monad m => a -> m a return () Just GraphOptions gOptions -> ParallelCommands cmd resp -> GraphOptions -> History cmd resp -> IO () forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (t :: * -> *). (Foldable t, Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommandsF t cmd resp -> GraphOptions -> History cmd resp -> IO () createAndPrintDot ParallelCommands cmd resp cmds GraphOptions gOptions History cmd resp hist' printCounterexample History cmd resp _hist Value _ = String -> IO () forall a. HasCallStack => String -> a error String "prettyParallelCommands: impossible, because `boolean l` was False." simplify :: Counterexample -> Counterexample simplify :: Counterexample -> Counterexample simplify (Fst ce :: Counterexample ce@(AnnotateC String _ Counterexample BotC)) = Counterexample ce simplify (Snd Counterexample ce) = Counterexample -> Counterexample simplify Counterexample ce simplify (ExistsC [] []) = Counterexample BotC simplify (ExistsC [a] _ [Fst Counterexample ce]) = Counterexample ce simplify (ExistsC [a] x (Fst Counterexample ce : [Counterexample] ces)) = Counterexample ce Counterexample -> Counterexample -> Counterexample `EitherC` Counterexample -> Counterexample simplify ([a] -> [Counterexample] -> Counterexample forall a. Show a => [a] -> [Counterexample] -> Counterexample ExistsC [a] x [Counterexample] ces) simplify (ExistsC [a] _ (Snd Counterexample ce : [Counterexample] _)) = Counterexample -> Counterexample simplify Counterexample ce simplify Counterexample _ = String -> Counterexample forall a. HasCallStack => String -> a error String "simplify: impossible, \ \because of the structure of linearise." prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Rank2.Foldable cmd => ParallelCommands cmd resp -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runParallelCommands'. -> PropertyM m () prettyParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd) => ParallelCommands cmd resp -> (History cmd resp, model Concrete, Logic) -> PropertyM m () prettyParallelCommands ParallelCommands cmd resp cmds = ParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m () forall (m :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (model :: (* -> *) -> *). (MonadIO m, Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m () prettyParallelCommandsWithOpts ParallelCommands cmd resp cmds Maybe GraphOptions forall a. Maybe a Nothing -- | Takes the output of parallel program runs and pretty prints a -- counterexample if any of the runs fail. prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Rank2.Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyNParallelCommandsWithOpts :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd) => NParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m () prettyNParallelCommandsWithOpts NParallelCommands cmd resp cmds Maybe GraphOptions mGraphOptions (History cmd resp h, model Concrete _, Logic l) = History cmd resp -> Value -> IO () printCounterexample History cmd resp h (Logic -> Value logic Logic l) IO () -> Property -> PropertyM m () forall (m :: * -> *). Monad m => IO () -> Property -> PropertyM m () `whenFailM` Bool -> Property forall prop. Testable prop => prop -> Property property (Logic -> Bool boolean Logic l) where printCounterexample :: History cmd resp -> Value -> IO () printCounterexample History cmd resp hist' (VFalse Counterexample ce) = do Doc AnsiStyle -> IO () PP.putDoc (Doc AnsiStyle -> IO ()) -> Doc AnsiStyle -> IO () forall a b. (a -> b) -> a -> b $ [Doc AnsiStyle] -> Doc AnsiStyle forall a. Monoid a => [a] -> a mconcat [ Doc AnsiStyle forall ann. Doc ann PP.line , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (Counterexample -> String forall a. Show a => a -> String show (Counterexample -> String) -> Counterexample -> String forall a b. (a -> b) -> a -> b $ Counterexample -> Counterexample simplify Counterexample ce) , Doc AnsiStyle forall ann. Doc ann PP.line ] case Maybe GraphOptions mGraphOptions of Maybe GraphOptions Nothing -> () -> IO () forall a. a -> IO a forall (m :: * -> *) a. Monad m => a -> m a return () Just GraphOptions gOptions -> NParallelCommands cmd resp -> GraphOptions -> History cmd resp -> IO () forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (t :: * -> *). (Foldable t, Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommandsF t cmd resp -> GraphOptions -> History cmd resp -> IO () createAndPrintDot NParallelCommands cmd resp cmds GraphOptions gOptions History cmd resp hist' printCounterexample History cmd resp _hist Value _ = String -> IO () forall a. HasCallStack => String -> a error String "prettyNParallelCommands: impossible, because `boolean l` was False." prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Rank2.Foldable cmd => NParallelCommands cmd resp -> (History cmd resp, model Concrete, Logic) -- ^ Output of 'runNParallelCommands'. -> PropertyM m () prettyNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd) => NParallelCommands cmd resp -> (History cmd resp, model Concrete, Logic) -> PropertyM m () prettyNParallelCommands NParallelCommands cmd resp cmds = NParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m () forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), MonadIO m, Foldable cmd) => NParallelCommands cmd resp -> Maybe GraphOptions -> (History cmd resp, model Concrete, Logic) -> PropertyM m () prettyNParallelCommandsWithOpts NParallelCommands cmd resp cmds Maybe GraphOptions forall a. Maybe a Nothing -- | Draw an ASCII diagram of the history of a parallel program. Useful for -- seeing how a race condition might have occured. toBoxDrawings :: forall cmd resp ann. Rank2.Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc ann toBoxDrawings :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) ann. (Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc ann toBoxDrawings (ParallelCommands Commands cmd resp prefix [Pair (Commands cmd resp)] suffixes) = Set Var -> History cmd resp -> Doc ann toBoxDrawings'' Set Var allVars where allVars :: Set Var allVars = Commands cmd resp -> Set Var forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable cmd => Commands cmd resp -> Set Var getAllUsedVars Commands cmd resp prefix Set Var -> Set Var -> Set Var forall a. Ord a => Set a -> Set a -> Set a `S.union` (Pair (Commands cmd resp) -> Set Var) -> [Pair (Commands cmd resp)] -> Set Var forall m a. Monoid m => (a -> m) -> [a] -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap ((Commands cmd resp -> Set Var) -> Pair (Commands cmd resp) -> Set Var forall m a. Monoid m => (a -> m) -> Pair a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap Commands cmd resp -> Set Var forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable cmd => Commands cmd resp -> Set Var getAllUsedVars) [Pair (Commands cmd resp)] suffixes toBoxDrawings'' :: Set Var -> History cmd resp -> Doc ann toBoxDrawings'' :: Set Var -> History cmd resp -> Doc ann toBoxDrawings'' Set Var knownVars (History History' cmd resp h) = [Doc ann] -> Doc ann forall a. Monoid a => [a] -> a mconcat ([ [(EventType, Pid)] -> Fork [String] -> Doc ann forall ann. [(EventType, Pid)] -> Fork [String] -> Doc ann exec [(EventType, Pid)] evT (((Pid, HistoryEvent cmd resp) -> String) -> History' cmd resp -> [String] forall a b. (a -> b) -> [a] -> [b] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (HistoryEvent cmd resp -> String out (HistoryEvent cmd resp -> String) -> ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp) -> (Pid, HistoryEvent cmd resp) -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . (Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp forall a b. (a, b) -> b snd) (History' cmd resp -> [String]) -> Fork (History' cmd resp) -> Fork [String] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> History' cmd resp -> History' cmd resp -> History' cmd resp -> Fork (History' cmd resp) forall a. a -> a -> a -> Fork a Fork History' cmd resp l History' cmd resp p History' cmd resp r) , Doc ann forall ann. Doc ann PP.line , Doc ann forall ann. Doc ann PP.line ] [Doc ann] -> [Doc ann] -> [Doc ann] forall a. [a] -> [a] -> [a] ++ ((Int, String) -> Doc ann) -> [(Int, String)] -> [Doc ann] forall a b. (a -> b) -> [a] -> [b] map (Int, String) -> Doc ann ppException [(Int, String)] exceptions ) where (Int _, [(Int, String)] exceptions, History' cmd resp h'') = ((Int, [(Int, String)], History' cmd resp) -> (Pid, HistoryEvent cmd resp) -> (Int, [(Int, String)], History' cmd resp)) -> (Int, [(Int, String)], History' cmd resp) -> History' cmd resp -> (Int, [(Int, String)], History' cmd resp) forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl' (\(Int i, [(Int, String)] excs, History' cmd resp evs) (Pid pid, HistoryEvent cmd resp ev) -> case HistoryEvent cmd resp ev of Exception String err -> (Int i Int -> Int -> Int forall a. Num a => a -> a -> a + Int 1, [(Int, String)] excs [(Int, String)] -> [(Int, String)] -> [(Int, String)] forall a. [a] -> [a] -> [a] ++ [(Int i, String err)], History' cmd resp evs History' cmd resp -> History' cmd resp -> History' cmd resp forall a. [a] -> [a] -> [a] ++ [(Pid pid, String -> HistoryEvent cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). String -> HistoryEvent cmd resp Exception (String -> HistoryEvent cmd resp) -> String -> HistoryEvent cmd resp forall a b. (a -> b) -> a -> b $ String "Exception " String -> String -> String forall a. Semigroup a => a -> a -> a <> Int -> String forall a. Show a => a -> String show Int i)]) HistoryEvent cmd resp _ -> (Int i, [(Int, String)] excs, History' cmd resp evs History' cmd resp -> History' cmd resp -> History' cmd resp forall a. [a] -> [a] -> [a] ++ [(Pid pid, HistoryEvent cmd resp ev)]) ) (Int 0 :: Int, [], []) History' cmd resp h (History' cmd resp p, History' cmd resp h') = ((Pid, HistoryEvent cmd resp) -> Bool) -> History' cmd resp -> (History' cmd resp, History' cmd resp) forall a. (a -> Bool) -> [a] -> ([a], [a]) partition (\(Pid, HistoryEvent cmd resp) e -> (Pid, HistoryEvent cmd resp) -> Pid forall a b. (a, b) -> a fst (Pid, HistoryEvent cmd resp) e Pid -> Pid -> Bool forall a. Eq a => a -> a -> Bool == Int -> Pid Pid Int 0) History' cmd resp h'' (History' cmd resp l, History' cmd resp r) = ((Pid, HistoryEvent cmd resp) -> Bool) -> History' cmd resp -> (History' cmd resp, History' cmd resp) forall a. (a -> Bool) -> [a] -> ([a], [a]) partition (\(Pid, HistoryEvent cmd resp) e -> (Pid, HistoryEvent cmd resp) -> Pid forall a b. (a, b) -> a fst (Pid, HistoryEvent cmd resp) e Pid -> Pid -> Bool forall a. Eq a => a -> a -> Bool == Int -> Pid Pid Int 1) History' cmd resp h' out :: HistoryEvent cmd resp -> String out :: HistoryEvent cmd resp -> String out (Invocation cmd Concrete cmd Set Var vars) | Set Var vars Set Var -> Set Var -> Bool forall a. Ord a => Set a -> Set a -> Bool `S.isSubsetOf` Set Var knownVars = [Var] -> String forall a. Show a => a -> String show (Set Var -> [Var] forall a. Set a -> [a] S.toList Set Var vars) String -> String -> String forall a. [a] -> [a] -> [a] ++ String " ← " String -> String -> String forall a. [a] -> [a] -> [a] ++ cmd Concrete -> String forall a. Show a => a -> String show cmd Concrete cmd | Bool otherwise = cmd Concrete -> String forall a. Show a => a -> String show cmd Concrete cmd out (Response resp Concrete resp) = resp Concrete -> String forall a. Show a => a -> String show resp Concrete resp out (Exception String err) = String err toEventType :: History' cmd resp -> [(EventType, Pid)] toEventType :: History' cmd resp -> [(EventType, Pid)] toEventType = ((Pid, HistoryEvent cmd resp) -> (EventType, Pid)) -> History' cmd resp -> [(EventType, Pid)] forall a b. (a -> b) -> [a] -> [b] map (Pid, HistoryEvent cmd resp) -> (EventType, Pid) forall {b} {cmd :: (* -> *) -> *} {resp :: (* -> *) -> *}. (b, HistoryEvent cmd resp) -> (EventType, b) go where go :: (b, HistoryEvent cmd resp) -> (EventType, b) go (b, HistoryEvent cmd resp) e = case (b, HistoryEvent cmd resp) e of (b pid, Invocation cmd Concrete _ Set Var _) -> (EventType Open, b pid) (b pid, Response resp Concrete _) -> (EventType Close, b pid) (b pid, Exception String _) -> (EventType Close, b pid) evT :: [(EventType, Pid)] evT :: [(EventType, Pid)] evT = History' cmd resp -> [(EventType, Pid)] toEventType (((Pid, HistoryEvent cmd resp) -> Bool) -> History' cmd resp -> History' cmd resp forall a. (a -> Bool) -> [a] -> [a] filter (\(Pid, HistoryEvent cmd resp) e -> (Pid, HistoryEvent cmd resp) -> Pid forall a b. (a, b) -> a fst (Pid, HistoryEvent cmd resp) e Pid -> [Pid] -> Bool forall a. Eq a => a -> [a] -> Bool forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool `Prelude.elem` (Int -> Pid) -> [Int] -> [Pid] forall a b. (a -> b) -> [a] -> [b] map Int -> Pid Pid [Int 1, Int 2]) History' cmd resp h) ppException :: (Int, String) -> Doc ann ppException :: (Int, String) -> Doc ann ppException (Int idx, String err) = [Doc ann] -> Doc ann forall a. Monoid a => [a] -> a mconcat [ String -> Doc ann forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (String -> Doc ann) -> String -> Doc ann forall a b. (a -> b) -> a -> b $ String "Exception " String -> String -> String forall a. Semigroup a => a -> a -> a <> Int -> String forall a. Show a => a -> String show Int idx String -> String -> String forall a. Semigroup a => a -> a -> a <> String ":" , Doc ann forall ann. Doc ann PP.line , Int -> Doc ann -> Doc ann forall ann. Int -> Doc ann -> Doc ann PP.indent Int 2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann forall a b. (a -> b) -> a -> b $ String -> Doc ann forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String err , Doc ann forall ann. Doc ann PP.line , Doc ann forall ann. Doc ann PP.line ] createAndPrintDot :: forall cmd resp t. Foldable t => Rank2.Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommandsF t cmd resp -> GraphOptions -> History cmd resp -> IO () createAndPrintDot :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (t :: * -> *). (Foldable t, Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) => ParallelCommandsF t cmd resp -> GraphOptions -> History cmd resp -> IO () createAndPrintDot (ParallelCommands Commands cmd resp prefix [t (Commands cmd resp)] suffixes) GraphOptions gOptions = Set Var -> History cmd resp -> IO () toDotGraph Set Var allVars where allVars :: Set Var allVars = Commands cmd resp -> Set Var forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable cmd => Commands cmd resp -> Set Var getAllUsedVars Commands cmd resp prefix Set Var -> Set Var -> Set Var forall a. Ord a => Set a -> Set a -> Set a `S.union` (t (Commands cmd resp) -> Set Var) -> [t (Commands cmd resp)] -> Set Var forall m a. Monoid m => (a -> m) -> [a] -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap ((Commands cmd resp -> Set Var) -> t (Commands cmd resp) -> Set Var forall m a. Monoid m => (a -> m) -> t a -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap Commands cmd resp -> Set Var forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable cmd => Commands cmd resp -> Set Var getAllUsedVars) [t (Commands cmd resp)] suffixes toDotGraph :: Set Var -> History cmd resp -> IO () toDotGraph :: Set Var -> History cmd resp -> IO () toDotGraph Set Var knownVars (History History' cmd resp h) = GraphOptions -> Rose [String] -> IO () printDotGraph GraphOptions gOptions (Rose [String] -> IO ()) -> Rose [String] -> IO () forall a b. (a -> b) -> a -> b $ (HistoryEvent cmd resp -> String) -> [HistoryEvent cmd resp] -> [String] forall a b. (a -> b) -> [a] -> [b] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap HistoryEvent cmd resp -> String out ([HistoryEvent cmd resp] -> [String]) -> Rose [HistoryEvent cmd resp] -> Rose [String] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [HistoryEvent cmd resp] -> Map Pid [HistoryEvent cmd resp] -> Rose [HistoryEvent cmd resp] forall a. a -> Map Pid a -> Rose a Rose ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp forall a b. (a, b) -> b snd ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp) -> History' cmd resp -> [HistoryEvent cmd resp] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> History' cmd resp prefixMessages) Map Pid [HistoryEvent cmd resp] groupByPid where (History' cmd resp prefixMessages, History' cmd resp h') = ((Pid, HistoryEvent cmd resp) -> Bool) -> History' cmd resp -> (History' cmd resp, History' cmd resp) forall a. (a -> Bool) -> [a] -> ([a], [a]) partition (\(Pid, HistoryEvent cmd resp) e -> (Pid, HistoryEvent cmd resp) -> Pid forall a b. (a, b) -> a fst (Pid, HistoryEvent cmd resp) e Pid -> Pid -> Bool forall a. Eq a => a -> a -> Bool == Int -> Pid Pid Int 0) History' cmd resp h alterF :: a -> Maybe [a] -> Maybe [a] alterF a a Maybe [a] Nothing = [a] -> Maybe [a] forall a. a -> Maybe a Just [a a] alterF a a (Just [a] ls) = [a] -> Maybe [a] forall a. a -> Maybe a Just ([a] -> Maybe [a]) -> [a] -> Maybe [a] forall a b. (a -> b) -> a -> b $ a a a -> [a] -> [a] forall a. a -> [a] -> [a] : [a] ls groupByPid :: Map Pid [HistoryEvent cmd resp] groupByPid = ((Pid, HistoryEvent cmd resp) -> Map Pid [HistoryEvent cmd resp] -> Map Pid [HistoryEvent cmd resp]) -> Map Pid [HistoryEvent cmd resp] -> History' cmd resp -> Map Pid [HistoryEvent cmd resp] forall a b. (a -> b -> b) -> b -> [a] -> b forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr (\(Pid p,HistoryEvent cmd resp e) Map Pid [HistoryEvent cmd resp] m -> (Maybe [HistoryEvent cmd resp] -> Maybe [HistoryEvent cmd resp]) -> Pid -> Map Pid [HistoryEvent cmd resp] -> Map Pid [HistoryEvent cmd resp] forall k a. Ord k => (Maybe a -> Maybe a) -> k -> Map k a -> Map k a Map.alter (HistoryEvent cmd resp -> Maybe [HistoryEvent cmd resp] -> Maybe [HistoryEvent cmd resp] forall {a}. a -> Maybe [a] -> Maybe [a] alterF HistoryEvent cmd resp e) Pid p Map Pid [HistoryEvent cmd resp] m) Map Pid [HistoryEvent cmd resp] forall k a. Map k a Map.empty History' cmd resp h' out :: HistoryEvent cmd resp -> String out :: HistoryEvent cmd resp -> String out (Invocation cmd Concrete cmd Set Var vars) | Set Var vars Set Var -> Set Var -> Bool forall a. Ord a => Set a -> Set a -> Bool `S.isSubsetOf` Set Var knownVars = [Var] -> String forall a. Show a => a -> String show (Set Var -> [Var] forall a. Set a -> [a] S.toList Set Var vars) String -> String -> String forall a. [a] -> [a] -> [a] ++ String " ← " String -> String -> String forall a. [a] -> [a] -> [a] ++ cmd Concrete -> String forall a. Show a => a -> String show cmd Concrete cmd | Bool otherwise = cmd Concrete -> String forall a. Show a => a -> String show cmd Concrete cmd out (Response resp Concrete resp) = String " → " String -> String -> String forall a. [a] -> [a] -> [a] ++ resp Concrete -> String forall a. Show a => a -> String show resp Concrete resp out (Exception String err) = String " → " String -> String -> String forall a. [a] -> [a] -> [a] ++ String err getAllUsedVars :: Rank2.Foldable cmd => Commands cmd resp -> Set Var getAllUsedVars :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable cmd => Commands cmd resp -> Set Var getAllUsedVars = [Var] -> Set Var forall a. Ord a => [a] -> Set a S.fromList ([Var] -> Set Var) -> (Commands cmd resp -> [Var]) -> Commands cmd resp -> Set Var forall b c a. (b -> c) -> (a -> b) -> a -> c . (Command cmd resp -> [Var]) -> [Command cmd resp] -> [Var] forall m a. Monoid m => (a -> m) -> [a] -> m forall (t :: * -> *) m a. (Foldable t, Monoid m) => (a -> m) -> t a -> m foldMap (\(Command cmd Symbolic cmd resp Symbolic _ [Var] _) -> cmd Symbolic -> [Var] forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var] getUsedVars cmd Symbolic cmd) ([Command cmd resp] -> [Var]) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> [Var] forall b c a. (b -> c) -> (a -> b) -> a -> c . Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands -- | Print the percentage of each command used. The prefix check is -- an unfortunate remaining for backwards compatibility. checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property checkCommandNamesParallel :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (t :: * -> *). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> Property -> Property checkCommandNamesParallel ParallelCommandsF t cmd resp cmds = Commands cmd resp -> Property -> Property forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> Property -> Property checkCommandNames (Commands cmd resp -> Property -> Property) -> Commands cmd resp -> Property -> Property forall a b. (a -> b) -> a -> b $ ParallelCommandsF t cmd resp -> Commands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp toSequential ParallelCommandsF t cmd resp cmds -- | Fail if some commands have not been executed. coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property coverCommandNamesParallel :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (t :: * -> *). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> Property -> Property coverCommandNamesParallel ParallelCommandsF t cmd resp cmds = Commands cmd resp -> Property -> Property forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> Property -> Property coverCommandNames (Commands cmd resp -> Property -> Property) -> Commands cmd resp -> Property -> Property forall a b. (a -> b) -> a -> b $ ParallelCommandsF t cmd resp -> Commands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp toSequential ParallelCommandsF t cmd resp cmds commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> [(String, Int)] commandNamesParallel :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (t :: * -> *). (Foldable t, CommandNames cmd) => ParallelCommandsF t cmd resp -> [(String, Int)] commandNamesParallel = Commands cmd resp -> [(String, Int)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> [(String, Int)] commandNames (Commands cmd resp -> [(String, Int)]) -> (ParallelCommandsF t cmd resp -> Commands cmd resp) -> ParallelCommandsF t cmd resp -> [(String, Int)] forall b c a. (b -> c) -> (a -> b) -> a -> c . ParallelCommandsF t cmd resp -> Commands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp toSequential toSequential :: Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp toSequential :: forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp toSequential ParallelCommandsF t cmd resp cmds = ParallelCommandsF t cmd resp -> Commands cmd resp forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). ParallelCommandsF t cmd resp -> Commands cmd resp prefix ParallelCommandsF t cmd resp cmds Commands cmd resp -> Commands cmd resp -> Commands cmd resp forall a. Semigroup a => a -> a -> a <> [Commands cmd resp] -> Commands cmd resp forall a. Monoid a => [a] -> a mconcat ((t (Commands cmd resp) -> [Commands cmd resp]) -> [t (Commands cmd resp)] -> [Commands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap t (Commands cmd resp) -> [Commands cmd resp] forall a. t a -> [a] forall (t :: * -> *) a. Foldable t => t a -> [a] toList (ParallelCommandsF t cmd resp -> [t (Commands cmd resp)] forall (t :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). ParallelCommandsF t cmd resp -> [t (Commands cmd resp)] suffixes ParallelCommandsF t cmd resp cmds))