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

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Sequential
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module contains helpers for generating, shrinking, and checking
-- sequential programs.
--
-----------------------------------------------------------------------------

module Test.StateMachine.Sequential
  ( forAllCommands
  , existsCommands
  , generateCommands
  , generateCommandsState
  , deadlockError
  , getUsedVars
  , shrinkCommands
  , shrinkAndValidate
  , ValidateEnv(..)
  , ShouldShrink(..)
  , initValidateEnv
  , runCommands
  , runCommandsWithSetup
  , runCommands'
  , getChanContents
  , Check(..)
  , executeCommands
  , prettyPrintHistory
  , prettyPrintHistory'
  , prettyCommands
  , prettyCommands'
  , saveCommands
  , runSavedCommands
  , commandNames
  , commandNamesInOrder
  , coverCommandNames
  , checkCommandNames
  , showLabelledExamples
  , showLabelledExamples'
  )
  where

import           Control.Exception
                   (SomeAsyncException(..), SomeException,
                   displayException, fromException)
import           Control.Monad
                   (when)
import           Control.Monad.Catch
                   (ExitCase(..), MonadCatch(..), MonadMask(..), catch)
import           Control.Monad.State.Strict
                   (StateT, evalStateT, get, lift, put, runStateT)
import           Data.Bifunctor
                   (second)
import           Data.Dynamic
                   (Dynamic, toDyn)
import           Data.Either
                   (fromRight)
import           Data.List
                   (inits)
import qualified Data.Map                          as M
import           Data.Map.Strict
                   (Map)
import           Data.Maybe
                   (fromMaybe)
import           Data.Monoid
import           Data.Proxy
                   (Proxy(..))
import qualified Data.Set                          as S
import           Data.Time
                   (defaultTimeLocale, formatTime, getZonedTime)
import           Prelude
import           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 qualified Text.PrettyPrint.ANSI.Leijen      as PP
import           Text.PrettyPrint.ANSI.Leijen
                   (Doc)
import           Text.Show.Pretty
                   (ppShow)
import           UnliftIO
                   (MonadIO, TChan, atomically, liftIO, newTChanIO,
                   tryReadTChan, writeTChan)
import           UnliftIO.Exception
                   (throwIO)

import           Test.StateMachine.ConstructorName
import           Test.StateMachine.Diffing
                   (CanDiff(..), ediff)
import           Test.StateMachine.Labelling
                   (Event(..), execCmds)
import           Test.StateMachine.Logic
import           Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2     as Rank2
import           Test.StateMachine.Utils

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

forAllCommands :: Testable prop
               => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))
               => (Rank2.Traversable cmd, Rank2.Foldable resp)
               => StateMachine model cmd m resp
               -> Maybe Int -- ^ Minimum number of commands.
               -> (Commands cmd resp -> prop)     -- ^ Predicate.
               -> Property
forAllCommands :: forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (Commands cmd resp -> prop) -> Property
forAllCommands StateMachine model cmd m resp
sm Maybe Int
mminSize =
  Gen (Commands cmd resp)
-> (Commands cmd resp -> [Commands cmd resp])
-> (Commands cmd resp -> String)
-> (Commands cmd resp -> prop)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands StateMachine model cmd m resp
sm Maybe Int
mminSize) (StateMachine model cmd m resp
-> Commands cmd resp -> [Commands cmd resp]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Commands cmd resp -> [Commands cmd resp]
shrinkCommands StateMachine model cmd m resp
sm) Commands cmd resp -> String
forall a. Show a => a -> String
ppShow

-- | Generate commands from a list of generators.
existsCommands :: forall model cmd m resp prop. (Testable prop, Rank2.Foldable resp)
               => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic))
               => StateMachine model cmd m resp
               -> [model Symbolic -> Gen (cmd Symbolic)]  -- ^ Generators.
               -> (Commands cmd resp -> prop)             -- ^ Predicate.
               -> Property
existsCommands :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *) prop.
(Testable prop, Foldable resp, Show (model Symbolic),
 Show (cmd Symbolic), Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> [model Symbolic -> Gen (cmd Symbolic)]
-> (Commands cmd resp -> prop)
-> Property
existsCommands StateMachine { forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel, model Symbolic -> cmd Symbolic -> Logic
precondition :: model Symbolic -> cmd Symbolic -> Logic
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition, forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock } [model Symbolic -> Gen (cmd Symbolic)]
gens0 =
  Property -> Property
forall prop. Testable prop => prop -> Property
once (Property -> Property)
-> ((Commands cmd resp -> prop) -> Property)
-> (Commands cmd resp -> prop)
-> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen (Commands cmd resp)
-> (Commands cmd resp -> [Commands cmd resp])
-> (Commands cmd resp -> String)
-> (Commands cmd resp -> prop)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow ([model Symbolic -> Gen (cmd Symbolic)]
-> model Symbolic
-> Counter
-> [Command cmd resp]
-> Gen (Commands cmd resp)
go [model Symbolic -> Gen (cmd Symbolic)]
gens0 model Symbolic
forall (r :: * -> *). model r
initModel Counter
newCounter []) ([Commands cmd resp] -> Commands cmd resp -> [Commands cmd resp]
forall a b. a -> b -> a
const []) Commands cmd resp -> String
forall a. Show a => a -> String
ppShow
  where
    go :: [model Symbolic -> Gen (cmd Symbolic)] -> model Symbolic -> Counter
       -> [Command cmd resp] -> Gen (Commands cmd resp)
    go :: [model Symbolic -> Gen (cmd Symbolic)]
-> model Symbolic
-> Counter
-> [Command cmd resp]
-> Gen (Commands cmd resp)
go []           model Symbolic
_model Counter
_counter [Command cmd resp]
acc = Commands cmd resp -> Gen (Commands cmd resp)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
acc))
    go (model Symbolic -> Gen (cmd Symbolic)
gen : [model Symbolic -> Gen (cmd Symbolic)]
gens) model Symbolic
model  Counter
counter  [Command cmd resp]
acc = do
      cmd Symbolic
cmd <- ([cmd Symbolic] -> cmd Symbolic)
-> (cmd Symbolic -> cmd Symbolic)
-> Either [cmd Symbolic] (cmd Symbolic)
-> cmd Symbolic
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (model Symbolic -> [Command cmd resp] -> String -> cmd Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) b.
(Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
model Symbolic -> [Command cmd resp] -> String -> b
deadlockError model Symbolic
model [Command cmd resp]
acc (String -> cmd Symbolic)
-> ([cmd Symbolic] -> String) -> [cmd Symbolic] -> cmd Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [cmd Symbolic] -> String
forall a. Show a => a -> String
ppShow) cmd Symbolic -> cmd Symbolic
forall a. a -> a
id (Either [cmd Symbolic] (cmd Symbolic) -> cmd Symbolic)
-> Gen (Either [cmd Symbolic] (cmd Symbolic)) -> Gen (cmd Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
               model Symbolic -> Gen (cmd Symbolic)
gen model Symbolic
model Gen (cmd Symbolic)
-> (cmd Symbolic -> Bool)
-> Gen (Either [cmd Symbolic] (cmd Symbolic))
forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
`suchThatEither` (Logic -> Bool
boolean (Logic -> Bool) -> (cmd Symbolic -> Logic) -> cmd Symbolic -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model Symbolic -> cmd Symbolic -> Logic
precondition model Symbolic
model)
      let (resp Symbolic
resp, Counter
counter') = GenSym (resp Symbolic) -> Counter -> (resp Symbolic, Counter)
forall a. GenSym a -> Counter -> (a, Counter)
runGenSym (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock model Symbolic
model cmd Symbolic
cmd) Counter
counter
      [model Symbolic -> Gen (cmd Symbolic)]
-> model Symbolic
-> Counter
-> [Command cmd resp]
-> Gen (Commands cmd resp)
go [model Symbolic -> Gen (cmd Symbolic)]
gens (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
cmd resp Symbolic
resp) Counter
counter'
         (cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
Command cmd Symbolic
cmd resp Symbolic
resp (resp Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars resp Symbolic
resp) Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
acc)

deadlockError :: (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic))
              => model Symbolic -> [Command cmd resp] -> String -> b
deadlockError :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) b.
(Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
model Symbolic -> [Command cmd resp] -> String -> b
deadlockError model Symbolic
model [Command cmd resp]
generated String
counterexamples = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ String
"\n"
  , String
"A deadlock occured while generating commands.\n"
  , String
"No pre-condition holds in the following model:\n\n"
  , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ model Symbolic -> String
forall a. Show a => a -> String
ppShow model Symbolic
model
  , String
"\n\nThe following commands have been generated so far:\n\n"
  , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Command cmd resp] -> String
