{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
module Test.StateMachine.Sequential
( forAllCommands
, existsCommands
, generateCommands
, generateCommandsState
, deadlockError
, getUsedVars
, shrinkCommands
, shrinkAndValidate
, ValidateEnv(..)
, ShouldShrink(..)
, initValidateEnv
, runCommands
, runCommandsWithSetup
, runCommands'
, getChanContents
, Check(..)
, executeCommands
, prettyPrintHistory
, prettyPrintHistory'
, prettyCommands
, prettyCommands'
, saveCommands
, runSavedCommands
, commandNames
, commandNamesInOrder
, coverCommandNames
, checkCommandNames
, showLabelledExamples
, showLabelledExamples'
)
where
import Control.Exception
(SomeException, SomeAsyncException (..), displayException,
fromException)
import Control.Monad (when)
import Control.Monad.Catch
(MonadCatch(..), MonadMask (..), catch, ExitCase (..))
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 Data.TreeDiff
(ToExpr, ansiWlBgEditExprCompact, ediff)
import Prelude
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.PrettyPrint.ANSI.Leijen
(Doc)
import qualified Text.PrettyPrint.ANSI.Leijen as PP
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.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
-> (Commands cmd resp -> prop)
-> 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 =
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (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) (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) forall a. Show a => a -> String
ppShow
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)]
-> (Commands cmd resp -> prop)
-> 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 (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel, 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 -> Gen (cmd Symbolic)]
gens0 =
forall prop. Testable prop => prop -> Property
once forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (r :: * -> *). model r
initModel Counter
newCounter []) (forall a b. a -> b -> a
const []) 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (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 <- forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
ppShow) forall a. a -> a
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
model Symbolic -> Gen (cmd Symbolic)
gen model Symbolic
model forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
`suchThatEither` (Logic -> Bool
boolean 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') = 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 (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'
(forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
Command cmd Symbolic
cmd resp Symbolic
resp (forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars resp Symbolic
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 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ 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
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
ppShow model Symbolic
model
, String
"\n\nThe following commands have been generated so far:\n\n"
, String
" " forall a. [a] -> [a] -> [a]
++ 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
" " 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
-> 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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } Maybe Int
mminSize =
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (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) 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
-> 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 :: model Symbolic -> cmd Symbolic -> Logic
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition, model Symbolic -> Maybe (Gen (cmd Symbolic))
generator :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Maybe (Gen (cmd Symbolic))
generator :: model Symbolic -> Maybe (Gen (cmd Symbolic))
generator, 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 } Counter
counter0 Maybe Int
mminSize = do
let minSize :: Int
minSize = forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
mminSize
Int
size0 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> forall a. Random a => (a, a) -> Gen a
choose (Int
minSize, Int
k 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 = forall (m :: * -> *) a. Monad m => a -> m a
return (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (forall a. [a] -> [a]
reverse [Command cmd resp]
cmds))
go Int
size Counter
counter [Command cmd resp]
cmds = do
model Symbolic
model <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (forall a. [a] -> [a]
reverse [Command cmd resp]
cmds))
Just Gen (cmd Symbolic)
gen -> do
Either [cmd Symbolic] (cmd Symbolic)
enext <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Gen (cmd Symbolic)
gen forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
`suchThatEither` (Logic -> Bool
boolean 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 -> 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 (forall a. [a] -> [a]
reverse [Command cmd resp]
cmds) (forall a. Show a => a -> String
ppShow [cmd Symbolic]
ces)
Right cmd Symbolic
next -> do
let (resp Symbolic
resp, Counter
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
forall s (m :: * -> *). MonadState s m => s -> m ()
put (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 forall a. Num a => a -> a -> a
- Int
1) Counter
counter' (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
Command cmd Symbolic
next resp Symbolic
resp (forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars resp Symbolic
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 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])
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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } =
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk [Command cmd resp] -> [Commands cmd resp]
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [Shrunk [a]]
shrinkListS' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
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) = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$
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)
(forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv forall (r :: * -> *). model r
initModel)
(forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
cmds)
data ValidateEnv model = ValidateEnv {
forall (model :: (* -> *) -> *).
ValidateEnv model -> model Symbolic
veModel :: model Symbolic
, forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope :: Map Var Var
, 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 = forall k a. Map k a
M.empty
, veCounter :: Counter
veCounter = Counter
newCounter
}
data ShouldShrink = MustShrink | DontShrink
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 :: 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 -> cmd Symbolic -> [cmd Symbolic]
shrinker :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> [cmd Symbolic]
shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
shrinker } =
\ShouldShrink
env ValidateEnv model
shouldShrink Commands cmd resp
cmds -> forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands) forall a b. (a -> b) -> a -> b
$ ShouldShrink
-> ValidateEnv model
-> [Command cmd resp]
-> [(ValidateEnv model, [Command cmd resp])]
go ShouldShrink
env ValidateEnv model
shouldShrink (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
_ [] = []
go ShouldShrink
DontShrink ValidateEnv model
env [] = [(ValidateEnv model
env, [])]
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 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)
Rank2.traverse (forall a. Map Var Var -> Symbolic a -> Maybe (Symbolic a)
remapVars Map Var Var
scope) cmd Symbolic
cmd' of
Just cmd Symbolic
remapped ->
let candidates :: [(ShouldShrink, cmd Symbolic)]
candidates :: [(ShouldShrink, cmd Symbolic)]
candidates =
case ShouldShrink
shouldShrink of
ShouldShrink
DontShrink -> [(ShouldShrink
DontShrink, cmd Symbolic
remapped)]
ShouldShrink
MustShrink -> forall a b. (a -> b) -> [a] -> [b]
map (ShouldShrink
DontShrink,) (model Symbolic -> cmd Symbolic -> [cmd Symbolic]
shrinker model Symbolic
model cmd Symbolic
remapped)
forall a. [a] -> [a] -> [a]
++ [(ShouldShrink
MustShrink, cmd Symbolic
remapped)]
in forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [(ShouldShrink, cmd Symbolic)]
candidates 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') = 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 = forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars resp Symbolic
resp
env' :: ValidateEnv model
env' = ValidateEnv {
veModel :: model Symbolic
veModel = 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 = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars' [Var]
vars) 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 forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
Command cmd Symbolic
cmd resp Symbolic
resp [Var]
varsforall a. a -> [a] -> [a]
:)) 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) = forall a. Typeable a => Var -> Symbolic a
Symbolic forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
Foldable resp, MonadMask m, MonadIO m) =>
m (StateMachine model cmd m resp)
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommandsWithSetup (forall (f :: * -> *) a. Applicative f => a -> f a
pure StateMachine model cmd m resp
sm)
runCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadIO m)
=> m (StateMachine model cmd m resp)
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommandsWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
Foldable resp, MonadMask m, MonadIO m) =>
m (StateMachine model cmd m resp)
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommandsWithSetup m (StateMachine model cmd m resp)
msm Commands cmd resp
cmds = forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall a b. (a -> b) -> a -> b
$ forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
Foldable resp, MonadMask m, MonadIO m) =>
m (StateMachine model cmd m resp)
-> Commands cmd resp
-> m (History cmd resp, model Concrete, Reason)
runCommands' m (StateMachine model cmd m resp)
msm Commands cmd resp
cmds
runCommands' :: (Show (cmd Concrete), Show (resp Concrete))
=> (Rank2.Traversable cmd, Rank2.Foldable resp)
=> (MonadMask m, MonadIO m)
=> 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) =>
m (StateMachine model cmd m resp)
-> Commands cmd resp
-> m (History cmd resp, model Concrete, Reason)
runCommands' m (StateMachine model cmd m resp)
msm Commands cmd resp
cmds = do
TChan (Pid, HistoryEvent cmd resp)
hchan <- forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
(Reason
reason, (Environment
_, model Symbolic
_, Counter
_, model Concrete
model)) <-
forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
MonadMask m =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
m (StateMachine model cmd m resp)
msm
(\StateMachine model cmd m resp
sm' ExitCase
(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)) -> forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
ExitCase
(Reason, (Environment, model Symbolic, Counter, model Concrete))
_ -> forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
)
(\sm' :: StateMachine model cmd m resp
sm'@StateMachine{ forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } -> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
(Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm' TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
0) Check
CheckEverything Commands cmd resp
cmds)
(Environment
emptyEnvironment, forall (r :: * -> *). model r
initModel, Counter
newCounter, forall (r :: * -> *). model r
initModel))
[(Pid, HistoryEvent cmd resp)]
hist <- forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
forall (m :: * -> *) a. Monad m => a -> m a
return (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
model, Reason
reason)
getChanContents :: MonadIO m => TChan a -> m [a]
getChanContents :: forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan a
chan = forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- 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 forall a. a -> [a] -> [a]
: [a]
acc)
Maybe a
Nothing -> 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
semantics :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete)
invariant :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> Maybe (model Concrete -> Logic)
postcondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Concrete -> cmd Concrete -> resp Concrete -> Logic
cleanup :: model Concrete -> m ()
mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
semantics :: cmd Concrete -> m (resp Concrete)
shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
generator :: model Symbolic -> Maybe (Gen (cmd Symbolic))
invariant :: Maybe (model Concrete -> Logic)
postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
precondition :: model Symbolic -> cmd Symbolic -> Logic
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
initModel :: forall (r :: * -> *). model r
cleanup :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
shrinker :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> [cmd Symbolic]
generator :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Maybe (Gen (cmd Symbolic))
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
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
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
..} TChan (Pid, HistoryEvent cmd resp)
hchan Pid
pid Check
check =
forall {t :: (* -> *) -> * -> *} {resp :: (* -> *) -> *}.
(MonadState
(Environment, model Symbolic, Counter, model Concrete) (t m),
MonadTrans t, MonadIO (t m)) =>
[Command cmd resp] -> t m Reason
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
where
go :: [Command cmd resp] -> t m Reason
go [] = 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) <- 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
PreconditionFailed (forall a. Show a => a -> String
show Counterexample
ce))
(Check
CheckEverything, VFalse Counterexample
ce) -> forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
PreconditionFailed (forall a. Show a => a -> String
show Counterexample
ce))
(Check, Value)
_otherwise -> do
let ccmd :: cmd Concrete
ccmd = forall b a. b -> Either a b -> b
fromRight (forall a. HasCallStack => String -> a
error String
"executeCommands: impossible") (forall (t :: (* -> *) -> *).
Traversable t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
env cmd Symbolic
scmd)
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Concrete -> Set Var -> HistoryEvent cmd resp
Invocation cmd Concrete
ccmd (forall a. Ord a => [a] -> Set a
S.fromList [Var]
vars)))
!Either String (resp Concrete)
ecresp <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> Either a b
Right (cmd Concrete -> m (resp Concrete)
semantics cmd Concrete
ccmd) forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`catch`
\(SomeException
err :: SomeException) -> do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SomeException -> Bool
isSomeAsyncException SomeException
err) (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall e. Exception e => e -> String
displayException SomeException
err) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) e a. (MonadIO m, Exception e) => e -> m a
throwIO SomeException
err)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left (forall e. Exception e => e -> String
displayException SomeException
err))
case Either String (resp Concrete)
ecresp of
Left String
err -> do
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
String -> HistoryEvent cmd resp
Exception String
err))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Reason
ExceptionThrown String
err
Right resp Concrete
cresp -> do
let cvars :: [Dynamic]
cvars = forall (f :: (* -> *) -> *). Foldable f => f Concrete -> [Dynamic]
getUsedConcrete resp Concrete
cresp
if forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vars forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dynamic]
cvars
then do
let err :: String
err = String -> String -> String -> String -> String
mockSemanticsMismatchError (forall a. Show a => a -> String
ppShow cmd Concrete
ccmd) (forall a. Show a => a -> String
ppShow [Var]
vars) (forall a. Show a => a -> String
ppShow resp Concrete
cresp) (forall a. Show a => a -> String
ppShow [Dynamic]
cvars)
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
resp Concrete -> HistoryEvent cmd resp
Response resp Concrete
cresp))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> Reason
MockSemanticsMismatch String
err
else do
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
PostconditionFailed (forall a. Show a => a -> String
show Counterexample
ce))
(Check, Value)
_otherwise ->
case (Check
check, Logic -> Value
logic (forall a. a -> Maybe a -> a
fromMaybe (forall a b. a -> b -> a
const Logic
Top) Maybe (model Concrete -> Logic)
invariant model Concrete
cmodel)) of
(Check
CheckEverything, VFalse Counterexample
ce') -> forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
InvariantBroken (forall a. Show a => a -> String
show Counterexample
ce'))
(Check, Value)
_otherwise -> do
let (resp Symbolic
sresp, Counter
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
forall s (m :: * -> *). MonadState s m => s -> m ()
put ( [Var] -> [Dynamic] -> Environment -> Environment
insertConcretes [Var]
vars [Dynamic]
cvars Environment
env
, 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'
, 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] -> t m Reason
go [Command cmd resp]
cmds
isSomeAsyncException :: SomeException -> Bool
isSomeAsyncException :: SomeException -> Bool
isSomeAsyncException SomeException
se = case 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 k (f :: (k -> *) -> *) m (p :: k -> *).
(Foldable f, Monoid m) =>
(forall (x :: k). p x -> m) -> f p -> m
Rank2.foldMap (\(Concrete x
x) -> [forall a. Typeable a => a -> Dynamic
toDyn x
x])
modelDiff :: ToExpr (model r) => model r -> Maybe (model r) -> Doc
modelDiff :: forall {k} (model :: k -> *) (r :: k).
ToExpr (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model r
model = Edit EditExpr -> Doc
ansiWlBgEditExprCompact forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. ToExpr a => a -> a -> Edit EditExpr
ediff model r
model forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe model r
model
prettyPrintHistory :: forall model cmd m resp. ToExpr (model Concrete)
=> (Show (cmd Concrete), Show (resp Concrete))
=> StateMachine model cmd m resp
-> History cmd resp
-> IO ()
prettyPrintHistory :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(ToExpr (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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel, 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 }
= Doc -> IO ()
PP.putDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model Concrete
-> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
go forall (r :: * -> *). model r
initModel forall a. Maybe a
Nothing
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [Operation cmd resp]
makeOperations
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
where
go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
go :: model Concrete
-> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
go model Concrete
current Maybe (model Concrete)
previous [] =
Doc
PP.line forall a. Semigroup a => a -> a -> a
<> forall {k} (model :: k -> *) (r :: k).
ToExpr (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous forall a. Semigroup a => a -> a -> a
<> Doc
PP.line forall a. Semigroup a => a -> a -> a
<> Doc
PP.line
go model Concrete
current Maybe (model Concrete)
previous [Crash cmd Concrete
cmd String
err Pid
pid] =
forall a. Monoid a => [a] -> a
mconcat
[ Doc
PP.line
, forall {k} (model :: k -> *) (r :: k).
ToExpr (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous
, Doc
PP.line, Doc
PP.line
, String -> Doc
PP.string String
" == "
, String -> Doc
PP.string (forall a. Show a => a -> String
ppShow cmd Concrete
cmd)
, String -> Doc
PP.string String
" ==> "
, String -> Doc
PP.string String
err
, String -> Doc
PP.string String
" [ "
, Int -> Doc
PP.int (Pid -> Int
unPid Pid
pid)
, String -> Doc
PP.string String
" ]"
, Doc
PP.line
]
go model Concrete
current Maybe (model Concrete)
previous (Operation cmd Concrete
cmd resp Concrete
resp Pid
pid : [Operation cmd resp]
ops) =
forall a. Monoid a => [a] -> a
mconcat
[ Doc
PP.line
, forall {k} (model :: k -> *) (r :: k).
ToExpr (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous
, Doc
PP.line, Doc
PP.line
, String -> Doc
PP.string String
" == "
, String -> Doc
PP.string (forall a. Show a => a -> String
ppShow cmd Concrete
cmd)
, String -> Doc
PP.string String
" ==> "
, String -> Doc
PP.string (forall a. Show a => a -> String
ppShow resp Concrete
resp)
, String -> Doc
PP.string String
" [ "
, Int -> Doc
PP.int (Pid -> Int
unPid Pid
pid)
, String -> Doc
PP.string String
" ]"
, Doc
PP.line
, model Concrete
-> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
go (forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
current cmd Concrete
cmd resp Concrete
resp) (forall a. a -> Maybe a
Just model Concrete
current) [Operation cmd resp]
ops
]
go model Concrete
_ Maybe (model Concrete)
_ [Operation cmd resp]
_ = forall a. HasCallStack => String -> a
error String
"prettyPrintHistory: impossible."
prettyCommands :: (MonadIO m, ToExpr (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, ToExpr (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 = forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(ToExpr (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 forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` Property
prop
prettyPrintHistory' :: forall model cmd m resp tag. ToExpr (model Concrete)
=> (Show (cmd Concrete), Show (resp Concrete), ToExpr 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.
(ToExpr (model Concrete), Show (cmd Concrete),
Show (resp Concrete), ToExpr 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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel, 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 } [Event model cmd resp Symbolic] -> [tag]
tag Commands cmd resp
cmds
= Doc -> IO ()
PP.putDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model Concrete
-> Maybe (model Concrete)
-> [tag]
-> [[tag]]
-> [Operation cmd resp]
-> Doc
go forall (r :: * -> *). model r
initModel forall a. Maybe a
Nothing [] (forall a b. (a -> b) -> [a] -> [b]
map [Event model cmd resp Symbolic] -> [tag]
tag (forall a. Int -> [a] -> [a]
drop Int
1 (forall a. [a] -> [[a]]
inits (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))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [Operation cmd resp]
makeOperations
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
where
tagsDiff :: [tag] -> [tag] -> Doc
tagsDiff :: [tag] -> [tag] -> Doc
tagsDiff [tag]
old [tag]
new = Edit EditExpr -> Doc
ansiWlBgEditExprCompact (forall a. ToExpr a => a -> a -> Edit EditExpr
ediff [tag]
old [tag]
new)
go :: model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]]
-> [Operation cmd resp] -> Doc
go :: model Concrete
-> Maybe (model Concrete)
-> [tag]
-> [[tag]]
-> [Operation cmd resp]
-> Doc
go model Concrete
current Maybe (model Concrete)
previous [tag]
_seen [[tag]]
_tags [] =
Doc
PP.line forall a. Semigroup a => a -> a -> a
<> forall {k} (model :: k -> *) (r :: k).
ToExpr (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous forall a. Semigroup a => a -> a -> a
<> Doc
PP.line forall a. Semigroup a => a -> a -> a
<> Doc
PP.line
go model Concrete
current Maybe (model Concrete)
previous [tag]
seen ([tag]
tags : [[tag]]
_) [Crash cmd Concrete
cmd String
err Pid
pid] =
forall a. Monoid a => [a] -> a
mconcat
[ Doc
PP.line
, forall {k} (model :: k -> *) (r :: k).
ToExpr (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous
, Doc
PP.line, Doc
PP.line
, String -> Doc
PP.string String
" == "
, String -> Doc
PP.string (forall a. Show a => a -> String
ppShow cmd Concrete
cmd)
, String -> Doc
PP.string String
" ==> "
, String -> Doc
PP.string String
err
, String -> Doc
PP.string String
" [ "
, Int -> Doc
PP.int (Pid -> Int
unPid Pid
pid)
, String -> Doc
PP.string String
" ]"
, Doc
PP.line
, if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [tag]
tags)
then Doc
PP.line forall a. Semigroup a => a -> a -> a
<> String -> Doc
PP.string String
" " forall a. Semigroup a => a -> a -> a
<> [tag] -> [tag] -> Doc
tagsDiff [tag]
seen [tag]
tags forall a. Semigroup a => a -> a -> a
<> Doc
PP.line
else Doc
PP.empty
]
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) =
forall a. Monoid a => [a] -> a
mconcat
[ Doc
PP.line
, forall {k} (model :: k -> *) (r :: k).
ToExpr (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous
, Doc
PP.line, Doc
PP.line
, String -> Doc
PP.string String
" == "
, String -> Doc
PP.string (forall a. Show a => a -> String
ppShow cmd Concrete
cmd)
, String -> Doc
PP.string String
" ==> "
, String -> Doc
PP.string (forall a. Show a => a -> String
ppShow resp Concrete
resp)
, String -> Doc
PP.string String
" [ "
, Int -> Doc
PP.int (Pid -> Int
unPid Pid
pid)
, String -> Doc
PP.string String
" ]"
, Doc
PP.line
, if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [tag]
tags)
then Doc
PP.line forall a. Semigroup a => a -> a -> a
<> String -> Doc
PP.string String
" " forall a. Semigroup a => a -> a -> a
<> [tag] -> [tag] -> Doc
tagsDiff [tag]
seen [tag]
tags forall a. Semigroup a => a -> a -> a
<> Doc
PP.line
else Doc
PP.empty
, model Concrete
-> Maybe (model Concrete)
-> [tag]
-> [[tag]]
-> [Operation cmd resp]
-> Doc
go (forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
current cmd Concrete
cmd resp Concrete
resp) (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]
_ = forall a. HasCallStack => String -> a
error String
"prettyPrintHistory': impossible."
prettyCommands' :: (MonadIO m, ToExpr (model Concrete), ToExpr 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, ToExpr (model Concrete), ToExpr 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 =
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *) tag.
(ToExpr (model Concrete), Show (cmd Concrete),
Show (resp Concrete), ToExpr 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 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 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 <- forall t. FormatTime t => TimeLocale -> String -> t -> String
formatTime TimeLocale
defaultTimeLocale String
"%F_%T" 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 (forall a. Show a => a -> String
ppShow Commands cmd resp
cmds)
String -> IO ()
putStrLn (String
"Saved counterexample in: " 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 <- forall a. Read a => String -> a
read forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return (Commands cmd resp
cmds, History cmd resp
hist, model Concrete
model, Reason
res)
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 =
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Commands" (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames Commands cmd resp
cmds)
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
= forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
1 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, Int)]
names forall a. Eq a => a -> a -> Bool
== Int
numOfConstructors) String
"coverage"
where
names :: [(String, Int)]
names = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames Commands cmd resp
cmds
numOfConstructors :: Int
numOfConstructors = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
Proxy (cmd r) -> [String]
cmdNames (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 = forall k a. Map k a -> [(k, a)]
M.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map String Int -> Command cmd resp -> Map String Int
go forall k a. Map k a
M.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith forall a. Num a => a -> a -> a
(+) (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 = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [String] -> Command cmd resp -> [String]
go [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Command cmd resp -> String
commandName Command cmd resp
cmd forall a. a -> [a] -> [a]
: [String]
ih
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
-> Int
-> ([Event model cmd resp Symbolic] -> [tag])
-> (tag -> Bool)
-> 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 -> forall (m :: * -> *) a. MonadIO m => (StdGen -> (a, StdGen)) -> m a
getStdRandom (forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
1, Int
999999))
Just Int
seed -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
seed
forall prop. Testable prop => Args -> prop -> IO ()
labelledExamplesWith (Args
stdArgs { replay :: Maybe (QCGen, Int)
replay = forall a. a -> Maybe a
Just (Int -> QCGen
mkQCGen Int
replaySeed, Int
0)
, maxSuccess :: Int
maxSuccess = Int
numTests
}) forall a b. (a -> b) -> a -> b
$
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands StateMachine model cmd m resp
sm forall a. Maybe a
Nothing)
(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)
forall a. Show a => a -> String
ppShow forall a b. (a -> b) -> a -> b
$ \Commands cmd resp
cmds ->
forall a. Show a => [a] -> Property -> Property
collects (forall a. (a -> Bool) -> [a] -> [a]
filter tag -> Bool
focus forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Event model cmd resp Symbolic] -> [tag]
tag forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a b. (a -> b) -> a -> b
$ Commands cmd resp
cmds) forall a b. (a -> b) -> a -> b
$
forall prop. Testable prop => prop -> Property
property Bool
True
String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Used replaySeed " forall a. [a] -> [a] -> [a]
++ 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 = 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 forall a. Maybe a
Nothing Int
1000 [Event model cmd resp Symbolic] -> [tag]
tag (forall a b. a -> b -> a
const Bool
True)