{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}

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

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

-- |
--
--
-- /___This is a superficial variation of the quickcheck-state-machine___/
-- /___source file that uses @io-classes@ instead of @MonadIO@, @UnliftIO@,___/
-- /___etc.___/ Perhaps
-- <https://github.com/input-output-hk/quickcheck-dynamic/tree/main/quickcheck-dynamic-iosim>
-- will supplant this.
--
--
--
-- Module      :  Test.Consensus.IOSimQSM.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.Consensus.IOSimQSM.Test.StateMachine.Sequential (runCommands') where

import Control.Concurrent.Class.MonadSTM.TChan
  ( TChan
  , newTChanIO
  , tryReadTChan
  , writeTChan
  )
import Control.Exception
  ( SomeAsyncException (..)
  , SomeException
  , displayException
  , fromException
  )
import Control.Monad (when)
import Control.Monad.Class.MonadSay
import Control.Monad.State.Strict (StateT, get, lift, put, runStateT)
import Data.Dynamic (Dynamic, toDyn)
import Data.Either (fromRight)
import Data.Maybe (fromMaybe)
import qualified Data.Set as S
import Ouroboros.Consensus.Util.IOLike
  ( ExitCase (..)
  , IOLike
  , MonadCatch (..)
  , atomically
  , catch
  , throwIO
  )
import Test.StateMachine.Logic
import Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.StateMachine.Utils
import Text.Show.Pretty (ppShow)

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

runCommands' ::
  (Show (cmd Concrete), Show (resp Concrete)) =>
  (Rank2.Traversable cmd, Rank2.Foldable resp) =>
  (IOLike m, MonadSay 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, IOLike m, MonadSay 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
  hchan <- m (TChan m (Pid, HistoryEvent cmd resp))
forall a. m (TChan m a)
forall (m :: * -> *) a. MonadSTM m => m (TChan m a)
newTChanIO
  (reason, (_, _, _, model)) <-
    fst
      <$> generalBracket
        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 m (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. IOLike m => TChan m a -> m [a]
getChanContents TChan m (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 (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> 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 m (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, IOLike m, MonadSay m) =>
StateMachine model cmd m resp
-> TChan m (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 m (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)
        )
  hist <- getChanContents hchan
  return (History hist, model, reason)

-- We should try our best to not let this function fail,
-- since it is used to cleanup resources, in parallel programs.
getChanContents :: IOLike m => TChan m a -> m [a]
getChanContents :: forall (m :: * -> *) a. IOLike m => TChan m a -> m [a]
getChanContents TChan m 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 m [a] -> m [a]
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically ([a] -> STM m [a]
forall {m :: * -> *}.
(TChan m ~ TChan m, MonadSTM m) =>
[a] -> STM m [a]
go' [])
 where
  go' :: [a] -> STM m [a]
go' [a]
acc = do
    mx <- TChan m a -> STM m (Maybe a)
forall a. TChan m a -> STM m (Maybe a)
forall (m :: * -> *) a. MonadSTM m => TChan m a -> STM m (Maybe a)
tryReadTChan TChan m a
TChan m a
chan
    case mx of
      Just a
x -> [a] -> STM m [a]
go' (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc)
      Maybe a
Nothing -> [a] -> STM m [a]
forall a. a -> STM m a
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
acc

data Check
  = CheckPrecondition
  | CheckEverything

executeCommands ::
  (Show (cmd Concrete), Show (resp Concrete)) =>
  (Rank2.Traversable cmd, Rank2.Foldable resp) =>
  (IOLike m, MonadSay m) =>
  StateMachine model cmd m resp ->
  TChan m (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, IOLike m, MonadSay m) =>
StateMachine model cmd m resp
-> TChan m (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
cleanup :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
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 ()
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
semantics :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete)
shrinker :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> [cmd Symbolic]
generator :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Maybe (Gen (cmd Symbolic))
invariant :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> Maybe (model Concrete -> Logic)
postcondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Concrete -> cmd Concrete -> resp Concrete -> Logic
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
..} TChan m (Pid, HistoryEvent cmd resp)
hchan Pid
pid Check
check =
  [Command cmd resp]
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall {t :: (* -> *) -> * -> *} {resp :: (* -> *) -> *}.
(MonadState
   (Environment, model Symbolic, Counter, model Concrete) (t m),
 MonadTrans t) =>
[Command cmd resp] -> t 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] -> t m Reason
go [] = Reason -> t m Reason
forall a. a -> t 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
    (env, smodel, counter, cmodel) <- t m (Environment, model Symbolic, Counter, model Concrete)
forall s (m :: * -> *). MonadState s m => m s
get
    case (check, logic (precondition smodel scmd)) of
      (Check
CheckPrecondition, VFalse Counterexample
ce) -> Reason -> t m Reason
forall a. a -> t 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 -> t m Reason
forall a. a -> t 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)
        m () -> t m ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> t m ()) -> m () -> t m ()
forall a b. (a -> b) -> a -> b
$ STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (TChan m (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM m ()
forall a. TChan m a -> a -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TChan m a -> a -> STM m ()
writeTChan TChan m (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)))
        !ecresp <-
          m (Either String (resp Concrete))
-> t m (Either String (resp Concrete))
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (Either String (resp Concrete))
 -> t m (Either String (resp Concrete)))
-> m (Either String (resp Concrete))
-> t 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. Exception e => m a -> (e -> m a) -> m a
forall (m :: * -> *) e a.
(MonadCatch m, 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) (String -> m ()
forall (m :: * -> *). MonadSay m => String -> m ()
say (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 e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow 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 ecresp of
          Left String
err -> do
            m () -> t m ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> t m ()) -> m () -> t m ()
forall a b. (a -> b) -> a -> b
$ STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (TChan m (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM m ()
forall a. TChan m a -> a -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TChan m a -> a -> STM m ()
writeTChan TChan m (Pid, HistoryEvent cmd resp)
hchan (Pid
pid, String -> HistoryEvent cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
String -> HistoryEvent cmd resp
Exception String
err))
            Reason -> t m Reason
forall a. a -> t m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason -> t m Reason) -> Reason -> t 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)
                m () -> t m ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> t m ()) -> m () -> t m ()
forall a b. (a -> b) -> a -> b
$ STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (TChan m (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM m ()
forall a. TChan m a -> a -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TChan m a -> a -> STM m ()
writeTChan TChan m (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 -> t m Reason
forall a. a -> t m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason -> t m Reason) -> Reason -> t m Reason
forall a b. (a -> b) -> a -> b
$ String -> Reason
MockSemanticsMismatch String
err
              else do
                m () -> t m ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> t m ()) -> m () -> t m ()
forall a b. (a -> b) -> a -> b
$ STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (TChan m (Pid, HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp) -> STM m ()
forall a. TChan m a -> a -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TChan m a -> a -> STM m ()
writeTChan TChan m (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 -> t m Reason
forall a. a -> t 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 -> t m Reason
forall a. a -> t 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) -> t 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] -> t 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])