forall a. Show a => a -> String
ppShow [Command cmd resp]
generated
  , String
"\n\n"
  , String
"Example commands generated whose pre-condition doesn't hold:\n\n"
  , String
"    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
counterexamples
  , String
"\n"
  ]

generateCommands :: (Rank2.Foldable resp, Show (model Symbolic))
                 => (Show (cmd Symbolic), Show (resp Symbolic))
                 => StateMachine model cmd m resp
                 -> Maybe Int -- ^ Minimum number of commands.
                 -> Gen (Commands cmd resp)
generateCommands :: forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } Maybe Int
mminSize =
  StateT (model Symbolic) Gen (Commands cmd resp)
-> model Symbolic -> Gen (Commands cmd resp)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (StateMachine model cmd m resp
-> Counter
-> Maybe Int
-> StateT (model Symbolic) Gen (Commands cmd resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Counter
-> Maybe Int
-> StateT (model Symbolic) Gen (Commands cmd resp)
generateCommandsState StateMachine model cmd m resp
sm Counter
newCounter Maybe Int
mminSize) model Symbolic
forall (r :: * -> *). model r
initModel

generateCommandsState :: forall model cmd m resp. Rank2.Foldable resp
                      => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic))
                      => StateMachine model cmd m resp
                      -> Counter
                      -> Maybe Int -- ^ Minimum number of commands.
                      -> StateT (model Symbolic) Gen (Commands cmd resp)
generateCommandsState :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Counter
-> Maybe Int
-> StateT (model Symbolic) Gen (Commands cmd resp)
generateCommandsState StateMachine { model Symbolic -> cmd Symbolic -> Logic
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition :: model Symbolic -> cmd Symbolic -> Logic
precondition, model Symbolic -> Maybe (Gen (cmd Symbolic))
generator :: model Symbolic -> Maybe (Gen (cmd Symbolic))
generator :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Maybe (Gen (cmd Symbolic))
generator, forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock } Counter
counter0 Maybe Int
mminSize = do
  let minSize :: Int
minSize = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 Maybe Int
mminSize
  Int
size0 <- Gen Int -> StateT (model Symbolic) Gen Int
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (model Symbolic) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((Int -> Gen Int) -> Gen Int
forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
minSize, Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
minSize)))
  Int
-> Counter
-> [Command cmd resp]
-> StateT (model Symbolic) Gen (Commands cmd resp)
go Int
size0 Counter
counter0 []
  where
    go :: Int -> Counter -> [Command cmd resp]
       -> StateT (model Symbolic) Gen (Commands cmd resp)
    go :: Int
-> Counter
-> [Command cmd resp]
-> StateT (model Symbolic) Gen (Commands cmd resp)
go Int
0    Counter
_       [Command cmd resp]
cmds = Commands cmd resp
-> StateT (model Symbolic) Gen (Commands cmd resp)
forall a. a -> StateT (model Symbolic) Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
cmds))
    go Int
size Counter
counter [Command cmd resp]
cmds = do
      model Symbolic
model <- StateT (model Symbolic) Gen (model Symbolic)
forall s (m :: * -> *). MonadState s m => m s
get
      case model Symbolic -> Maybe (Gen (cmd Symbolic))
generator model Symbolic
model of
        Maybe (Gen (cmd Symbolic))
Nothing  -> Commands cmd resp
-> StateT (model Symbolic) Gen (Commands cmd resp)
forall a. a -> StateT (model Symbolic) Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
cmds))
        Just Gen (cmd Symbolic)
gen -> do
          Either [cmd Symbolic] (cmd Symbolic)
enext <- Gen (Either [cmd Symbolic] (cmd Symbolic))
-> StateT
     (model Symbolic) Gen (Either [cmd Symbolic] (cmd Symbolic))
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (model Symbolic) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Gen (Either [cmd Symbolic] (cmd Symbolic))
 -> StateT
      (model Symbolic) Gen (Either [cmd Symbolic] (cmd Symbolic)))
-> Gen (Either [cmd Symbolic] (cmd Symbolic))
-> StateT
     (model Symbolic) Gen (Either [cmd Symbolic] (cmd Symbolic))
forall a b. (a -> b) -> a -> b
$ Gen (cmd Symbolic)
gen Gen (cmd Symbolic)
-> (cmd Symbolic -> Bool)
-> Gen (Either [cmd Symbolic] (cmd Symbolic))
forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
`suchThatEither` (Logic -> Bool
boolean (Logic -> Bool) -> (cmd Symbolic -> Logic) -> cmd Symbolic -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model Symbolic -> cmd Symbolic -> Logic
precondition model Symbolic
model)
          case Either [cmd Symbolic] (cmd Symbolic)
enext of
            Left  [cmd Symbolic]
ces  -> model Symbolic
-> [Command cmd resp]
-> String
-> StateT (model Symbolic) Gen (Commands cmd resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) b.
(Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
model Symbolic -> [Command cmd resp] -> String -> b
deadlockError model Symbolic
model ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
cmds) ([cmd Symbolic] -> String
forall a. Show a => a -> String
ppShow [cmd Symbolic]
ces)
            Right cmd Symbolic
next -> do
              let (resp Symbolic
resp, Counter
counter') = GenSym (resp Symbolic) -> Counter -> (resp Symbolic, Counter)
forall a. GenSym a -> Counter -> (a, Counter)
runGenSym (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock model Symbolic
model cmd Symbolic
next) Counter
counter
              model Symbolic -> StateT (model Symbolic) Gen ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
next resp Symbolic
resp)
              Int
-> Counter
-> [Command cmd resp]
-> StateT (model Symbolic) Gen (Commands cmd resp)
go (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Counter
counter' (cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
Command cmd Symbolic
next resp Symbolic
resp (resp Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars resp Symbolic
resp) Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
cmds)

getUsedVars :: Rank2.Foldable f => f Symbolic -> [Var]
getUsedVars :: forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars = (forall x. Symbolic x -> [Var]) -> f Symbolic -> [Var]
forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> f p -> m
forall k (f :: (k -> *) -> *) m (p :: k -> *).
(Foldable f, Monoid m) =>
(forall (x :: k). p x -> m) -> f p -> m
Rank2.foldMap (\(Symbolic Var
v) -> [Var
v])

-- | Shrink commands in a pre-condition and scope respecting way.
shrinkCommands ::  forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
               => StateMachine model cmd m resp -> Commands cmd resp
               -> [Commands cmd resp]
shrinkCommands :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Commands cmd resp -> [Commands cmd resp]
shrinkCommands sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } =
    (Shrunk [Command cmd resp] -> [Commands cmd resp])
