{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TupleSections         #-}

-----------------------------------------------------------------------------
-- |
-- 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
  , 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 -- ^ 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 =
  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

-- | 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 (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 -- ^ 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 (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 -- ^ 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 :: 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])

-- | 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 (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)

-- | 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   = 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 :: 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
_   [] = []          -- 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 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 ->
          -- 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 -> 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)

-- 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 = 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."

-- | Variant of 'prettyCommands' that also prints the @tag@s covered by each
-- command.
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)

------------------------------------------------------------------------

-- | 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 =
    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)

-- | 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
  = 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

------------------------------------------------------------------------

-- | 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   -> 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)