content: {-# LANGUAGE DeriveAnyClass       #-}
  {-# LANGUAGE DeriveGeneric        #-}
  {-# LANGUAGE DerivingStrategies   #-}
  {-# LANGUAGE ExplicitNamespaces   #-}
  {-# LANGUAGE FlexibleContexts     #-}
  {-# LANGUAGE FlexibleInstances    #-}
  {-# LANGUAGE MonoLocalBinds       #-}
  {-# LANGUAGE PolyKinds            #-}
  {-# LANGUAGE RecordWildCards      #-}
  {-# LANGUAGE ScopedTypeVariables  #-}
  {-# LANGUAGE StandaloneDeriving   #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  module Mock
      ( prop_sequential_mock
      , prop_parallel_mock
      , prop_nparallel_mock
      )
      where
  
  import           Control.Concurrent
  import           Control.Monad.IO.Class
                     (liftIO)
  import           GHC.Generics
                     (Generic, Generic1)
  import           Prelude
  import           Test.QuickCheck
  import           Test.QuickCheck.Monadic
                     (monadicIO)
  import           Test.StateMachine
  import           Test.StateMachine.DotDrawing
  import qualified Test.StateMachine.Types.Rank2 as Rank2
  
  ------------------------------------------------------------------------
  
  data Command r
    = Create
    deriving stock (Eq, Generic1)
    deriving anyclass (Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
  
  deriving stock instance Show (Command Symbolic)
  deriving stock instance Read (Command Symbolic)
  deriving stock instance Show (Command Concrete)
  
  data Response r
    = Created (Reference Int r)
    | NotCreated
    deriving stock (Eq, Generic1)
    deriving anyclass Rank2.Foldable
  
  deriving stock instance Show (Response Symbolic)
  deriving stock instance Read (Response Symbolic)
  deriving stock instance Show (Response Concrete)
  
  data Model r = Model {
        refs :: [Reference Int r]
      , c    :: Int
      }
    deriving stock (Generic, Show)
  
  instance ToExpr (Model Symbolic)
  instance ToExpr (Model Concrete)
  
  initModel :: Model r
  initModel = Model [] 0
  
  transition :: Model r -> Command r -> Response r -> Model r
  transition m@Model{..} cmd resp = case (cmd, resp, c) of
    (Create, Created ref, 0) -> Model (ref : refs) 1
    (Create, _, _)           -> m
  
  precondition :: Model Symbolic -> Command Symbolic -> Logic
  precondition _ cmd = case cmd of
      Create        -> Top
  
  postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
  postcondition _ _ _ = Top
  
  semantics :: MVar Int -> Command Concrete -> IO (Response Concrete)
  semantics counter cmd = case cmd of
    Create        -> do
      c <- modifyMVar counter (\x -> return (x + 1, x))
      case c of
          0 -> return $ Created $ reference c
          _ -> return NotCreated
  
  mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
  mock Model{..} cmd = case (cmd, c) of
    (Create, 0) -> Created   <$> genSym
    (Create, _) -> return NotCreated
  
  generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
  generator _            = Just $ frequency
      [(1, return Create)]
  
  shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
  shrinker _ _ = []
  
  sm :: MVar Int ->  StateMachine Model Command IO Response
  sm counter = StateMachine initModel transition precondition postcondition
          Nothing generator shrinker (semantics counter) mock noCleanup
  
  smUnused :: StateMachine Model Command IO Response
  smUnused = sm undefined
  
  prop_sequential_mock :: Property
  prop_sequential_mock = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do
    counter <- liftIO $ newMVar 0
    (hist, _model, res) <- runCommands (sm counter) cmds
    prettyCommands smUnused hist (res === Ok)
  
  prop_parallel_mock :: Property
  prop_parallel_mock = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do
      counter <- liftIO $ newMVar 0
      ret <- runParallelCommandsNTimes 1 (sm counter) cmds
      prettyParallelCommandsWithOpts cmds opts ret
        where opts = Just $ GraphOptions "mock-test-output.png" Png
  
  prop_nparallel_mock :: Property
  prop_nparallel_mock = forAllNParallelCommands smUnused 3 $ \cmds -> monadicIO $ do
      counter <- liftIO $ newMVar 0
      ret <- runNParallelCommandsNTimes 1 (sm counter) cmds
      prettyNParallelCommandsWithOpts cmds opts ret
        where opts = Just $ GraphOptions "mock-np-test-output.png" Png
  