-> [Shrunk [Command cmd resp]] -> [Commands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk [Command cmd resp] -> [Commands cmd resp]
go ([Shrunk [Command cmd resp]] -> [Commands cmd resp])
-> (Commands cmd resp -> [Shrunk [Command cmd resp]])
-> Commands cmd resp
-> [Commands cmd resp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Command cmd resp] -> [Shrunk [Command cmd resp]]
forall a. [a] -> [Shrunk [a]]
shrinkListS' ([Command cmd resp] -> [Shrunk [Command cmd resp]])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Shrunk [Command cmd resp]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
  where
    go :: Shrunk [Command cmd resp] -> [Commands cmd resp]
    go :: Shrunk [Command cmd resp] -> [Commands cmd resp]
go (Shrunk Bool
shrunk [Command cmd resp]
cmds) = ((ValidateEnv model, Commands cmd resp) -> Commands cmd resp)
-> [(ValidateEnv model, Commands cmd resp)] -> [Commands cmd resp]
forall a b. (a -> b) -> [a] -> [b]
map (ValidateEnv model, Commands cmd resp) -> Commands cmd resp
forall a b. (a, b) -> b
snd ([(ValidateEnv model, Commands cmd resp)] -> [Commands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)] -> [Commands cmd resp]
forall a b. (a -> b) -> a -> b
$
        StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm
                          (if Bool
shrunk then ShouldShrink
DontShrink else ShouldShrink
MustShrink)
                          (model Symbolic -> ValidateEnv model
forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv model Symbolic
forall (r :: * -> *). model r
initModel)
                          ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
cmds)

-- | Environment required during 'shrinkAndValidate'
data ValidateEnv model = ValidateEnv {
      -- | The model we're starting validation from
      forall (model :: (* -> *) -> *).
ValidateEnv model -> model Symbolic
veModel   :: model Symbolic

      -- | Reference renumbering
      --
      -- When a command
      --
      -- > Command .. [Var i, ..]
      --
      -- is changed during validation to
      --
      -- > Command .. [Var j, ..]
      --
      -- then any subsequent uses of @Var i@ should be replaced by @Var j@. This
      -- is recorded in 'veScope'. When we /remove/ the first command
      -- altogether (during shrinking), then @Var i@ won't appear in the
      -- 'veScope' and shrank candidates that contain commands referring to @Var
      -- i@ should be considered as invalid.
    , forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope   :: Map Var Var

      -- | Counter (for generating new references)
    , forall (model :: (* -> *) -> *). ValidateEnv model -> Counter
veCounter :: Counter
    }

initValidateEnv :: model Symbolic -> ValidateEnv model
initValidateEnv :: forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv model Symbolic
initModel = ValidateEnv {
      veModel :: model Symbolic
veModel   = model Symbolic
initModel
    , veScope :: Map Var Var
veScope   = Map Var Var
forall k a. Map k a
M.empty
    , veCounter :: Counter
veCounter = Counter
newCounter
    }

data ShouldShrink = MustShrink | DontShrink

-- | Validate list of commands, optionally shrinking one of the commands
--
-- The input to this function is a list of commands ('Commands'), for example
--
-- > [A, B, C, D, E, F, G, H]
--
-- The /result/ is a /list/ of 'Commands', i.e. a list of lists. The
-- outermost list is used for all the shrinking possibilities. For example,
-- let's assume we haven't shrunk something yet, and therefore need to shrink
-- one of the commands. Let's further assume that only commands B and E can be
-- shrunk, to B1, B2 and E1, E2, E3 respectively. Then the result will look
-- something like
--
-- > [    -- outermost list recording all the shrink possibilities
-- >     [A', B1', C', D', E' , F', G', H']   -- B shrunk to B1
-- >   , [A', B2', C', D', E' , F', G', H']   -- B shrunk to B2
-- >   , [A', B' , C', D', E1', F', G', H']   -- E shrunk to E1
-- >   , [A', B' , C', D', E2', F', G', H']   -- E shrunk to E2
-- >   , [A', B' , C', D', E3', F', G', H']   -- E shrunk to E3
-- > ]
--
-- where one of the commands has been shrunk and all commands have been
-- validated and renumbered (references updated). So, in this example, the
-- result will contain at most 5 lists; it may contain fewer, since some of
-- these lists may not be valid.
--
-- If we _did_ already shrink something, then no commands will be shrunk, and
-- the resulting list will either be empty (if the list of commands was invalid)
-- or contain a /single/ element with the validated and renumbered commands.
shrinkAndValidate :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
                  => StateMachine model cmd m resp
                  -> ShouldShrink
                  -> ValidateEnv model
                  -> Commands cmd resp
                  -> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine { model Symbolic -> cmd Symbolic -> Logic
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition :: model Symbolic -> cmd Symbolic -> Logic
precondition, forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock, model Symbolic -> cmd Symbolic -> [cmd Symbolic]
shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
shrinker :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> [cmd Symbolic]
shrinker } =
    \ShouldShrink
env ValidateEnv model
shouldShrink Commands cmd resp
cmds -> ((ValidateEnv model, [Command cmd resp])
 -> (ValidateEnv model, Commands cmd resp))
-> [(ValidateEnv model, [Command cmd resp])]
-> [(ValidateEnv model, Commands cmd resp)]
forall a b. (a -> b) -> [a] -> [b]
map (([Command cmd resp] -> Commands cmd resp)
-> (ValidateEnv model, [Command cmd resp])
-> (ValidateEnv model, Commands cmd resp)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands) ([(ValidateEnv model, [Command cmd resp])]
 -> [(ValidateEnv model, Commands cmd resp)])
-> [(ValidateEnv model, [Command cmd resp])]
-> [(ValidateEnv model, Commands cmd resp)]
forall a b. (a -> b) -> a -> b
$ ShouldShrink
-> ValidateEnv model
-> [Command cmd resp]
-> [(ValidateEnv model, [Command cmd resp])]
go ShouldShrink
env ValidateEnv model
shouldShrink (Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands Commands cmd resp
cmds)
  where
    go :: ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])]
    go :: ShouldShrink
-> ValidateEnv model
-> [Command cmd resp]
-> [(ValidateEnv model, [Command cmd resp])]
go ShouldShrink
MustShrink   ValidateEnv model
_   [] = []          -- we failed to shrink anything
    go ShouldShrink
DontShrink   ValidateEnv model
env [] = [(ValidateEnv model
env, [])] -- successful termination
    go ShouldShrink
shouldShrink (ValidateEnv model Symbolic
model Map Var Var
scope Counter
counter) (Command cmd Symbolic
cmd' resp Symbolic
_resp [Var]
vars' : [Command cmd resp]
cmds) =
      case (forall a. Symbolic a -> Maybe (Symbolic a))
-> cmd Symbolic -> Maybe (cmd Symbolic)
forall k (t :: (k -> *) -> *) (f :: * -> *) (p :: k -> *)
       (q :: k -> *).
(Traversable t, Applicative f) =>
(forall (a :: k). p a -> f (q a)) -> t p -> f (t q)
forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> cmd p -> f (cmd q)
Rank2.traverse (Map Var Var -> Symbolic a -> Maybe (Symbolic a)
forall a. Map Var Var -> Symbolic a -> Maybe (Symbolic a)
remapVars Map Var Var
scope) cmd Symbolic
cmd' of
        Just cmd Symbolic
remapped ->
          -- shrink at most one command
          let candidates :: [(ShouldShrink, cmd Symbolic)]
              candidates :: [(ShouldShrink, cmd Symbolic)]
candidates =
                case ShouldShrink
shouldShrink of
                  ShouldShrink
DontShrink -> [(ShouldShrink
DontShrink, cmd Symbolic
remapped)]
                  ShouldShrink
MustShrink -> (cmd Symbolic -> (ShouldShrink, cmd Symbolic))
-> [cmd Symbolic] -> [(ShouldShrink, cmd Symbolic)]
forall a b. (a -> b) -> [a] -> [b]
map (ShouldShrink
DontShrink,) (model Symbolic -> cmd Symbolic -> [cmd Symbolic]
shrinker model Symbolic
model cmd Symbolic
remapped)
                             [(ShouldShrink, cmd Symbolic)]
-> [(ShouldShrink, cmd Symbolic)] -> [(ShouldShrink, cmd Symbolic)]
forall a. [a] -> [a] -> [a]
++ [(ShouldShrink
MustShrink, cmd Symbolic
remapped)]
          in (((ShouldShrink, cmd Symbolic)
  -> [(ValidateEnv model, [Command cmd resp])])
 -> [(ShouldShrink, cmd Symbolic)]
 -> [(ValidateEnv model, [Command cmd resp])])
