{-# LANGUAGE BangPatterns #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} ----------------------------------------------------------------------------- -- | -- Module : Test.StateMachine.Sequential -- 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 -- sequential programs. -- ----------------------------------------------------------------------------- module Test.StateMachine.Sequential ( forAllCommands , existsCommands , generateCommands , generateCommandsState , deadlockError , getUsedVars , shrinkCommands , shrinkAndValidate , ValidateEnv(..) , ShouldShrink(..) , initValidateEnv , runCommands , runCommands' , getChanContents , Check(..) , executeCommands , prettyPrintHistory , prettyPrintHistory' , prettyCommands , prettyCommands' , saveCommands , runSavedCommands , commandNames , commandNamesInOrder , coverCommandNames , checkCommandNames , showLabelledExamples , showLabelledExamples' ) where import Control.Exception (SomeAsyncException(..), SomeException, displayException, fromException) import Control.Monad (when) import Control.Monad.Catch (ExitCase(..), MonadCatch, MonadMask, catch, generalBracket) import Control.Monad.State.Strict (StateT, evalStateT, get, lift, put, runStateT) import Data.Bifunctor (second) import Data.Dynamic (Dynamic, toDyn) import Data.Either (fromRight) import Data.List (inits) import qualified Data.Map as M import Data.Map.Strict (Map) import Data.Maybe (fromMaybe) import Data.Monoid import Data.Proxy (Proxy(..)) import qualified Data.Set as S import Data.Time (defaultTimeLocale, formatTime, getZonedTime) import Prelude import Prettyprinter (Doc) import qualified Prettyprinter as PP import qualified Prettyprinter.Render.Terminal as PP import System.Directory (createDirectoryIfMissing) import System.FilePath ((</>)) import System.Random (getStdRandom, randomR) import Test.QuickCheck (Gen, Property, Testable, choose, cover, forAllShrinkShow, labelledExamplesWith, maxSuccess, once, property, replay, sized, stdArgs, tabulate, whenFail) import Test.QuickCheck.Monadic (PropertyM, run) import Test.QuickCheck.Random (mkQCGen) import Text.Show.Pretty (ppShow) import UnliftIO (MonadIO, TChan, atomically, liftIO, newTChanIO, tryReadTChan, writeTChan) import UnliftIO.Exception (throwIO) import Test.StateMachine.ConstructorName import Test.StateMachine.Diffing (CanDiff(..), ediff) import Test.StateMachine.Labelling (Event(..), execCmds) import Test.StateMachine.Logic import Test.StateMachine.Types import qualified Test.StateMachine.Types.Rank2 as Rank2 import Test.StateMachine.Utils ------------------------------------------------------------------------ forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Maybe Int -- ^ Minimum number of commands. -> (Commands cmd resp -> prop) -- ^ Predicate. -> Property forAllCommands :: 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 -> (Commands cmd resp -> prop) -> Property forAllCommands StateMachine model cmd m resp sm Maybe Int mminSize = Gen (Commands cmd resp) -> (Commands cmd resp -> [Commands cmd resp]) -> (Commands cmd resp -> String) -> (Commands cmd resp -> prop) -> Property forall prop a. Testable prop => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property forAllShrinkShow (StateMachine model cmd m resp -> Maybe Int -> Gen (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) (StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp] shrinkCommands StateMachine model cmd m resp sm) Commands cmd resp -> String forall a. Show a => a -> String ppShow -- | Generate commands from a list of generators. existsCommands :: forall model cmd m resp prop. (Testable prop, Rank2.Foldable resp) => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> [model Symbolic -> Gen (cmd Symbolic)] -- ^ Generators. -> (Commands cmd resp -> prop) -- ^ Predicate. -> Property existsCommands :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *) prop. (Testable prop, Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> [model Symbolic -> Gen (cmd Symbolic)] -> (Commands cmd resp -> prop) -> Property existsCommands 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, 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 -> Gen (cmd Symbolic)] gens0 = Property -> Property forall prop. Testable prop => prop -> Property once (Property -> Property) -> ((Commands cmd resp -> prop) -> Property) -> (Commands cmd resp -> prop) -> Property forall b c a. (b -> c) -> (a -> b) -> a -> c . Gen (Commands cmd resp) -> (Commands cmd resp -> [Commands cmd resp]) -> (Commands cmd resp -> String) -> (Commands cmd resp -> prop) -> Property forall prop a. Testable prop => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property forAllShrinkShow ([model Symbolic -> Gen (cmd Symbolic)] -> model Symbolic -> Counter -> [Command cmd resp] -> Gen (Commands cmd resp) go [model Symbolic -> Gen (cmd Symbolic)] gens0 model Symbolic forall (r :: * -> *). model r initModel Counter newCounter []) ([Commands cmd resp] -> Commands cmd resp -> [Commands cmd resp] forall a b. a -> b -> a const []) Commands cmd resp -> String forall a. Show a => a -> String ppShow where go :: [model Symbolic -> Gen (cmd Symbolic)] -> model Symbolic -> Counter -> [Command cmd resp] -> Gen (Commands cmd resp) go :: [model Symbolic -> Gen (cmd Symbolic)] -> model Symbolic -> Counter -> [Command cmd resp] -> Gen (Commands cmd resp) go [] model Symbolic _model Counter _counter [Command cmd resp] acc = Commands cmd resp -> Gen (Commands cmd resp) forall a. a -> Gen a forall (m :: * -> *) a. Monad m => a -> m a return ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands ([Command cmd resp] -> [Command cmd resp] forall a. [a] -> [a] reverse [Command cmd resp] acc)) go (model Symbolic -> Gen (cmd Symbolic) gen : [model Symbolic -> Gen (cmd Symbolic)] gens) model Symbolic model Counter counter [Command cmd resp] acc = do cmd Symbolic cmd <- ([cmd Symbolic] -> cmd Symbolic) -> (cmd Symbolic -> cmd Symbolic) -> Either [cmd Symbolic] (cmd Symbolic) -> cmd Symbolic forall a c b. (a -> c) -> (b -> c) -> Either a b -> c either (model Symbolic -> [Command cmd resp] -> String -> cmd Symbolic forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) b. (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b deadlockError model Symbolic model [Command cmd resp] acc (String -> cmd Symbolic) -> ([cmd Symbolic] -> String) -> [cmd Symbolic] -> cmd Symbolic forall b c a. (b -> c) -> (a -> b) -> a -> c . [cmd Symbolic] -> String forall a. Show a => a -> String ppShow) cmd Symbolic -> cmd Symbolic forall a. a -> a id (Either [cmd Symbolic] (cmd Symbolic) -> cmd Symbolic) -> Gen (Either [cmd Symbolic] (cmd Symbolic)) -> Gen (cmd Symbolic) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> model Symbolic -> Gen (cmd Symbolic) gen model Symbolic model Gen (cmd Symbolic) -> (cmd Symbolic -> Bool) -> Gen (Either [cmd Symbolic] (cmd Symbolic)) forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a) `suchThatEither` (Logic -> Bool boolean (Logic -> Bool) -> (cmd Symbolic -> Logic) -> cmd Symbolic -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . model Symbolic -> cmd Symbolic -> Logic precondition model Symbolic model) let (resp Symbolic resp, Counter counter') = 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 counter [model Symbolic -> Gen (cmd Symbolic)] -> model Symbolic -> Counter -> [Command cmd resp] -> Gen (Commands cmd resp) go [model Symbolic -> Gen (cmd Symbolic)] gens (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) Counter counter' (cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp Command cmd Symbolic cmd resp Symbolic resp (resp Symbolic -> [Var] forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var] getUsedVars resp Symbolic resp) Command cmd resp -> [Command cmd resp] -> [Command cmd resp] forall a. a -> [a] -> [a] : [Command cmd resp] acc) deadlockError :: (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b deadlockError :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) b. (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b deadlockError model Symbolic model [Command cmd resp] generated String counterexamples = String -> b forall a. HasCallStack => String -> a error (String -> b) -> String -> b forall a b. (a -> b) -> a -> b $ [String] -> String forall (t :: * -> *) a. Foldable t => t [a] -> [a] concat [ String "\n" , String "A deadlock occured while generating commands.\n" , String "No pre-condition holds in the following model:\n\n" , String " " String -> String -> String forall a. [a] -> [a] -> [a] ++ model Symbolic -> String forall a. Show a => a -> String ppShow model Symbolic model , String "\n\nThe following commands have been generated so far:\n\n" , String " " String -> String -> String forall a. [a] -> [a] -> [a] ++ [Command cmd resp] -> String forall a. Show a => a -> String ppShow [Command cmd resp] generated , String "\n\n" , String "Example commands generated whose pre-condition doesn't hold:\n\n" , String " " String -> String -> String forall a. [a] -> [a] -> [a] ++ String counterexamples , String "\n" ] generateCommands :: (Rank2.Foldable resp, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -- ^ Minimum number of commands. -> Gen (Commands cmd resp) generateCommands :: 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 sm :: StateMachine model cmd m resp sm@StateMachine { forall (r :: * -> *). model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r initModel :: forall (r :: * -> *). model r initModel } Maybe Int mminSize = StateT (model Symbolic) Gen (Commands cmd resp) -> model Symbolic -> Gen (Commands cmd resp) forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a evalStateT (StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic) Gen (Commands cmd resp) forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic) Gen (Commands cmd resp) generateCommandsState StateMachine model cmd m resp sm Counter newCounter Maybe Int mminSize) model Symbolic forall (r :: * -> *). model r initModel generateCommandsState :: forall model cmd m resp. Rank2.Foldable resp => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Counter -> Maybe Int -- ^ Minimum number of commands. -> StateT (model Symbolic) Gen (Commands cmd resp) generateCommandsState :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Foldable resp, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic) Gen (Commands cmd resp) generateCommandsState StateMachine { model Symbolic -> cmd Symbolic -> Logic precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> Logic precondition :: model Symbolic -> cmd Symbolic -> Logic precondition, model Symbolic -> Maybe (Gen (cmd Symbolic)) generator :: model Symbolic -> Maybe (Gen (cmd Symbolic)) generator :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Maybe (Gen (cmd Symbolic)) generator, forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock } Counter counter0 Maybe Int mminSize = do let minSize :: Int minSize = Int -> Maybe Int -> Int forall a. a -> Maybe a -> a fromMaybe Int 0 Maybe Int mminSize Int size0 <- Gen Int -> StateT (model Symbolic) Gen Int forall (m :: * -> *) a. Monad m => m a -> StateT (model Symbolic) m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift ((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 minSize, Int k Int -> Int -> Int forall a. Num a => a -> a -> a + Int minSize))) Int -> Counter -> [Command cmd resp] -> StateT (model Symbolic) Gen (Commands cmd resp) go Int size0 Counter counter0 [] where go :: Int -> Counter -> [Command cmd resp] -> StateT (model Symbolic) Gen (Commands cmd resp) go :: Int -> Counter -> [Command cmd resp] -> StateT (model Symbolic) Gen (Commands cmd resp) go Int 0 Counter _ [Command cmd resp] cmds = Commands cmd resp -> StateT (model Symbolic) Gen (Commands cmd resp) forall a. a -> StateT (model Symbolic) Gen a forall (m :: * -> *) a. Monad m => a -> m a return ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands ([Command cmd resp] -> [Command cmd resp] forall a. [a] -> [a] reverse [Command cmd resp] cmds)) go Int size Counter counter [Command cmd resp] cmds = do model Symbolic model <- StateT (model Symbolic) Gen (model Symbolic) forall s (m :: * -> *). MonadState s m => m s get case model Symbolic -> Maybe (Gen (cmd Symbolic)) generator model Symbolic model of Maybe (Gen (cmd Symbolic)) Nothing -> Commands cmd resp -> StateT (model Symbolic) Gen (Commands cmd resp) forall a. a -> StateT (model Symbolic) Gen a forall (m :: * -> *) a. Monad m => a -> m a return ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands ([Command cmd resp] -> [Command cmd resp] forall a. [a] -> [a] reverse [Command cmd resp] cmds)) Just Gen (cmd Symbolic) gen -> do Either [cmd Symbolic] (cmd Symbolic) enext <- Gen (Either [cmd Symbolic] (cmd Symbolic)) -> StateT (model Symbolic) Gen (Either [cmd Symbolic] (cmd Symbolic)) forall (m :: * -> *) a. Monad m => m a -> StateT (model Symbolic) m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Gen (Either [cmd Symbolic] (cmd Symbolic)) -> StateT (model Symbolic) Gen (Either [cmd Symbolic] (cmd Symbolic))) -> Gen (Either [cmd Symbolic] (cmd Symbolic)) -> StateT (model Symbolic) Gen (Either [cmd Symbolic] (cmd Symbolic)) forall a b. (a -> b) -> a -> b $ Gen (cmd Symbolic) gen Gen (cmd Symbolic) -> (cmd Symbolic -> Bool) -> Gen (Either [cmd Symbolic] (cmd Symbolic)) forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a) `suchThatEither` (Logic -> Bool boolean (Logic -> Bool) -> (cmd Symbolic -> Logic) -> cmd Symbolic -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . model Symbolic -> cmd Symbolic -> Logic precondition model Symbolic model) case Either [cmd Symbolic] (cmd Symbolic) enext of Left [cmd Symbolic] ces -> model Symbolic -> [Command cmd resp] -> String -> StateT (model Symbolic) Gen (Commands cmd resp) forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) b. (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b deadlockError model Symbolic model ([Command cmd resp] -> [Command cmd resp] forall a. [a] -> [a] reverse [Command cmd resp] cmds) ([cmd Symbolic] -> String forall a. Show a => a -> String ppShow [cmd Symbolic] ces) Right cmd Symbolic next -> do let (resp Symbolic resp, Counter counter') = 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 next) Counter counter model Symbolic -> StateT (model Symbolic) Gen () forall s (m :: * -> *). MonadState s m => s -> m () put (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 next resp Symbolic resp) Int -> Counter -> [Command cmd resp] -> StateT (model Symbolic) Gen (Commands cmd resp) go (Int size Int -> Int -> Int forall a. Num a => a -> a -> a - Int 1) Counter counter' (cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp Command cmd Symbolic next resp Symbolic resp (resp Symbolic -> [Var] forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var] getUsedVars resp Symbolic resp) Command cmd resp -> [Command cmd resp] -> [Command cmd resp] forall a. a -> [a] -> [a] : [Command cmd resp] cmds) getUsedVars :: Rank2.Foldable f => f Symbolic -> [Var] getUsedVars :: forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var] getUsedVars = (forall x. Symbolic x -> [Var]) -> f Symbolic -> [Var] forall m (p :: * -> *). Monoid m => (forall x. p x -> m) -> f p -> m forall k (f :: (k -> *) -> *) m (p :: k -> *). (Foldable f, Monoid m) => (forall (x :: k). p x -> m) -> f p -> m Rank2.foldMap (\(Symbolic Var v) -> [Var v]) -- | Shrink commands in a pre-condition and scope respecting way. shrinkCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp] shrinkCommands :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp] shrinkCommands 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 } = (Shrunk [Command cmd resp] -> [Commands cmd resp]) -> [Shrunk [Command cmd resp]] -> [Commands cmd resp] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap Shrunk [Command cmd resp] -> [Commands cmd resp] go ([Shrunk [Command cmd resp]] -> [Commands cmd resp]) -> (Commands cmd resp -> [Shrunk [Command cmd resp]]) -> Commands cmd resp -> [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 where go :: Shrunk [Command cmd resp] -> [Commands cmd resp] go :: Shrunk [Command cmd resp] -> [Commands cmd resp] go (Shrunk Bool shrunk [Command cmd resp] cmds) = ((ValidateEnv model, Commands cmd resp) -> Commands cmd resp) -> [(ValidateEnv model, Commands cmd resp)] -> [Commands cmd resp] forall a b. (a -> b) -> [a] -> [b] map (ValidateEnv model, Commands cmd resp) -> Commands cmd resp forall a b. (a, b) -> b snd ([(ValidateEnv model, Commands cmd resp)] -> [Commands cmd resp]) -> [(ValidateEnv model, Commands cmd resp)] -> [Commands cmd resp] forall a b. (a -> b) -> a -> b $ 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 (if Bool shrunk then ShouldShrink DontShrink else ShouldShrink MustShrink) (model Symbolic -> ValidateEnv model forall (model :: (* -> *) -> *). model Symbolic -> ValidateEnv model initValidateEnv model Symbolic forall (r :: * -> *). model r initModel) ([Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands [Command cmd resp] cmds) -- | Environment required during 'shrinkAndValidate' data ValidateEnv model = ValidateEnv { -- | The model we're starting validation from forall (model :: (* -> *) -> *). ValidateEnv model -> model Symbolic veModel :: model Symbolic -- | Reference renumbering -- -- When a command -- -- > Command .. [Var i, ..] -- -- is changed during validation to -- -- > Command .. [Var j, ..] -- -- then any subsequent uses of @Var i@ should be replaced by @Var j@. This -- is recorded in 'veScope'. When we /remove/ the first command -- altogether (during shrinking), then @Var i@ won't appear in the -- 'veScope' and shrank candidates that contain commands referring to @Var -- i@ should be considered as invalid. , forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var veScope :: Map Var Var -- | Counter (for generating new references) , forall (model :: (* -> *) -> *). ValidateEnv model -> Counter veCounter :: Counter } initValidateEnv :: model Symbolic -> ValidateEnv model initValidateEnv :: forall (model :: (* -> *) -> *). model Symbolic -> ValidateEnv model initValidateEnv model Symbolic initModel = ValidateEnv { veModel :: model Symbolic veModel = model Symbolic initModel , veScope :: Map Var Var veScope = Map Var Var forall k a. Map k a M.empty , veCounter :: Counter veCounter = Counter newCounter } data ShouldShrink = MustShrink | DontShrink -- | Validate list of commands, optionally shrinking one of the commands -- -- The input to this function is a list of commands ('Commands'), for example -- -- > [A, B, C, D, E, F, G, H] -- -- The /result/ is a /list/ of 'Commands', i.e. a list of lists. The -- outermost list is used for all the shrinking possibilities. For example, -- let's assume we haven't shrunk something yet, and therefore need to shrink -- one of the commands. Let's further assume that only commands B and E can be -- shrunk, to B1, B2 and E1, E2, E3 respectively. Then the result will look -- something like -- -- > [ -- outermost list recording all the shrink possibilities -- > [A', B1', C', D', E' , F', G', H'] -- B shrunk to B1 -- > , [A', B2', C', D', E' , F', G', H'] -- B shrunk to B2 -- > , [A', B' , C', D', E1', F', G', H'] -- E shrunk to E1 -- > , [A', B' , C', D', E2', F', G', H'] -- E shrunk to E2 -- > , [A', B' , C', D', E3', F', G', H'] -- E shrunk to E3 -- > ] -- -- where one of the commands has been shrunk and all commands have been -- validated and renumbered (references updated). So, in this example, the -- result will contain at most 5 lists; it may contain fewer, since some of -- these lists may not be valid. -- -- If we _did_ already shrink something, then no commands will be shrunk, and -- the resulting list will either be empty (if the list of commands was invalid) -- or contain a /single/ element with the validated and renumbered commands. shrinkAndValidate :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)] shrinkAndValidate :: 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 Symbolic -> cmd Symbolic -> Logic precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> Logic precondition :: model Symbolic -> cmd Symbolic -> Logic precondition, forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition :: forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) mock, model Symbolic -> cmd Symbolic -> [cmd Symbolic] shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic] shrinker :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> [cmd Symbolic] shrinker } = \ShouldShrink env ValidateEnv model shouldShrink Commands cmd resp cmds -> ((ValidateEnv model, [Command cmd resp]) -> (ValidateEnv model, Commands cmd resp)) -> [(ValidateEnv model, [Command cmd resp])] -> [(ValidateEnv model, Commands cmd resp)] forall a b. (a -> b) -> [a] -> [b] map (([Command cmd resp] -> Commands cmd resp) -> (ValidateEnv model, [Command cmd resp]) -> (ValidateEnv model, Commands cmd resp) forall b c a. (b -> c) -> (a, b) -> (a, c) forall (p :: * -> * -> *) b c a. Bifunctor p => (b -> c) -> p a b -> p a c second [Command cmd resp] -> Commands cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). [Command cmd resp] -> Commands cmd resp Commands) ([(ValidateEnv model, [Command cmd resp])] -> [(ValidateEnv model, Commands cmd resp)]) -> [(ValidateEnv model, [Command cmd resp])] -> [(ValidateEnv model, Commands cmd resp)] forall a b. (a -> b) -> a -> b $ ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])] go ShouldShrink env ValidateEnv model shouldShrink (Commands cmd resp -> [Command cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). Commands cmd resp -> [Command cmd resp] unCommands Commands cmd resp cmds) where go :: ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])] go :: ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])] go ShouldShrink MustShrink ValidateEnv model _ [] = [] -- we failed to shrink anything go ShouldShrink DontShrink ValidateEnv model env [] = [(ValidateEnv model env, [])] -- successful termination go ShouldShrink shouldShrink (ValidateEnv model Symbolic model Map Var Var scope Counter counter) (Command cmd Symbolic cmd' resp Symbolic _resp [Var] vars' : [Command cmd resp] cmds) = case (forall a. Symbolic a -> Maybe (Symbolic a)) -> cmd Symbolic -> Maybe (cmd Symbolic) forall k (t :: (k -> *) -> *) (f :: * -> *) (p :: k -> *) (q :: k -> *). (Traversable t, Applicative f) => (forall (a :: k). p a -> f (q a)) -> t p -> f (t q) forall (f :: * -> *) (p :: * -> *) (q :: * -> *). Applicative f => (forall a. p a -> f (q a)) -> cmd p -> f (cmd q) Rank2.traverse (Map Var Var -> Symbolic a -> Maybe (Symbolic a) forall a. Map Var Var -> Symbolic a -> Maybe (Symbolic a) remapVars Map Var Var scope) cmd Symbolic cmd' of Just cmd Symbolic remapped -> -- shrink at most one command let candidates :: [(ShouldShrink, cmd Symbolic)] candidates :: [(ShouldShrink, cmd Symbolic)] candidates = case ShouldShrink shouldShrink of ShouldShrink DontShrink -> [(ShouldShrink DontShrink, cmd Symbolic remapped)] ShouldShrink MustShrink -> (cmd Symbolic -> (ShouldShrink, cmd Symbolic)) -> [cmd Symbolic] -> [(ShouldShrink, cmd Symbolic)] forall a b. (a -> b) -> [a] -> [b] map (ShouldShrink DontShrink,) (model Symbolic -> cmd Symbolic -> [cmd Symbolic] shrinker model Symbolic model cmd Symbolic remapped) [(ShouldShrink, cmd Symbolic)] -> [(ShouldShrink, cmd Symbolic)] -> [(ShouldShrink, cmd Symbolic)] forall a. [a] -> [a] -> [a] ++ [(ShouldShrink MustShrink, cmd Symbolic remapped)] in (((ShouldShrink, cmd Symbolic) -> [(ValidateEnv model, [Command cmd resp])]) -> [(ShouldShrink, cmd Symbolic)] -> [(ValidateEnv model, [Command cmd resp])]) -> [(ShouldShrink, cmd Symbolic)] -> ((ShouldShrink, cmd Symbolic) -> [(ValidateEnv model, [Command cmd resp])]) -> [(ValidateEnv model, [Command cmd resp])] forall a b c. (a -> b -> c) -> b -> a -> c flip ((ShouldShrink, cmd Symbolic) -> [(ValidateEnv model, [Command cmd resp])]) -> [(ShouldShrink, cmd Symbolic)] -> [(ValidateEnv model, [Command cmd resp])] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap [(ShouldShrink, cmd Symbolic)] candidates (((ShouldShrink, cmd Symbolic) -> [(ValidateEnv model, [Command cmd resp])]) -> [(ValidateEnv model, [Command cmd resp])]) -> ((ShouldShrink, cmd Symbolic) -> [(ValidateEnv model, [Command cmd resp])]) -> [(ValidateEnv model, [Command cmd resp])] forall a b. (a -> b) -> a -> b $ \(ShouldShrink shouldShrink', cmd Symbolic cmd) -> if Logic -> Bool boolean (model Symbolic -> cmd Symbolic -> Logic precondition model Symbolic model cmd Symbolic cmd) then let (resp Symbolic resp, Counter counter') = 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 counter vars :: [Var] vars = resp Symbolic -> [Var] forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var] getUsedVars resp Symbolic resp env' :: ValidateEnv model env' = ValidateEnv { veModel :: model Symbolic veModel = 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 , veScope :: Map Var Var veScope = [(Var, Var)] -> Map Var Var forall k a. Ord k => [(k, a)] -> Map k a M.fromList ([Var] -> [Var] -> [(Var, Var)] forall a b. [a] -> [b] -> [(a, b)] zip [Var] vars' [Var] vars) Map Var Var -> Map Var Var -> Map Var Var forall k a. Ord k => Map k a -> Map k a -> Map k a `M.union` Map Var Var scope , veCounter :: Counter veCounter = Counter counter' } in ((ValidateEnv model, [Command cmd resp]) -> (ValidateEnv model, [Command cmd resp])) -> [(ValidateEnv model, [Command cmd resp])] -> [(ValidateEnv model, [Command cmd resp])] forall a b. (a -> b) -> [a] -> [b] map (([Command cmd resp] -> [Command cmd resp]) -> (ValidateEnv model, [Command cmd resp]) -> (ValidateEnv model, [Command cmd resp]) forall b c a. (b -> c) -> (a, b) -> (a, c) forall (p :: * -> * -> *) b c a. Bifunctor p => (b -> c) -> p a b -> p a c second (cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp Command cmd Symbolic cmd resp Symbolic resp [Var] varsCommand cmd resp -> [Command cmd resp] -> [Command cmd resp] forall a. a -> [a] -> [a] :)) ([(ValidateEnv model, [Command cmd resp])] -> [(ValidateEnv model, [Command cmd resp])]) -> [(ValidateEnv model, [Command cmd resp])] -> [(ValidateEnv model, [Command cmd resp])] forall a b. (a -> b) -> a -> b $ ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])] go ShouldShrink shouldShrink' ValidateEnv model env' [Command cmd resp] cmds else [] Maybe (cmd Symbolic) Nothing -> [] remapVars :: Map Var Var -> Symbolic a -> Maybe (Symbolic a) remapVars :: forall a. Map Var Var -> Symbolic a -> Maybe (Symbolic a) remapVars Map Var Var scope (Symbolic Var v) = Var -> Symbolic a forall a. Typeable a => Var -> Symbolic a Symbolic (Var -> Symbolic a) -> Maybe Var -> Maybe (Symbolic a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Var -> Map Var Var -> Maybe Var forall k a. Ord k => k -> Map k a -> Maybe a M.lookup Var v Map Var Var scope runCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) runCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) runCommands StateMachine model cmd m resp sm Commands cmd resp cmds = 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 $ StateMachine model cmd m resp -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason) forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason) runCommands' StateMachine model cmd m resp sm Commands cmd resp cmds runCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason) runCommands' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason) runCommands' 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, model Concrete -> m () cleanup :: model Concrete -> m () cleanup :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () cleanup } Commands cmd resp cmds = do TChan (Pid, HistoryEvent cmd resp) hchan <- m (TChan (Pid, HistoryEvent cmd resp)) forall (m :: * -> *) a. MonadIO m => m (TChan a) newTChanIO (Reason reason, (Environment _, model Symbolic _, Counter _, model Concrete model)) <- ((Reason, (Environment, model Symbolic, Counter, model Concrete)), ()) -> (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall a b. (a, b) -> a fst (((Reason, (Environment, model Symbolic, Counter, model Concrete)), ()) -> (Reason, (Environment, model Symbolic, Counter, model Concrete))) -> m ((Reason, (Environment, model Symbolic, Counter, model Concrete)), ()) -> m (Reason, (Environment, model Symbolic, Counter, model Concrete)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> m () -> (() -> ExitCase (Reason, (Environment, model Symbolic, Counter, model Concrete)) -> m ()) -> (() -> m (Reason, (Environment, model Symbolic, Counter, model Concrete))) -> m ((Reason, (Environment, model Symbolic, Counter, model Concrete)), ()) 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 (Reason, (Environment, model Symbolic, Counter, model Concrete)) ec -> case ExitCase (Reason, (Environment, model Symbolic, Counter, model Concrete)) ec of ExitCaseSuccess (Reason _, (Environment _, model Symbolic _, Counter _, model Concrete model)) -> model Concrete -> m () cleanup model Concrete model ExitCase (Reason, (Environment, model Symbolic, Counter, model Concrete)) _ -> 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 >>= model Concrete -> m () cleanup (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) (\() _ -> do 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 cmds) (Environment emptyEnvironment, model Symbolic forall (r :: * -> *). model r initModel, Counter newCounter, model Concrete forall (r :: * -> *). model r initModel) ) [(Pid, HistoryEvent cmd resp)] hist <- TChan (Pid, HistoryEvent cmd resp) -> m [(Pid, HistoryEvent cmd resp)] forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan (Pid, HistoryEvent cmd resp) hchan (History cmd resp, model Concrete, Reason) -> m (History cmd resp, model Concrete, Reason) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> History cmd resp History [(Pid, HistoryEvent cmd resp)] hist, model Concrete model, Reason reason) -- We should try our best to not let this function fail, -- since it is used to cleanup resources, in parallel programs. getChanContents :: MonadIO m => TChan a -> m [a] getChanContents :: forall (m :: * -> *) a. MonadIO m => TChan a -> m [a] getChanContents TChan a chan = [a] -> [a] forall a. [a] -> [a] reverse ([a] -> [a]) -> m [a] -> m [a] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> STM [a] -> m [a] forall (m :: * -> *) a. MonadIO m => STM a -> m a atomically ([a] -> STM [a] go' []) where go' :: [a] -> STM [a] go' [a] acc = do Maybe a mx <- TChan a -> STM (Maybe a) forall a. TChan a -> STM (Maybe a) tryReadTChan TChan a chan case Maybe a mx of Just a x -> [a] -> STM [a] go' (a x a -> [a] -> [a] forall a. a -> [a] -> [a] : [a] acc) Maybe a Nothing -> [a] -> STM [a] forall a. a -> STM a forall (m :: * -> *) a. Monad m => a -> m a return [a] acc data Check = CheckPrecondition | CheckEverything | CheckNothing executeCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.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 :: 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 {Maybe (model Concrete -> Logic) cmd Concrete -> m (resp Concrete) model Concrete -> m () model Concrete -> cmd Concrete -> resp Concrete -> Logic model Symbolic -> Maybe (Gen (cmd Symbolic)) model Symbolic -> cmd Symbolic -> [cmd Symbolic] model Symbolic -> cmd Symbolic -> Logic model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) forall (r :: * -> *). model r forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> forall (r :: * -> *). model r precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> Logic 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 mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) generator :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> Maybe (Gen (cmd Symbolic)) shrinker :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> [cmd Symbolic] cleanup :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> m () initModel :: forall (r :: * -> *). model r transition :: forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r precondition :: model Symbolic -> cmd Symbolic -> Logic postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic invariant :: Maybe (model Concrete -> Logic) generator :: model Symbolic -> Maybe (Gen (cmd Symbolic)) shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic] semantics :: cmd Concrete -> m (resp Concrete) mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) cleanup :: model Concrete -> m () postcondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> model Concrete -> cmd Concrete -> resp Concrete -> Logic invariant :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> Maybe (model Concrete -> Logic) semantics :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete) ..} TChan (Pid, HistoryEvent cmd resp) hchan Pid pid Check check = [Command cmd resp] -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason go ([Command cmd resp] -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason 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 :: [Command cmd resp] -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason go [] = Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a. a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (m :: * -> *) a. Monad m => a -> m a return Reason Ok go (Command cmd Symbolic scmd resp Symbolic _ [Var] vars : [Command cmd resp] cmds) = do (Environment env, model Symbolic smodel, Counter counter, model Concrete cmodel) <- StateT (Environment, model Symbolic, Counter, model Concrete) m (Environment, model Symbolic, Counter, model Concrete) forall s (m :: * -> *). MonadState s m => m s get case (Check check, Logic -> Value logic (model Symbolic -> cmd Symbolic -> Logic precondition model Symbolic smodel cmd Symbolic scmd)) of (Check CheckPrecondition, VFalse Counterexample ce) -> Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a. a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (m :: * -> *) a. Monad m => a -> m a return (String -> Reason PreconditionFailed (Counterexample -> String forall a. Show a => a -> String show Counterexample ce)) (Check CheckEverything, VFalse Counterexample ce) -> Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a. a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (m :: * -> *) a. Monad m => a -> m a return (String -> Reason PreconditionFailed (Counterexample -> String forall a. Show a => a -> String show Counterexample ce)) (Check, Value) _otherwise -> do let ccmd :: cmd Concrete ccmd = cmd Concrete -> Either EnvironmentError (cmd Concrete) -> cmd Concrete forall b a. b -> Either a b -> b fromRight (String -> cmd Concrete forall a. HasCallStack => String -> a error String "executeCommands: impossible") (Environment -> cmd Symbolic -> Either EnvironmentError (cmd Concrete) forall (t :: (* -> *) -> *). Traversable t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete) reify Environment env cmd Symbolic scmd) STM () -> StateT (Environment, model Symbolic, Counter, model Concrete) m () forall (m :: * -> *) a. MonadIO m => STM a -> m a atomically (TChan (Pid, HistoryEvent cmd resp) -> (Pid, HistoryEvent cmd resp) -> STM () forall a. TChan a -> a -> STM () writeTChan TChan (Pid, HistoryEvent cmd resp) hchan (Pid pid, cmd Concrete -> Set Var -> HistoryEvent cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). cmd Concrete -> Set Var -> HistoryEvent cmd resp Invocation cmd Concrete ccmd ([Var] -> Set Var forall a. Ord a => [a] -> Set a S.fromList [Var] vars))) !Either String (resp Concrete) ecresp <- m (Either String (resp Concrete)) -> StateT (Environment, model Symbolic, Counter, model Concrete) m (Either String (resp Concrete)) forall (m :: * -> *) a. Monad m => m a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (m (Either String (resp Concrete)) -> StateT (Environment, model Symbolic, Counter, model Concrete) m (Either String (resp Concrete))) -> m (Either String (resp Concrete)) -> StateT (Environment, model Symbolic, Counter, model Concrete) m (Either String (resp Concrete)) forall a b. (a -> b) -> a -> b $ (resp Concrete -> Either String (resp Concrete)) -> m (resp Concrete) -> m (Either String (resp Concrete)) forall a b. (a -> b) -> m a -> m b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap resp Concrete -> Either String (resp Concrete) forall a b. b -> Either a b Right (cmd Concrete -> m (resp Concrete) semantics cmd Concrete ccmd) m (Either String (resp Concrete)) -> (SomeException -> m (Either String (resp Concrete))) -> m (Either String (resp Concrete)) forall e a. (HasCallStack, Exception e) => m a -> (e -> m a) -> m a forall (m :: * -> *) e a. (MonadCatch m, HasCallStack, Exception e) => m a -> (e -> m a) -> m a `catch` \(SomeException err :: SomeException) -> do Bool -> m () -> m () forall (f :: * -> *). Applicative f => Bool -> f () -> f () when (SomeException -> Bool isSomeAsyncException SomeException err) (IO () -> m () forall a. IO a -> m a forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO (String -> IO () putStrLn (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ SomeException -> String forall e. Exception e => e -> String displayException SomeException err) m () -> m () -> m () forall a b. m a -> m b -> m b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b >> SomeException -> m () forall (m :: * -> *) e a. (MonadIO m, Exception e) => e -> m a throwIO SomeException err) Either String (resp Concrete) -> m (Either String (resp Concrete)) forall a. a -> m a forall (m :: * -> *) a. Monad m => a -> m a return (String -> Either String (resp Concrete) forall a b. a -> Either a b Left (SomeException -> String forall e. Exception e => e -> String displayException SomeException err)) case Either String (resp Concrete) ecresp of Left String err -> do STM () -> StateT (Environment, model Symbolic, Counter, model Concrete) m () forall (m :: * -> *) a. MonadIO m => STM a -> m a atomically (TChan (Pid, HistoryEvent cmd resp) -> (Pid, HistoryEvent cmd resp) -> STM () forall a. TChan a -> a -> STM () writeTChan TChan (Pid, HistoryEvent cmd resp) hchan (Pid pid, String -> HistoryEvent cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). String -> HistoryEvent cmd resp Exception String err)) Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a. a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (m :: * -> *) a. Monad m => a -> m a return (Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason) -> Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a b. (a -> b) -> a -> b $ String -> Reason ExceptionThrown String err Right resp Concrete cresp -> do let cvars :: [Dynamic] cvars = resp Concrete -> [Dynamic] forall (f :: (* -> *) -> *). Foldable f => f Concrete -> [Dynamic] getUsedConcrete resp Concrete cresp if [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 /= [Dynamic] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [Dynamic] cvars then do let err :: String err = String -> String -> String -> String -> String mockSemanticsMismatchError (cmd Concrete -> String forall a. Show a => a -> String ppShow cmd Concrete ccmd) ([Var] -> String forall a. Show a => a -> String ppShow [Var] vars) (resp Concrete -> String forall a. Show a => a -> String ppShow resp Concrete cresp) ([Dynamic] -> String forall a. Show a => a -> String ppShow [Dynamic] cvars) STM () -> StateT (Environment, model Symbolic, Counter, model Concrete) m () forall (m :: * -> *) a. MonadIO m => STM a -> m a atomically (TChan (Pid, HistoryEvent cmd resp) -> (Pid, HistoryEvent cmd resp) -> STM () forall a. TChan a -> a -> STM () writeTChan TChan (Pid, HistoryEvent cmd resp) hchan (Pid pid, resp Concrete -> HistoryEvent cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). resp Concrete -> HistoryEvent cmd resp Response resp Concrete cresp)) Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a. a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (m :: * -> *) a. Monad m => a -> m a return (Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason) -> Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a b. (a -> b) -> a -> b $ String -> Reason MockSemanticsMismatch String err else do STM () -> StateT (Environment, model Symbolic, Counter, model Concrete) m () forall (m :: * -> *) a. MonadIO m => STM a -> m a atomically (TChan (Pid, HistoryEvent cmd resp) -> (Pid, HistoryEvent cmd resp) -> STM () forall a. TChan a -> a -> STM () writeTChan TChan (Pid, HistoryEvent cmd resp) hchan (Pid pid, resp Concrete -> HistoryEvent cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). resp Concrete -> HistoryEvent cmd resp Response resp Concrete cresp)) case (Check check, Logic -> Value logic (model Concrete -> cmd Concrete -> resp Concrete -> Logic postcondition model Concrete cmodel cmd Concrete ccmd resp Concrete cresp)) of (Check CheckEverything, VFalse Counterexample ce) -> Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a. a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (m :: * -> *) a. Monad m => a -> m a return (String -> Reason PostconditionFailed (Counterexample -> String forall a. Show a => a -> String show Counterexample ce)) (Check, Value) _otherwise -> case (Check check, Logic -> Value logic ((model Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> model Concrete -> Logic forall a. a -> Maybe a -> a fromMaybe (Logic -> model Concrete -> Logic forall a b. a -> b -> a const Logic Top) Maybe (model Concrete -> Logic) invariant model Concrete cmodel)) of (Check CheckEverything, VFalse Counterexample ce') -> Reason -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason forall a. a -> StateT (Environment, model Symbolic, Counter, model Concrete) m a forall (m :: * -> *) a. Monad m => a -> m a return (String -> Reason InvariantBroken (Counterexample -> String forall a. Show a => a -> String show Counterexample ce')) (Check, Value) _otherwise -> do let (resp Symbolic sresp, Counter counter') = 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 smodel cmd Symbolic scmd) Counter counter (Environment, model Symbolic, Counter, model Concrete) -> StateT (Environment, model Symbolic, Counter, model Concrete) m () forall s (m :: * -> *). MonadState s m => s -> m () put ( [Var] -> [Dynamic] -> Environment -> Environment insertConcretes [Var] vars [Dynamic] cvars Environment env , 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 smodel cmd Symbolic scmd resp Symbolic sresp , Counter counter' , 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 cmodel cmd Concrete ccmd resp Concrete cresp ) [Command cmd resp] -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason go [Command cmd resp] cmds isSomeAsyncException :: SomeException -> Bool isSomeAsyncException :: SomeException -> Bool isSomeAsyncException SomeException se = case SomeException -> Maybe SomeAsyncException forall e. Exception e => SomeException -> Maybe e fromException SomeException se of Just (SomeAsyncException e _) -> Bool True Maybe SomeAsyncException _ -> Bool False mockSemanticsMismatchError :: String -> String -> String -> String -> String mockSemanticsMismatchError :: String -> String -> String -> String -> String mockSemanticsMismatchError String cmd String svars String cresp String cvars = [String] -> String unlines [ String "" , String "Mismatch between `mock` and `semantics`." , String "" , String "The definition of `mock` for the command:" , String "" , String " ", String cmd , String "" , String "returns the following references:" , String "" , String " ", String svars , String "" , String "while the response from `semantics`:" , String "" , String " ", String cresp , String "" , String "returns the following references:" , String "" , String " ", String cvars , String "" , String "Continuing to execute commands at this point could result in scope" , String "errors, because we might have commands that use references (returned" , String "by `mock`) that are not available (returned by `semantics`)." , String "" ] getUsedConcrete :: Rank2.Foldable f => f Concrete -> [Dynamic] getUsedConcrete :: forall (f :: (* -> *) -> *). Foldable f => f Concrete -> [Dynamic] getUsedConcrete = (forall x. Concrete x -> [Dynamic]) -> f Concrete -> [Dynamic] forall m (p :: * -> *). Monoid m => (forall x. p x -> m) -> f p -> m forall k (f :: (k -> *) -> *) m (p :: k -> *). (Foldable f, Monoid m) => (forall (x :: k). p x -> m) -> f p -> m Rank2.foldMap (\(Concrete x x) -> [x -> Dynamic forall a. Typeable a => a -> Dynamic toDyn x x]) modelDiff :: forall model r. CanDiff (model r) => model r -> Maybe (model r) -> Doc PP.AnsiStyle modelDiff :: forall {k} (model :: k -> *) (r :: k). CanDiff (model r) => model r -> Maybe (model r) -> Doc AnsiStyle modelDiff model r model = Proxy (model r) -> ADiff (model r) -> Doc AnsiStyle forall x. CanDiff x => Proxy x -> ADiff x -> Doc AnsiStyle diffToDocCompact Proxy (model r) p (ADiff (model r) -> Doc AnsiStyle) -> (Maybe (model r) -> ADiff (model r)) -> Maybe (model r) -> Doc AnsiStyle forall b c a. (b -> c) -> (a -> b) -> a -> c . (model r -> model r -> ADiff (model r)) -> model r -> model r -> ADiff (model r) forall a b c. (a -> b -> c) -> b -> a -> c flip model r -> model r -> ADiff (model r) forall x. CanDiff x => x -> x -> ADiff x ediff model r model (model r -> ADiff (model r)) -> (Maybe (model r) -> model r) -> Maybe (model r) -> ADiff (model r) forall b c a. (b -> c) -> (a -> b) -> a -> c . model r -> Maybe (model r) -> model r forall a. a -> Maybe a -> a fromMaybe model r model where p :: Proxy (model r) p = forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @(model r) prettyPrintHistory :: forall model cmd m resp. CanDiff (model Concrete) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO () prettyPrintHistory :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO () prettyPrintHistory 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, 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 } = Doc AnsiStyle -> IO () PP.putDoc (Doc AnsiStyle -> IO ()) -> (History cmd resp -> Doc AnsiStyle) -> History cmd resp -> IO () forall b c a. (b -> c) -> (a -> b) -> a -> c . model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc AnsiStyle go model Concrete forall (r :: * -> *). model r initModel Maybe (model Concrete) forall a. Maybe a Nothing ([Operation cmd resp] -> Doc AnsiStyle) -> (History cmd resp -> [Operation cmd resp]) -> History cmd resp -> Doc AnsiStyle forall b c a. (b -> c) -> (a -> b) -> a -> c . History' cmd resp -> [Operation cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> [Operation cmd resp] makeOperations (History' cmd resp -> [Operation cmd resp]) -> (History cmd resp -> History' cmd resp) -> History cmd resp -> [Operation cmd resp] forall b c a. (b -> c) -> (a -> b) -> a -> c . History cmd resp -> History' cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History cmd resp -> History' cmd resp unHistory where go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc PP.AnsiStyle go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc AnsiStyle go model Concrete current Maybe (model Concrete) previous [] = Doc AnsiStyle forall ann. Doc ann PP.line Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> model Concrete -> Maybe (model Concrete) -> Doc AnsiStyle forall {k} (model :: k -> *) (r :: k). CanDiff (model r) => model r -> Maybe (model r) -> Doc AnsiStyle modelDiff model Concrete current Maybe (model Concrete) previous Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> Doc AnsiStyle forall ann. Doc ann PP.line Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> Doc AnsiStyle forall ann. Doc ann PP.line go model Concrete current Maybe (model Concrete) previous [Crash cmd Concrete cmd String err Pid pid] = [Doc AnsiStyle] -> Doc AnsiStyle forall a. Monoid a => [a] -> a mconcat [ Doc AnsiStyle forall ann. Doc ann PP.line , model Concrete -> Maybe (model Concrete) -> Doc AnsiStyle forall {k} (model :: k -> *) (r :: k). CanDiff (model r) => model r -> Maybe (model r) -> Doc AnsiStyle modelDiff model Concrete current Maybe (model Concrete) previous , Doc AnsiStyle forall ann. Doc ann PP.line, 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 String " == " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (cmd Concrete -> String forall a. Show a => a -> String ppShow cmd Concrete cmd) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ==> " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String err , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " [ " , Int -> Doc AnsiStyle forall ann. Int -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (Pid -> Int unPid Pid pid) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ]" , Doc AnsiStyle forall ann. Doc ann PP.line ] go model Concrete current Maybe (model Concrete) previous (Operation cmd Concrete cmd resp Concrete resp Pid pid : [Operation cmd resp] ops) = [Doc AnsiStyle] -> Doc AnsiStyle forall a. Monoid a => [a] -> a mconcat [ Doc AnsiStyle forall ann. Doc ann PP.line , model Concrete -> Maybe (model Concrete) -> Doc AnsiStyle forall {k} (model :: k -> *) (r :: k). CanDiff (model r) => model r -> Maybe (model r) -> Doc AnsiStyle modelDiff model Concrete current Maybe (model Concrete) previous , Doc AnsiStyle forall ann. Doc ann PP.line, 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 String " == " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (cmd Concrete -> String forall a. Show a => a -> String ppShow cmd Concrete cmd) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ==> " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (resp Concrete -> String forall a. Show a => a -> String ppShow resp Concrete resp) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " [ " , Int -> Doc AnsiStyle forall ann. Int -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (Pid -> Int unPid Pid pid) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ]" , Doc AnsiStyle forall ann. Doc ann PP.line , model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc AnsiStyle go (model Concrete -> cmd Concrete -> resp Concrete -> model Concrete forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition model Concrete current cmd Concrete cmd resp Concrete resp) (model Concrete -> Maybe (model Concrete) forall a. a -> Maybe a Just model Concrete current) [Operation cmd resp] ops ] go model Concrete _ Maybe (model Concrete) _ [Operation cmd resp] _ = String -> Doc AnsiStyle forall a. HasCallStack => String -> a error String "prettyPrintHistory: impossible." prettyCommands :: (MonadIO m, CanDiff (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m () prettyCommands :: forall (m :: * -> *) (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). (MonadIO m, CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m () prettyCommands StateMachine model cmd m resp sm History cmd resp hist Property prop = StateMachine model cmd m resp -> History cmd resp -> IO () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO () prettyPrintHistory StateMachine model cmd m resp sm History cmd resp hist IO () -> Property -> PropertyM m () forall (m :: * -> *). Monad m => IO () -> Property -> PropertyM m () `whenFailM` Property prop prettyPrintHistory' :: forall model cmd m resp tag. CanDiff (model Concrete) => (Show (cmd Concrete), Show (resp Concrete), CanDiff [tag]) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> IO () prettyPrintHistory' :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *) tag. (CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete), CanDiff [tag]) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> IO () prettyPrintHistory' 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, 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 } [Event model cmd resp Symbolic] -> [tag] tag Commands cmd resp cmds = Doc AnsiStyle -> IO () PP.putDoc (Doc AnsiStyle -> IO ()) -> (History cmd resp -> Doc AnsiStyle) -> History cmd resp -> IO () forall b c a. (b -> c) -> (a -> b) -> a -> c . model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]] -> [Operation cmd resp] -> Doc AnsiStyle go model Concrete forall (r :: * -> *). model r initModel Maybe (model Concrete) forall a. Maybe a Nothing [] (([Event model cmd resp Symbolic] -> [tag]) -> [[Event model cmd resp Symbolic]] -> [[tag]] forall a b. (a -> b) -> [a] -> [b] map [Event model cmd resp Symbolic] -> [tag] tag (Int -> [[Event model cmd resp Symbolic]] -> [[Event model cmd resp Symbolic]] forall a. Int -> [a] -> [a] drop Int 1 ([Event model cmd resp Symbolic] -> [[Event model cmd resp Symbolic]] forall a. [a] -> [[a]] inits (StateMachine model cmd m resp -> Commands cmd resp -> [Event model cmd resp Symbolic] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> Commands cmd resp -> [Event model cmd resp Symbolic] execCmds StateMachine model cmd m resp sm Commands cmd resp cmds)))) ([Operation cmd resp] -> Doc AnsiStyle) -> (History cmd resp -> [Operation cmd resp]) -> History cmd resp -> Doc AnsiStyle forall b c a. (b -> c) -> (a -> b) -> a -> c . History' cmd resp -> [Operation cmd resp] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History' cmd resp -> [Operation cmd resp] makeOperations (History' cmd resp -> [Operation cmd resp]) -> (History cmd resp -> History' cmd resp) -> History cmd resp -> [Operation cmd resp] forall b c a. (b -> c) -> (a -> b) -> a -> c . History cmd resp -> History' cmd resp forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). History cmd resp -> History' cmd resp unHistory where tagsDiff :: [tag] -> [tag] -> Doc PP.AnsiStyle tagsDiff :: [tag] -> [tag] -> Doc AnsiStyle tagsDiff [tag] old [tag] new = Proxy [tag] -> ADiff [tag] -> Doc AnsiStyle forall x. CanDiff x => Proxy x -> ADiff x -> Doc AnsiStyle diffToDocCompact (forall t. Proxy t forall {k} (t :: k). Proxy t Proxy @[tag]) ([tag] -> [tag] -> ADiff [tag] forall x. CanDiff x => x -> x -> ADiff x ediff [tag] old [tag] new) go :: model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]] -> [Operation cmd resp] -> Doc PP.AnsiStyle go :: model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]] -> [Operation cmd resp] -> Doc AnsiStyle go model Concrete current Maybe (model Concrete) previous [tag] _seen [[tag]] _tags [] = Doc AnsiStyle forall ann. Doc ann PP.line Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> model Concrete -> Maybe (model Concrete) -> Doc AnsiStyle forall {k} (model :: k -> *) (r :: k). CanDiff (model r) => model r -> Maybe (model r) -> Doc AnsiStyle modelDiff model Concrete current Maybe (model Concrete) previous Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> Doc AnsiStyle forall ann. Doc ann PP.line Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> Doc AnsiStyle forall ann. Doc ann PP.line go model Concrete current Maybe (model Concrete) previous [tag] seen ([tag] tags : [[tag]] _) [Crash cmd Concrete cmd String err Pid pid] = [Doc AnsiStyle] -> Doc AnsiStyle forall a. Monoid a => [a] -> a mconcat [ Doc AnsiStyle forall ann. Doc ann PP.line , model Concrete -> Maybe (model Concrete) -> Doc AnsiStyle forall {k} (model :: k -> *) (r :: k). CanDiff (model r) => model r -> Maybe (model r) -> Doc AnsiStyle modelDiff model Concrete current Maybe (model Concrete) previous , Doc AnsiStyle forall ann. Doc ann PP.line, 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 String " == " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (cmd Concrete -> String forall a. Show a => a -> String ppShow cmd Concrete cmd) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ==> " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String err , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " [ " , Int -> Doc AnsiStyle forall ann. Int -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (Pid -> Int unPid Pid pid) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ]" , Doc AnsiStyle forall ann. Doc ann PP.line , if Bool -> Bool not ([tag] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [tag] tags) then Doc AnsiStyle forall ann. Doc ann PP.line Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> [tag] -> [tag] -> Doc AnsiStyle tagsDiff [tag] seen [tag] tags Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> Doc AnsiStyle forall ann. Doc ann PP.line else Doc AnsiStyle forall ann. Doc ann PP.emptyDoc ] go model Concrete current Maybe (model Concrete) previous [tag] seen ([tag] tags : [[tag]] tagss) (Operation cmd Concrete cmd resp Concrete resp Pid pid : [Operation cmd resp] ops) = [Doc AnsiStyle] -> Doc AnsiStyle forall a. Monoid a => [a] -> a mconcat [ Doc AnsiStyle forall ann. Doc ann PP.line , model Concrete -> Maybe (model Concrete) -> Doc AnsiStyle forall {k} (model :: k -> *) (r :: k). CanDiff (model r) => model r -> Maybe (model r) -> Doc AnsiStyle modelDiff model Concrete current Maybe (model Concrete) previous , Doc AnsiStyle forall ann. Doc ann PP.line, 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 String " == " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (cmd Concrete -> String forall a. Show a => a -> String ppShow cmd Concrete cmd) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ==> " , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (resp Concrete -> String forall a. Show a => a -> String ppShow resp Concrete resp) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " [ " , Int -> Doc AnsiStyle forall ann. Int -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty (Pid -> Int unPid Pid pid) , String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " ]" , Doc AnsiStyle forall ann. Doc ann PP.line , if Bool -> Bool not ([tag] -> Bool forall a. [a] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [tag] tags) then Doc AnsiStyle forall ann. Doc ann PP.line Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> String -> Doc AnsiStyle forall ann. String -> Doc ann forall a ann. Pretty a => a -> Doc ann PP.pretty String " " Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> [tag] -> [tag] -> Doc AnsiStyle tagsDiff [tag] seen [tag] tags Doc AnsiStyle -> Doc AnsiStyle -> Doc AnsiStyle forall a. Semigroup a => a -> a -> a <> Doc AnsiStyle forall ann. Doc ann PP.line else Doc AnsiStyle forall ann. Doc ann PP.emptyDoc , model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]] -> [Operation cmd resp] -> Doc AnsiStyle go (model Concrete -> cmd Concrete -> resp Concrete -> model Concrete forall (r :: * -> *). (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r transition model Concrete current cmd Concrete cmd resp Concrete resp) (model Concrete -> Maybe (model Concrete) forall a. a -> Maybe a Just model Concrete current) [tag] tags [[tag]] tagss [Operation cmd resp] ops ] go model Concrete _ Maybe (model Concrete) _ [tag] _ [[tag]] _ [Operation cmd resp] _ = String -> Doc AnsiStyle forall a. HasCallStack => String -> a error String "prettyPrintHistory': impossible." -- | Variant of 'prettyCommands' that also prints the @tag@s covered by each -- command. prettyCommands' :: (MonadIO m, CanDiff (model Concrete), CanDiff [tag]) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> Property -> PropertyM m () prettyCommands' :: forall (m :: * -> *) (model :: (* -> *) -> *) tag (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). (MonadIO m, CanDiff (model Concrete), CanDiff [tag], Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> Property -> PropertyM m () prettyCommands' StateMachine model cmd m resp sm [Event model cmd resp Symbolic] -> [tag] tag Commands cmd resp cmds History cmd resp hist Property prop = StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> IO () forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *) tag. (CanDiff (model Concrete), Show (cmd Concrete), Show (resp Concrete), CanDiff [tag]) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> IO () prettyPrintHistory' StateMachine model cmd m resp sm [Event model cmd resp Symbolic] -> [tag] tag Commands cmd resp cmds History cmd resp hist IO () -> Property -> PropertyM m () forall (m :: * -> *). Monad m => IO () -> Property -> PropertyM m () `whenFailM` Property prop saveCommands :: (Show (cmd Symbolic), Show (resp Symbolic)) => FilePath -> Commands cmd resp -> Property -> Property saveCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). (Show (cmd Symbolic), Show (resp Symbolic)) => String -> Commands cmd resp -> Property -> Property saveCommands String dir Commands cmd resp cmds Property prop = IO () go IO () -> Property -> Property forall prop. Testable prop => IO () -> prop -> Property `whenFail` Property prop where go :: IO () go :: IO () go = do Bool -> String -> IO () createDirectoryIfMissing Bool True String dir String file <- TimeLocale -> String -> ZonedTime -> String forall t. FormatTime t => TimeLocale -> String -> t -> String formatTime TimeLocale defaultTimeLocale String "%F_%T" (ZonedTime -> String) -> IO ZonedTime -> IO String forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> IO ZonedTime getZonedTime let fp :: String fp = String dir String -> String -> String </> String file String -> String -> IO () writeFile String fp (Commands cmd resp -> String forall a. Show a => a -> String ppShow Commands cmd resp cmds) String -> IO () putStrLn (String "Saved counterexample in: " String -> String -> String forall a. [a] -> [a] -> [a] ++ String fp) String -> IO () putStrLn String "" runSavedCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => (MonadMask m, MonadIO m) => (Read (cmd Symbolic), Read (resp Symbolic)) => StateMachine model cmd m resp -> FilePath -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason) runSavedCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m, Read (cmd Symbolic), Read (resp Symbolic)) => StateMachine model cmd m resp -> String -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason) runSavedCommands StateMachine model cmd m resp sm String fp = do Commands cmd resp cmds <- String -> Commands cmd resp forall a. Read a => String -> a read (String -> Commands cmd resp) -> PropertyM m String -> PropertyM m (Commands cmd resp) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> IO String -> PropertyM m String forall a. IO a -> PropertyM m a forall (m :: * -> *) a. MonadIO m => IO a -> m a liftIO (String -> IO String readFile String fp) (History cmd resp hist, model Concrete model, Reason res) <- StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *) (model :: (* -> *) -> *). (Show (cmd Concrete), Show (resp Concrete), Traversable cmd, Foldable resp, MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason) runCommands StateMachine model cmd m resp sm Commands cmd resp cmds (Commands cmd resp, History cmd resp, model Concrete, Reason) -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason) forall a. a -> PropertyM m a forall (m :: * -> *) a. Monad m => a -> m a return (Commands cmd resp cmds, History cmd resp hist, model Concrete model, Reason res) ------------------------------------------------------------------------ -- | Print the percentage of each command used. The prefix check is -- an unfortunate remaining for backwards compatibility. checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property checkCommandNames :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> Property -> Property checkCommandNames Commands cmd resp cmds = String -> [String] -> Property -> Property forall prop. Testable prop => String -> [String] -> prop -> Property tabulate String "Commands" ((String, Int) -> String forall a b. (a, b) -> a fst ((String, Int) -> String) -> [(String, Int)] -> [String] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Commands cmd resp -> [(String, Int)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> [(String, Int)] commandNames Commands cmd resp cmds) -- | Fail if some commands have not been executed. coverCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property coverCommandNames :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> Property -> Property coverCommandNames Commands cmd resp cmds = Double -> Bool -> String -> Property -> Property forall prop. Testable prop => Double -> Bool -> String -> prop -> Property cover Double 1 ([(String, Int)] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [(String, Int)] names Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int numOfConstructors) String "coverage" where names :: [(String, Int)] names = Commands cmd resp -> [(String, Int)] forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> [(String, Int)] commandNames Commands cmd resp cmds numOfConstructors :: Int numOfConstructors = [String] -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length (Proxy (cmd Symbolic) -> [String] forall k (cmd :: k -> *) (r :: k). CommandNames cmd => Proxy (cmd r) -> [String] forall (r :: * -> *). Proxy (cmd r) -> [String] cmdNames (Proxy (cmd Symbolic) forall {k} (t :: k). Proxy t Proxy :: Proxy (cmd Symbolic))) commandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [(String, Int)] commandNames :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> [(String, Int)] commandNames = Map String Int -> [(String, Int)] forall k a. Map k a -> [(k, a)] M.toList (Map String Int -> [(String, Int)]) -> (Commands cmd resp -> Map String Int) -> Commands cmd resp -> [(String, Int)] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Map String Int -> Command cmd resp -> Map String Int) -> Map String Int -> [Command cmd resp] -> Map String Int forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl Map String Int -> Command cmd resp -> Map String Int go Map String Int forall k a. Map k a M.empty ([Command cmd resp] -> Map String Int) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> Map String Int 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 :: Map String Int -> Command cmd resp -> Map String Int go :: Map String Int -> Command cmd resp -> Map String Int go Map String Int ih Command cmd resp cmd = (Int -> Int -> Int) -> String -> Int -> Map String Int -> Map String Int forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a M.insertWith Int -> Int -> Int forall a. Num a => a -> a -> a (+) (Command cmd resp -> String forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Command cmd resp -> String commandName Command cmd resp cmd) Int 1 Map String Int ih commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String] commandNamesInOrder :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Commands cmd resp -> [String] commandNamesInOrder = [String] -> [String] forall a. [a] -> [a] reverse ([String] -> [String]) -> (Commands cmd resp -> [String]) -> Commands cmd resp -> [String] forall b c a. (b -> c) -> (a -> b) -> a -> c . ([String] -> Command cmd resp -> [String]) -> [String] -> [Command cmd resp] -> [String] forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl [String] -> Command cmd resp -> [String] go [] ([Command cmd resp] -> [String]) -> (Commands cmd resp -> [Command cmd resp]) -> Commands cmd resp -> [String] 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 :: [String] -> Command cmd resp -> [String] go :: [String] -> Command cmd resp -> [String] go [String] ih Command cmd resp cmd = Command cmd resp -> String forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *). CommandNames cmd => Command cmd resp -> String commandName Command cmd resp cmd String -> [String] -> [String] forall a. a -> [a] -> [a] : [String] ih ------------------------------------------------------------------------ -- | Show minimal examples for each of the generated tags. showLabelledExamples' :: (Show tag, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> Maybe Int -- ^ Seed -> Int -- ^ Number of tests to run to find examples -> ([Event model cmd resp Symbolic] -> [tag]) -> (tag -> Bool) -- ^ Tag filter (can be @const True@) -> IO () showLabelledExamples' :: forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *). (Show tag, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> Int -> ([Event model cmd resp Symbolic] -> [tag]) -> (tag -> Bool) -> IO () showLabelledExamples' StateMachine model cmd m resp sm Maybe Int mReplay Int numTests [Event model cmd resp Symbolic] -> [tag] tag tag -> Bool focus = do Int replaySeed <- case Maybe Int mReplay of Maybe Int Nothing -> (StdGen -> (Int, StdGen)) -> IO Int forall (m :: * -> *) a. MonadIO m => (StdGen -> (a, StdGen)) -> m a getStdRandom ((Int, Int) -> StdGen -> (Int, StdGen) forall g. RandomGen g => (Int, Int) -> g -> (Int, g) forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g) randomR (Int 1, Int 999999)) Just Int seed -> Int -> IO Int forall a. a -> IO a forall (m :: * -> *) a. Monad m => a -> m a return Int seed Args -> Property -> IO () forall prop. Testable prop => Args -> prop -> IO () labelledExamplesWith (Args stdArgs { replay = Just (mkQCGen replaySeed, 0) , maxSuccess = numTests }) (Property -> IO ()) -> Property -> IO () forall a b. (a -> b) -> a -> b $ Gen (Commands cmd resp) -> (Commands cmd resp -> [Commands cmd resp]) -> (Commands cmd resp -> String) -> (Commands 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 (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) (StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp] shrinkCommands StateMachine model cmd m resp sm) Commands cmd resp -> String forall a. Show a => a -> String ppShow ((Commands cmd resp -> Property) -> Property) -> (Commands cmd resp -> Property) -> Property forall a b. (a -> b) -> a -> b $ \Commands cmd resp cmds -> [tag] -> Property -> Property forall a. Show a => [a] -> Property -> Property collects ((tag -> Bool) -> [tag] -> [tag] forall a. (a -> Bool) -> [a] -> [a] filter tag -> Bool focus ([tag] -> [tag]) -> (Commands cmd resp -> [tag]) -> Commands cmd resp -> [tag] forall b c a. (b -> c) -> (a -> b) -> a -> c . [Event model cmd resp Symbolic] -> [tag] tag ([Event model cmd resp Symbolic] -> [tag]) -> (Commands cmd resp -> [Event model cmd resp Symbolic]) -> Commands cmd resp -> [tag] forall b c a. (b -> c) -> (a -> b) -> a -> c . StateMachine model cmd m resp -> Commands cmd resp -> [Event model cmd resp Symbolic] forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (m :: * -> *) (resp :: (* -> *) -> *). StateMachine model cmd m resp -> Commands cmd resp -> [Event model cmd resp Symbolic] execCmds StateMachine model cmd m resp sm (Commands cmd resp -> [tag]) -> Commands cmd resp -> [tag] forall a b. (a -> b) -> a -> b $ Commands cmd resp cmds) (Property -> Property) -> Property -> Property forall a b. (a -> b) -> a -> b $ Bool -> Property forall prop. Testable prop => prop -> Property property Bool True String -> IO () putStrLn (String -> IO ()) -> String -> IO () forall a b. (a -> b) -> a -> b $ String "Used replaySeed " String -> String -> String forall a. [a] -> [a] -> [a] ++ Int -> String forall a. Show a => a -> String show Int replaySeed showLabelledExamples :: (Show tag, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => (Rank2.Traversable cmd, Rank2.Foldable resp) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> IO () showLabelledExamples :: forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *). (Show tag, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> IO () showLabelledExamples StateMachine model cmd m resp sm [Event model cmd resp Symbolic] -> [tag] tag = StateMachine model cmd m resp -> Maybe Int -> Int -> ([Event model cmd resp Symbolic] -> [tag]) -> (tag -> Bool) -> IO () forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *). (Show tag, Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic), Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> Int -> ([Event model cmd resp Symbolic] -> [tag]) -> (tag -> Bool) -> IO () showLabelledExamples' StateMachine model cmd m resp sm Maybe Int forall a. Maybe a Nothing Int 1000 [Event model cmd resp Symbolic] -> [tag] tag (Bool -> tag -> Bool forall a b. a -> b -> a const Bool True)