{-# 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 (MonadSay, say)
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
  TChan m (Pid, HistoryEvent cmd resp)
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
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.
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
MonadCatch m =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
              m (StateMachine model cmd m resp)
msm
              (\StateMachine model cmd m resp
sm' ExitCase
  (Reason, (Environment, model Symbolic, Counter, model Concrete))
ec -> case ExitCase
  (Reason, (Environment, model Symbolic, Counter, model Concrete))
ec of
                            ExitCaseSuccess (Reason
_, (Environment
_,model Symbolic
_,Counter
_,model Concrete
model)) -> 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, MonadSay m, IOLike 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))
  [(Pid, HistoryEvent cmd resp)]
hist <- 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
  (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 :: 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
      Maybe a
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 Maybe a
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)
                => (MonadSay m, IOLike 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, MonadSay m, IOLike 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 ()
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
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)
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]
semantics :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete)
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
..} 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
      (Environment
env, model Symbolic
smodel, Counter
counter, model Concrete
cmodel) <- t 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 -> 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)))
          !Either String (resp Concrete)
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 Either String (resp Concrete)
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])