-> [(ShouldShrink, cmd Symbolic)]
-> ((ShouldShrink, cmd Symbolic)
    -> [(ValidateEnv model, [Command cmd resp])])
-> [(ValidateEnv model, [Command cmd resp])]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((ShouldShrink, cmd Symbolic)
 -> [(ValidateEnv model, [Command cmd resp])])
-> [(ShouldShrink, cmd Symbolic)]
-> [(ValidateEnv model, [Command cmd resp])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [(ShouldShrink, cmd Symbolic)]
candidates (((ShouldShrink, cmd Symbolic)
  -> [(ValidateEnv model, [Command cmd resp])])
 -> [(ValidateEnv model, [Command cmd resp])])
-> ((ShouldShrink, cmd Symbolic)
    -> [(ValidateEnv model, [Command cmd resp])])
-> [(ValidateEnv model, [Command cmd resp])]
forall a b. (a -> b) -> a -> b
$ \(ShouldShrink
shouldShrink', cmd Symbolic
cmd) ->
               if Logic -> Bool
boolean (model Symbolic -> cmd Symbolic -> Logic
precondition model Symbolic
model cmd Symbolic
cmd)
                 then let (resp Symbolic
resp, Counter
counter') = GenSym (resp Symbolic) -> Counter -> (resp Symbolic, Counter)
forall a. GenSym a -> Counter -> (a, Counter)
runGenSym (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock model Symbolic
model cmd Symbolic
cmd) Counter
counter
                          vars :: [Var]
vars = resp Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars resp Symbolic
resp
                          env' :: ValidateEnv model
env' = ValidateEnv {
                                     veModel :: model Symbolic
veModel   = model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
cmd resp Symbolic
resp
                                   , veScope :: Map Var Var
veScope   = [(Var, Var)] -> Map Var Var
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([Var] -> [Var] -> [(Var, Var)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vars' [Var]
vars) Map Var Var -> Map Var Var -> Map Var Var
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map Var Var
scope
                                   , veCounter :: Counter
veCounter = Counter
counter'
                                   }
                      in ((ValidateEnv model, [Command cmd resp])
 -> (ValidateEnv model, [Command cmd resp]))
-> [(ValidateEnv model, [Command cmd resp])]
-> [(ValidateEnv model, [Command cmd resp])]
forall a b. (a -> b) -> [a] -> [b]
map (([Command cmd resp] -> [Command cmd resp])
-> (ValidateEnv model, [Command cmd resp])
-> (ValidateEnv model, [Command cmd resp])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
Command cmd Symbolic
cmd resp Symbolic
resp [Var]
varsCommand cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
:)) ([(ValidateEnv model, [Command cmd resp])]
 -> [(ValidateEnv model, [Command cmd resp])])
-> [(ValidateEnv model, [Command cmd resp])]
-> [(ValidateEnv model, [Command cmd resp])]
forall a b. (a -> b) -> a -> b
$ ShouldShrink
-> ValidateEnv model
-> [Command cmd resp]
-> [(ValidateEnv model, [Command cmd resp])]
go ShouldShrink
shouldShrink' ValidateEnv model
env' [Command cmd resp]
cmds
                 else []
        Maybe (cmd Symbolic)
Nothing ->
          []

    remapVars :: Map Var Var -> Symbolic a -> Maybe (Symbolic a)
    remapVars :: forall a. Map Var Var -> Symbolic a -> Maybe (Symbolic a)
remapVars Map Var Var
scope (Symbolic Var
v) = Var -> Symbolic a
forall a. Typeable a => Var -> Symbolic a
Symbolic (Var -> Symbolic a) -> Maybe Var -> Maybe (Symbolic a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> Map Var Var -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
v Map Var Var
scope

runCommands :: (Show (cmd Concrete), Show (resp Concrete))
            => (Rank2.Traversable cmd, Rank2.Foldable resp)
            => (MonadMask m, MonadIO m)
            => StateMachine model cmd m resp
            -> Commands cmd resp
            -> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m) =>
StateMachine model cmd m resp
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands StateMachine model cmd m resp
sm = m (StateMachine model cmd m resp)
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m) =>
m (StateMachine model cmd m resp)
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommandsWithSetup (StateMachine model cmd m resp -> m (StateMachine model cmd m resp)
forall a. a -> m a
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 = m (History cmd resp, model Concrete, Reason)
-> PropertyM m (History cmd resp, model Concrete, Reason)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m (History cmd resp, model Concrete, Reason)
 -> PropertyM m (History cmd resp, model Concrete, Reason))
-> m (History cmd resp, model Concrete, Reason)
-> PropertyM m (History cmd resp, model Concrete, Reason)
forall a b. (a -> b) -> a -> b
$ m (StateMachine model cmd m resp)
-> Commands cmd resp
-> m (History cmd resp, model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m) =>
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 <- m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
  (Reason
reason, (Environment
_, model Symbolic
_, Counter
_, model Concrete
model)) <-
    ((Reason, (Environment, model Symbolic, Counter, model Concrete)),
 ())
-> (Reason, (Environment, model Symbolic, Counter, model Concrete))
forall a b. (a, b) -> a
fst (((Reason, (Environment, model Symbolic, Counter, model Concrete)),
  ())
 -> (Reason,
     (Environment, model Symbolic, Counter, model Concrete)))
-> m ((Reason,
       (Environment, model Symbolic, Counter, model Concrete)),
      ())
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
    -> ExitCase
         (Reason, (Environment, model Symbolic, Counter, model Concrete))
    -> m ())
-> (StateMachine model cmd m resp
    -> m (Reason,
          (Environment, model Symbolic, Counter, model Concrete)))
-> m ((Reason,
       (Environment, model Symbolic, Counter, model Concrete)),
      ())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
              m (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)) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
                            ExitCase
  (Reason, (Environment, model Symbolic, Counter, model Concrete))
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
              )
              (\sm' :: StateMachine model cmd m resp
sm'@StateMachine{ forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } -> StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
                       (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm' TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
0) Check
CheckEverything Commands cmd resp
cmds)
                       (Environment
emptyEnvironment, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel))
  [(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
  (History cmd resp, model Concrete, Reason)
-> m (History cmd resp, model Concrete, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
model, Reason
reason)

-- We should try our best to not let this function fail,
-- since it is used to cleanup resources, in parallel programs.
getChanContents :: MonadIO m => TChan a -> m [a]
getChanContents :: forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan a
chan = [a] -> [a]
forall a. [a] -> [a]
reverse ([a] -> [a]) -> m [a] -> m [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM [a] -> m [a]
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically ([a] -> STM [a]
go' [])
  where
    go' :: [a] -> STM [a]
go' [a]
acc = do
      Maybe a
mx <- TChan a -> STM (Maybe a)
forall a. TChan a -> STM (Maybe a)
tryReadTChan TChan a
chan
      case Maybe a
mx of
        Just a
x  -> [a] -> STM [a]
go' (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc)
        Maybe a
Nothing -> [a] -> STM [a]
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
acc

data Check
  = CheckPrecondition
  | CheckEverything
  | CheckNothing

executeCommands :: (Show (cmd Concrete), Show (resp Concrete))
                => (Rank2.Traversable cmd, Rank2.Foldable resp)
                => (MonadCatch m, MonadIO m)
                => StateMachine model cmd m resp
                -> TChan (Pid, HistoryEvent cmd resp)
                -> Pid
                -> Check
                -> Commands cmd resp
                -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine {Maybe (model Concrete -> Logic)
cmd Concrete -> m (resp Concrete)
model Concrete -> m ()
model Concrete -> cmd Concrete -> resp Concrete -> Logic
model Symbolic -> Maybe (Gen (cmd Symbolic))
model Symbolic -> cmd Symbolic -> [cmd Symbolic]
model Symbolic -> cmd Symbolic -> Logic
model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
forall (r :: * -> *). model r
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
generator :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Maybe (Gen (cmd Symbolic))
shrinker :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> [cmd Symbolic]
cleanup :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
initModel :: forall (r :: * -> *). model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
precondition :: model Symbolic -> cmd Symbolic -> Logic
postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
invariant :: Maybe (model Concrete -> Logic)
generator :: model Symbolic -> Maybe (Gen (cmd Symbolic))
shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
semantics :: cmd Concrete -> m (resp Concrete)
mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
cleanup :: model Concrete -> m ()
postcondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Concrete -> cmd Concrete -> resp Concrete -> Logic
invariant :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> Maybe (model Concrete -> Logic)
semantics :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete)
..} TChan (Pid, HistoryEvent cmd resp)
hchan Pid
pid Check
check =
  [Command cmd resp]
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
go ([Command cmd resp]
 -> StateT
      (Environment, model Symbolic, Counter, model Concrete) m Reason)
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
  where
    go :: [Command cmd resp]
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
go []                           = Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a.
a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (m :: * -> *) a. Monad m => a -> m a
return Reason
Ok
    go (Command cmd Symbolic
scmd resp Symbolic
_ [Var]
vars : [Command cmd resp]
cmds) = do
      (Environment
env, model Symbolic
smodel, Counter
counter, model Concrete
cmodel) <- StateT
  (Environment, model Symbolic, Counter, model Concrete)
  m
  (Environment, model Symbolic, Counter, model Concrete)
forall s (m :: * -> *). MonadState s m => m s
get
      case (Check
check, Logic -> Value
logic (model Symbolic -> cmd Symbolic -> Logic
precondition model Symbolic
smodel cmd Symbolic
scmd)) of
        (Check
CheckPrecondition, VFalse Counterexample
ce) -> Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a.
a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
PreconditionFailed (Counterexample -> String
forall a. Show a => a -> String
show Counterexample
ce))
        (Check
CheckEverything,   VFalse Counterexample
ce) -> Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a.
a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
PreconditionFailed (Counterexample -> String
forall a. Show a => a -> String
show Counterexample
ce))
        (Check, Value)
_otherwise                    -> do
          let ccmd :: cmd Concrete
ccmd = cmd Concrete
-> Either EnvironmentError (cmd Concrete) -> cmd Concrete
forall b a. b -> Either a b -> b
fromRight (String -> cmd Concrete
forall a. HasCallStack => String -> a
error String
"executeCommands: impossible") (Environment
-> cmd Symbolic -> Either EnvironmentError (cmd Concrete)
forall (t :: (* -> *) -> *).
Traversable t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
env cmd Symbolic
scmd)
          STM ()
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m ()
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (TChan (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, cmd Concrete -> Set Var -> HistoryEvent cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Concrete -> Set Var -> HistoryEvent cmd resp
Invocation cmd Concrete
ccmd ([Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
vars)))
          !Either String (resp Concrete)
ecresp <- m (Either String (resp Concrete))
-> StateT
     (Environment, model Symbolic, Counter, model Concrete)
     m
     (Either String (resp Concrete))
forall (m :: * -> *) a.
Monad m =>
m a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Either String (resp Concrete))
 -> StateT
      (Environment, model Symbolic, Counter, model Concrete)
      m
      (Either String (resp Concrete)))
-> m (Either String (resp Concrete))
-> StateT
     (Environment, model Symbolic, Counter, model Concrete)
     m
     (Either String (resp Concrete))
forall a b. (a -> b) -> a -> b
$ (resp Concrete -> Either String (resp Concrete))
-> m (resp Concrete) -> m (Either String (resp Concrete))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap resp Concrete -> Either String (resp Concrete)
forall a b. b -> Either a b
Right (cmd Concrete -> m (resp Concrete)
semantics cmd Concrete
ccmd) m (Either String (resp Concrete))
-> (SomeException -> m (Either String (resp Concrete)))
-> m (Either String (resp Concrete))
forall e a. (HasCallStack, Exception e) => m a -> (e -> m a) -> m a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
`catch`
                            \(SomeException
err :: SomeException) -> do
                              Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SomeException -> Bool
isSomeAsyncException SomeException
err) (IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SomeException -> String
forall e. Exception e => e -> String
displayException SomeException
err) m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SomeException -> m ()
forall (m :: * -> *) e a. (MonadIO m, Exception e) => e -> m a
throwIO SomeException
err)
                              Either String (resp Concrete) -> m (Either String (resp Concrete))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String (resp Concrete)
forall a b. a -> Either a b
Left (SomeException -> String
forall e. Exception e => e -> String
displayException SomeException
err))
          case Either String (resp Concrete)
ecresp of
            Left String
err    -> do
              STM ()
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m ()
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (TChan (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, String -> HistoryEvent cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
String -> HistoryEvent cmd resp
Exception String
err))
              Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a.
a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason
 -> StateT
      (Environment, model Symbolic, Counter, model Concrete) m Reason)
-> Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a b. (a -> b) -> a -> b
$ String -> Reason
ExceptionThrown String
err
            Right resp Concrete
cresp -> do
              let cvars :: [Dynamic]
cvars = resp Concrete -> [Dynamic]
forall (f :: (* -> *) -> *). Foldable f => f Concrete -> [Dynamic]
getUsedConcrete resp Concrete
cresp
              if [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Dynamic] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Dynamic]
cvars
              then do
                let err :: String
err = String -> String -> String -> String -> String
mockSemanticsMismatchError (cmd Concrete -> String
forall a. Show a => a -> String
ppShow cmd Concrete
ccmd) ([Var] -> String
forall a. Show a => a -> String
ppShow [Var]
vars) (resp Concrete -> String
forall a. Show a => a -> String
ppShow resp Concrete
cresp) ([Dynamic] -> String
forall a. Show a => a -> String
ppShow [Dynamic]
cvars)
                STM ()
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m ()
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (TChan (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, resp Concrete -> HistoryEvent cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
resp Concrete -> HistoryEvent cmd resp
Response resp Concrete
cresp))
                Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a.
a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason
 -> StateT
      (Environment, model Symbolic, Counter, model Concrete) m Reason)
-> Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a b. (a -> b) -> a -> b
$ String -> Reason
MockSemanticsMismatch String
err
              else do
                STM ()
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m ()
forall (m :: * -> *) a. MonadIO m => STM a -> m a
atomically (TChan (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, resp Concrete -> HistoryEvent cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
resp Concrete -> HistoryEvent cmd resp
Response resp Concrete
cresp))
                case (Check
check, Logic -> Value
logic (model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition model Concrete
cmodel cmd Concrete
ccmd resp Concrete
cresp)) of
                  (Check
CheckEverything, VFalse Counterexample
ce) -> Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a.
a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
PostconditionFailed (Counterexample -> String
forall a. Show a => a -> String
show Counterexample
ce))
                  (Check, Value)
_otherwise ->
                    case (Check
check, Logic -> Value
logic ((model Concrete -> Logic)
-> Maybe (model Concrete -> Logic) -> model Concrete -> Logic
forall a. a -> Maybe a -> a
fromMaybe (Logic -> model Concrete -> Logic
forall a b. a -> b -> a
const Logic
Top) Maybe (model Concrete -> Logic)
invariant model Concrete
cmodel)) of
                      (Check
CheckEverything, VFalse Counterexample
ce') -> Reason
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall a.
a
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Reason
InvariantBroken (Counterexample -> String
forall a. Show a => a -> String
show Counterexample
ce'))
                      (Check, Value)
_otherwise                    -> do
                        let (resp Symbolic
sresp, Counter
counter') = GenSym (resp Symbolic) -> Counter -> (resp Symbolic, Counter)
forall a. GenSym a -> Counter -> (a, Counter)
runGenSym (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock model Symbolic
smodel cmd Symbolic
scmd) Counter
counter
                        (Environment, model Symbolic, Counter, model Concrete)
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ( [Var] -> [Dynamic] -> Environment -> Environment
insertConcretes [Var]
vars [Dynamic]
cvars Environment
env
                            , model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
smodel cmd Symbolic
scmd resp Symbolic
sresp
                            , Counter
counter'
                            , model Concrete -> cmd Concrete -> resp Concrete -> model Concrete
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
cmodel cmd Concrete
ccmd resp Concrete
cresp
                            )
                        [Command cmd resp]
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
go [Command cmd resp]
cmds

    isSomeAsyncException :: SomeException -> Bool
    isSomeAsyncException :: SomeException -> Bool
isSomeAsyncException SomeException
se = case SomeException -> Maybe SomeAsyncException
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
se of
      Just (SomeAsyncException e
_) -> Bool
True
      Maybe SomeAsyncException
_                           -> Bool
False

    mockSemanticsMismatchError :: String -> String -> String -> String -> String
    mockSemanticsMismatchError :: String -> String -> String -> String -> String
mockSemanticsMismatchError String
cmd String
svars String
cresp String
cvars = [String] -> String
unlines
      [ String
""
      , String
"Mismatch between `mock` and `semantics`."
      , String
""
      , String
"The definition of `mock` for the command:"
      , String
""
      , String
"    ", String
cmd
      , String
""
      , String
"returns the following references:"
      , String
""
      , String
"    ", String
svars
      , String
""
      , String
"while the response from `semantics`:"
      , String
""
      , String
"    ", String
cresp
      , String
""
      , String
"returns the following references:"
      , String
""
      , String
"    ", String
cvars
      , String
""
      , String
"Continuing to execute commands at this point could result in scope"
      , String
"errors, because we might have commands that use references (returned"
      , String
"by `mock`) that are not available (returned by `semantics`)."
      , String
""
      ]

getUsedConcrete :: Rank2.Foldable f => f Concrete -> [Dynamic]
getUsedConcrete :: forall (f :: (* -> *) -> *). Foldable f => f Concrete -> [Dynamic]
getUsedConcrete = (forall x. Concrete x -> [Dynamic]) -> f Concrete -> [Dynamic]
forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> f p -> m
forall k (f :: (k -> *) -> *) m (p :: k -> *).
(Foldable f, Monoid m) =>
(forall (x :: k). p x -> m) -> f p -> m
Rank2.foldMap (\(Concrete x
x) -> [x -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn x
x])

modelDiff :: forall model r. CanDiff (model r) => model r -> Maybe (model r) -> Doc
modelDiff :: forall {k} (model :: k -> *) (r :: k).
CanDiff (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model r
model = Proxy (model r) -> ADiff (model r) -> Doc
forall x. CanDiff x => Proxy x -> ADiff x -> Doc
diffToDocCompact Proxy (model r)
p (ADiff (model r) -> Doc)
-> (Maybe (model r) -> ADiff (model r)) -> Maybe (model r) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (model r -> model r -> ADiff (model r))
-> model r -> model r -> ADiff (model r)
forall a b c. (a -> b -> c) -> b -> a -> c
flip model r -> model r -> ADiff (model r)
forall x. CanDiff x => x -> x -> ADiff x
ediff model r
model (model r -> ADiff (model r))
-> (Maybe (model r) -> model r)
-> Maybe (model r)
-> ADiff (model r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model r -> Maybe (model r) -> model r
forall a. a -> Maybe a -> a
fromMaybe model r
model
 where
   p :: Proxy (model r)
p = forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(model r)

prettyPrintHistory :: forall model cmd m resp. CanDiff (model Concrete)
                   => (Show (cmd Concrete), Show (resp Concrete))
                   => StateMachine model cmd m resp
                   -> History cmd resp
                   -> IO ()
prettyPrintHistory :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(CanDiff (model Concrete), Show (cmd Concrete),
 Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> IO ()
prettyPrintHistory StateMachine { forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel, forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition }
  = Doc -> IO ()
PP.putDoc
  (Doc -> IO ())
-> (History cmd resp -> Doc) -> History cmd resp -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model Concrete
-> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
go model Concrete
forall (r :: * -> *). model r
initModel Maybe (model Concrete)
forall a. Maybe a
Nothing
  ([Operation cmd resp] -> Doc)
-> (History cmd resp -> [Operation cmd resp])
-> History cmd resp
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History' cmd resp -> [Operation cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [Operation cmd resp]
makeOperations
  (History' cmd resp -> [Operation cmd resp])
-> (History cmd resp -> History' cmd resp)
-> History cmd resp
-> [Operation cmd resp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
  where
    go :: model Concrete -> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
    go :: model Concrete
-> Maybe (model Concrete) -> [Operation cmd resp] -> Doc
go model Concrete
current Maybe (model Concrete)
previous [] =
      Doc
PP.line Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> model Concrete -> Maybe (model Concrete) -> Doc
forall {k} (model :: k -> *) (r :: k).
CanDiff (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
PP.line Doc -> Doc -> Doc
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] =
      [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
        [ Doc
PP.line
        , model Concrete -> Maybe (model Concrete) -> Doc
forall {k} (model :: k -> *) (r :: k).
CanDiff (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 (cmd Concrete -> 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) =
      [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
        [ Doc
PP.line
        , model Concrete -> Maybe (model Concrete) -> Doc
forall {k} (model :: k -> *) (r :: k).
CanDiff (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 (cmd Concrete -> String
forall a. Show a => a -> String
ppShow cmd Concrete
cmd)
        , String -> Doc
PP.string String
" ==> "
        , String -> Doc
PP.string (resp Concrete -> 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 (model Concrete -> cmd Concrete -> resp Concrete -> model Concrete
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
current cmd Concrete
cmd resp Concrete
resp) (model Concrete -> Maybe (model Concrete)
forall a. a -> Maybe a
Just model Concrete
current) [Operation cmd resp]
ops
        ]
    go model Concrete
_ Maybe (model Concrete)
_ [Operation cmd resp]
_ = String -> Doc
forall a. HasCallStack => String -> a
error String
"prettyPrintHistory: impossible."

prettyCommands :: (MonadIO m, CanDiff (model Concrete))
               => (Show (cmd Concrete), Show (resp Concrete))
               => StateMachine model cmd m resp
               -> History cmd resp
               -> Property
               -> PropertyM m ()
prettyCommands :: forall (m :: * -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(MonadIO m, CanDiff (model Concrete), Show (cmd Concrete),
 Show (resp Concrete)) =>
StateMachine model cmd m resp
-> History cmd resp -> Property -> PropertyM m ()
prettyCommands StateMachine model cmd m resp
sm History cmd resp
hist Property
prop = StateMachine model cmd m resp -> History cmd resp -> IO ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(CanDiff (model Concrete), Show (cmd Concrete),
 Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> IO ()
prettyPrintHistory StateMachine model cmd m resp
sm History cmd resp
hist IO () -> Property -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` Property
prop

prettyPrintHistory' :: forall model cmd m resp tag. CanDiff (model Concrete)
                    => (Show (cmd Concrete), Show (resp Concrete), CanDiff [tag])
                    => StateMachine model cmd m resp
                    -> ([Event model cmd resp Symbolic] -> [tag])
                    -> Commands cmd resp
                    -> History cmd resp
                    -> IO ()
prettyPrintHistory' :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *) tag.
(CanDiff (model Concrete), Show (cmd Concrete),
 Show (resp Concrete), CanDiff [tag]) =>
StateMachine model cmd m resp
-> ([Event model cmd resp Symbolic] -> [tag])
-> Commands cmd resp
-> History cmd resp
-> IO ()
prettyPrintHistory' sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel, forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition } [Event model cmd resp Symbolic] -> [tag]
tag Commands cmd resp
cmds
  = Doc -> IO ()
PP.putDoc
  (Doc -> IO ())
-> (History cmd resp -> Doc) -> History cmd resp -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. model Concrete
-> Maybe (model Concrete)
-> [tag]
-> [[tag]]
-> [Operation cmd resp]
-> Doc
go model Concrete
forall (r :: * -> *). model r
initModel Maybe (model Concrete)
forall a. Maybe a
Nothing [] (([Event model cmd resp Symbolic] -> [tag])
-> [[Event model cmd resp Symbolic]] -> [[tag]]
forall a b. (a -> b) -> [a] -> [b]
map [Event model cmd resp Symbolic] -> [tag]
tag (Int
-> [[Event model cmd resp Symbolic]]
-> [[Event model cmd resp Symbolic]]
forall a. Int -> [a] -> [a]
drop Int
1 ([Event model cmd resp Symbolic]
-> [[Event model cmd resp Symbolic]]
forall a. [a] -> [[a]]
inits (StateMachine model cmd m resp
-> Commands cmd resp -> [Event model cmd resp Symbolic]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> Commands cmd resp -> [Event model cmd resp Symbolic]
execCmds StateMachine model cmd m resp
sm Commands cmd resp
cmds))))
  ([Operation cmd resp] -> Doc)
-> (History cmd resp -> [Operation cmd resp])
-> History cmd resp
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History' cmd resp -> [Operation cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [Operation cmd resp]
makeOperations
  (History' cmd resp -> [Operation cmd resp])
-> (History cmd resp -> History' cmd resp)
-> History cmd resp
-> [Operation cmd resp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
  where
    tagsDiff :: [tag] -> [tag] -> Doc
    tagsDiff :: [tag] -> [tag] -> Doc
tagsDiff [tag]
old [tag]
new = Proxy [tag] -> ADiff [tag] -> Doc
forall x. CanDiff x => Proxy x -> ADiff x -> Doc
diffToDocCompact (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @[tag]) ([tag] -> [tag] -> ADiff [tag]
forall x. CanDiff x => x -> x -> ADiff x
ediff [tag]
old [tag]
new)

    go :: model Concrete -> Maybe (model Concrete) -> [tag] -> [[tag]]
       -> [Operation cmd resp] -> Doc
    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 Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> model Concrete -> Maybe (model Concrete) -> Doc
forall {k} (model :: k -> *) (r :: k).
CanDiff (model r) =>
model r -> Maybe (model r) -> Doc
modelDiff model Concrete
current Maybe (model Concrete)
previous Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
PP.line Doc -> Doc -> Doc
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] =
      [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
        [ Doc
PP.line
        , model Concrete -> Maybe (model Concrete) -> Doc
forall {k} (model :: k -> *) (r :: k).
CanDiff (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 (cmd Concrete -> 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 ([tag] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [tag]
tags)
          then Doc
PP.line Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
PP.string String
"   " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [tag] -> [tag] -> Doc
tagsDiff [tag]
seen [tag]
tags Doc -> Doc -> Doc
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) =
      [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
        [ Doc
PP.line
        , model Concrete -> Maybe (model Concrete) -> Doc
forall {k} (model :: k -> *) (r :: k).
CanDiff (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 (cmd Concrete -> String
forall a. Show a => a -> String
ppShow cmd Concrete
cmd)
        , String -> Doc
PP.string String
" ==> "
        , String -> Doc
PP.string (resp Concrete -> 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 ([tag] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [tag]
tags)
          then Doc
PP.line Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
PP.string String
"   " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [tag] -> [tag] -> Doc
tagsDiff [tag]
seen [tag]
tags Doc -> Doc -> Doc
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 (model Concrete -> cmd Concrete -> resp Concrete -> model Concrete
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
current cmd Concrete
cmd resp Concrete
resp) (model Concrete -> Maybe (model Concrete)
forall a. a -> Maybe a
Just model Concrete
current) [tag]
tags [[tag]]
tagss [Operation cmd resp]
ops
        ]
    go model Concrete
_ Maybe (model Concrete)
_ [tag]
_ [[tag]]
_ [Operation cmd resp]
_ = String -> Doc
forall a. HasCallStack => String -> a
error String
"prettyPrintHistory': impossible."

-- | Variant of 'prettyCommands' that also prints the @tag@s covered by each
-- command.
prettyCommands' :: (MonadIO m, CanDiff (model Concrete), CanDiff [tag])
                => (Show (cmd Concrete), Show (resp Concrete))
                => StateMachine model cmd m resp
                -> ([Event model cmd resp Symbolic] -> [tag])
                -> Commands cmd resp
                -> History cmd resp
                -> Property
                -> PropertyM m ()
prettyCommands' :: forall (m :: * -> *) (model :: (* -> *) -> *) tag
       (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(MonadIO m, CanDiff (model Concrete), CanDiff [tag],
 Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp
-> ([Event model cmd resp Symbolic] -> [tag])
-> Commands cmd resp
-> History cmd resp
-> Property
-> PropertyM m ()
prettyCommands' StateMachine model cmd m resp
sm [Event model cmd resp Symbolic] -> [tag]
tag Commands cmd resp
cmds History cmd resp
hist Property
prop =
  StateMachine model cmd m resp
-> ([Event model cmd resp Symbolic] -> [tag])
-> Commands cmd resp
-> History cmd resp
-> IO ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *) tag.
(CanDiff (model Concrete), Show (cmd Concrete),
 Show (resp Concrete), CanDiff [tag]) =>
StateMachine model cmd m resp
-> ([Event model cmd resp Symbolic] -> [tag])
-> Commands cmd resp
-> History cmd resp
-> IO ()
prettyPrintHistory' StateMachine model cmd m resp
sm [Event model cmd resp Symbolic] -> [tag]
tag Commands cmd resp
cmds History cmd resp
hist IO () -> Property -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` Property
prop

saveCommands :: (Show (cmd Symbolic), Show (resp Symbolic))
             => FilePath -> Commands cmd resp -> Property -> Property
saveCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(Show (cmd Symbolic), Show (resp Symbolic)) =>
String -> Commands cmd resp -> Property -> Property
saveCommands String
dir Commands cmd resp
cmds Property
prop = IO ()
go IO () -> Property -> Property
forall prop. Testable prop => IO () -> prop -> Property
`whenFail` Property
prop
  where
    go :: IO ()
    go :: IO ()
go = do
      Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dir
      String
file <- TimeLocale -> String -> ZonedTime -> String
forall t. FormatTime t => TimeLocale -> String -> t -> String
formatTime TimeLocale
defaultTimeLocale String
"%F_%T" (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
      let fp :: String
fp = String
dir String -> String -> String
</> String
file
      String -> String -> IO ()
writeFile String
fp (Commands cmd resp -> String
forall a. Show a => a -> String
ppShow Commands cmd resp
cmds)
      String -> IO ()
putStrLn (String
"Saved counterexample in: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fp)
      String -> IO ()
putStrLn String
""

runSavedCommands :: (Show (cmd Concrete), Show (resp Concrete))
                 => (Rank2.Traversable cmd, Rank2.Foldable resp)
                 => (MonadMask m, MonadIO m)
                 => (Read (cmd Symbolic), Read (resp Symbolic))
                 => StateMachine model cmd m resp
                 -> FilePath
                 -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason)
runSavedCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m, Read (cmd Symbolic),
 Read (resp Symbolic)) =>
StateMachine model cmd m resp
-> String
-> PropertyM
     m (Commands cmd resp, History cmd resp, model Concrete, Reason)
runSavedCommands StateMachine model cmd m resp
sm String
fp = do
  Commands cmd resp
cmds <- String -> Commands cmd resp
forall a. Read a => String -> a
read (String -> Commands cmd resp)
-> PropertyM m String -> PropertyM m (Commands cmd resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> PropertyM m String
forall a. IO a -> PropertyM m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO String
readFile String
fp)
  (History cmd resp
hist, model Concrete
model, Reason
res) <- StateMachine model cmd m resp
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m) =>
StateMachine model cmd m resp
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands StateMachine model cmd m resp
sm Commands cmd resp
cmds
  (Commands cmd resp, History cmd resp, model Concrete, Reason)
-> PropertyM
     m (Commands cmd resp, History cmd resp, model Concrete, Reason)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Commands cmd resp
cmds, History cmd resp
hist, model Concrete
model, Reason
res)

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

-- | Print the percentage of each command used. The prefix check is
--   an unfortunate remaining for backwards compatibility.
checkCommandNames :: forall cmd resp. CommandNames cmd
                  => Commands cmd resp -> Property -> Property
checkCommandNames :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
checkCommandNames Commands cmd resp
cmds =
    String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Commands" ((String, Int) -> String
forall a b. (a, b) -> a
fst ((String, Int) -> String) -> [(String, Int)] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Commands cmd resp -> [(String, Int)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames Commands cmd resp
cmds)

-- | Fail if some commands have not been executed.
coverCommandNames :: forall cmd resp. CommandNames cmd
                  => Commands cmd resp -> Property -> Property
coverCommandNames :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
coverCommandNames Commands cmd resp
cmds
  = Double -> Bool -> String -> Property -> Property
forall prop.
Testable prop =>
Double -> Bool -> String -> prop -> Property
cover Double
1 ([(String, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, Int)]
names Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
numOfConstructors) String
"coverage"
  where
    names :: [(String, Int)]
names             = Commands cmd resp -> [(String, Int)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames Commands cmd resp
cmds
    numOfConstructors :: Int
numOfConstructors = [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Proxy (cmd Symbolic) -> [String]
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
Proxy (cmd r) -> [String]
forall (r :: * -> *). Proxy (cmd r) -> [String]
cmdNames (Proxy (cmd Symbolic)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (cmd Symbolic)))

commandNames :: forall cmd resp. CommandNames cmd
             => Commands cmd resp -> [(String, Int)]
commandNames :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames = Map String Int -> [(String, Int)]
forall k a. Map k a -> [(k, a)]
M.toList (Map String Int -> [(String, Int)])
-> (Commands cmd resp -> Map String Int)
-> Commands cmd resp
-> [(String, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map String Int -> Command cmd resp -> Map String Int)
-> Map String Int -> [Command cmd resp] -> Map String Int
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Map String Int -> Command cmd resp -> Map String Int
go Map String Int
forall k a. Map k a
M.empty ([Command cmd resp] -> Map String Int)
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> Map String Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
  where
    go :: Map String Int -> Command cmd resp -> Map String Int
    go :: Map String Int -> Command cmd resp -> Map String Int
go Map String Int
ih Command cmd resp
cmd = (Int -> Int -> Int)
-> String -> Int -> Map String Int -> Map String Int
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Command cmd resp -> String
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Command cmd resp -> String
commandName Command cmd resp
cmd) Int
1 Map String Int
ih

commandNamesInOrder :: forall cmd resp. CommandNames cmd
                    => Commands cmd resp -> [String]
commandNamesInOrder :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [String]
commandNamesInOrder = [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String])
-> (Commands cmd resp -> [String]) -> Commands cmd resp -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String] -> Command cmd resp -> [String])
-> [String] -> [Command cmd resp] -> [String]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [String] -> Command cmd resp -> [String]
go [] ([Command cmd resp] -> [String])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
  where
    go :: [String] -> Command cmd resp -> [String]
    go :: [String] -> Command cmd resp -> [String]
go [String]
ih Command cmd resp
cmd = Command cmd resp -> String
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Command cmd resp -> String
commandName Command cmd resp
cmd String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ih

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

-- | Show minimal examples for each of the generated tags.
showLabelledExamples' :: (Show tag, Show (model Symbolic))
                      => (Show (cmd Symbolic), Show (resp Symbolic))
                      => (Rank2.Traversable cmd, Rank2.Foldable resp)
                      => StateMachine model cmd m resp
                      -> Maybe Int
                      -- ^ Seed
                      -> Int
                      -- ^ Number of tests to run to find examples
                      -> ([Event model cmd resp Symbolic] -> [tag])
                      -> (tag -> Bool)
                      -- ^ Tag filter (can be @const True@)
                      -> IO ()
showLabelledExamples' :: forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (m :: * -> *).
(Show tag, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int
-> Int
-> ([Event model cmd resp Symbolic] -> [tag])
-> (tag -> Bool)
-> IO ()
showLabelledExamples' StateMachine model cmd m resp
sm Maybe Int
mReplay Int
numTests [Event model cmd resp Symbolic] -> [tag]
tag tag -> Bool
focus = do
    Int
replaySeed <- case Maybe Int
mReplay of
      Maybe Int
Nothing   -> (StdGen -> (Int, StdGen)) -> IO Int
forall (m :: * -> *) a. MonadIO m => (StdGen -> (a, StdGen)) -> m a
getStdRandom ((Int, Int) -> StdGen -> (Int, StdGen)
forall g. RandomGen g => (Int, Int) -> g -> (Int, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
1, Int
999999))
      Just Int
seed -> Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
seed

    Args -> Property -> IO ()
forall prop. Testable prop => Args -> prop -> IO ()
labelledExamplesWith (Args
stdArgs { replay     = Just (mkQCGen replaySeed, 0)
                                  , maxSuccess = numTests
                                  }) (Property -> IO ()) -> Property -> IO ()
forall a b. (a -> b) -> a -> b
$
      Gen (Commands cmd resp)
-> (Commands cmd resp -> [Commands cmd resp])
-> (Commands cmd resp -> String)
-> (Commands cmd resp -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands StateMachine model cmd m resp
sm Maybe Int
forall a. Maybe a
Nothing)
                       (StateMachine model cmd m resp
-> Commands cmd resp -> [Commands cmd resp]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Commands cmd resp -> [Commands cmd resp]
shrinkCommands   StateMachine model cmd m resp
sm)
                       Commands cmd resp -> String
forall a. Show a => a -> String
ppShow ((Commands cmd resp -> Property) -> Property)
-> (Commands cmd resp -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Commands cmd resp
cmds ->
        [tag] -> Property -> Property
forall a. Show a => [a] -> Property -> Property
collects ((tag -> Bool) -> [tag] -> [tag]
forall a. (a -> Bool) -> [a] -> [a]
filter tag -> Bool
focus ([tag] -> [tag])
-> (Commands cmd resp -> [tag]) -> Commands cmd resp -> [tag]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Event model cmd resp Symbolic] -> [tag]
tag ([Event model cmd resp Symbolic] -> [tag])
-> (Commands cmd resp -> [Event model cmd resp Symbolic])
-> Commands cmd resp
-> [tag]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp
-> Commands cmd resp -> [Event model cmd resp Symbolic]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> Commands cmd resp -> [Event model cmd resp Symbolic]
execCmds StateMachine model cmd m resp
sm (Commands cmd resp -> [tag]) -> Commands cmd resp -> [tag]
forall a b. (a -> b) -> a -> b
$ Commands cmd resp
cmds) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
          Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True

    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Used replaySeed " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
replaySeed

showLabelledExamples :: (Show tag, Show (model Symbolic))
                     => (Show (cmd Symbolic), Show (resp Symbolic))
                     => (Rank2.Traversable cmd, Rank2.Foldable resp)
                     => StateMachine model cmd m resp
                     -> ([Event model cmd resp Symbolic] -> [tag])
                     -> IO ()
showLabelledExamples :: forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (m :: * -> *).
(Show tag, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ([Event model cmd resp Symbolic] -> [tag]) -> IO ()
showLabelledExamples StateMachine model cmd m resp
sm [Event model cmd resp Symbolic] -> [tag]
tag = StateMachine model cmd m resp
-> Maybe Int
-> Int
-> ([Event model cmd resp Symbolic] -> [tag])
-> (tag -> Bool)
-> IO ()
forall tag (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (m :: * -> *).
(Show tag, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int
-> Int
-> ([Event model cmd resp Symbolic] -> [tag])
-> (tag -> Bool)
-> IO ()
showLabelledExamples' StateMachine model cmd m resp
sm Maybe Int
forall a. Maybe a
Nothing Int
1000 [Event model cmd resp Symbolic] -> [tag]
tag (Bool -> tag -> Bool
forall a b. a -> b -> a
const Bool
True)