{-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneDeriving #-} ----------------------------------------------------------------------------- -- | -- Module : Echo -- Copyright : (C) 2018, Damian Nadales -- License : BSD-style (see the file LICENSE) -- -- Maintainer : Stevan Andjelkovic -- Stability : provisional -- Portability : non-portable (GHC extensions) -- ------------------------------------------------------------------------ module Echo ( mkEnv , prop_echoOK , prop_echoNParallelOK , prop_echoParallelOK ) where import Data.Kind (Type) import GHC.Generics (Generic, Generic1) import Prelude import Test.QuickCheck (Gen, Property, arbitrary, oneof, (===)) import Test.QuickCheck.Monadic (monadicIO) import UnliftIO (TVar, atomically, newTVarIO, readTVar, writeTVar) import Test.StateMachine import Test.StateMachine.TreeDiff import Test.StateMachine.Types as QC import qualified Test.StateMachine.Types.Rank2 as Rank2 ------------------------------------------------------------------------ -- | Echo API. data Env = Env { _buf :: TVar (Maybe String) } -- | Create a new environment. mkEnv :: IO Env mkEnv = Env <$> newTVarIO Nothing -- | Input a string. Returns 'True' iff the buffer was empty and the given -- string was added to it. input :: Env -> String -> IO Bool input (Env mBuf) str = atomically $ do res <- readTVar mBuf case res of Nothing -> writeTVar mBuf (Just str) >> return True Just _ -> return False -- | Output the buffer contents. output :: Env -> IO (Maybe String) output (Env mBuf) = atomically $ do res <- readTVar mBuf writeTVar mBuf Nothing return res ------------------------------------------------------------------------ -- | Spec for echo. prop_echoOK :: Property prop_echoOK = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do (hist, _, res) <- runCommandsWithSetup echoSM cmds prettyCommands smUnused hist (res === Ok) prop_echoParallelOK :: Property prop_echoParallelOK = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do prettyParallelCommands cmds =<< runParallelCommandsWithSetup echoSM cmds prop_echoNParallelOK :: Int -> Property prop_echoNParallelOK np = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do prettyNParallelCommands cmds =<< runNParallelCommandsWithSetup echoSM cmds smUnused :: StateMachine Model Action IO Response smUnused = StateMachine { initModel = Empty -- At the beginning of time nothing was received. , transition = transitions , precondition = preconditions , postcondition = postconditions , QC.generator = Echo.generator , invariant = Nothing , QC.shrinker = Echo.shrinker , QC.semantics = e , QC.mock = Echo.mock , cleanup = noCleanup } where e = error "SUT must not be used" echoSM :: IO (StateMachine Model Action IO Response) echoSM = do env <- mkEnv pure $ StateMachine { initModel = Empty -- At the beginning of time nothing was received. , transition = transitions , precondition = preconditions , postcondition = postconditions , QC.generator = Echo.generator , invariant = Nothing , QC.shrinker = Echo.shrinker , QC.semantics = Echo.semantics env , QC.mock = Echo.mock , cleanup = noCleanup } transitions :: Model r -> Action r -> Response r -> Model r transitions Empty (In str) _ = Buf str transitions (Buf _) Echo _ = Empty transitions Empty Echo _ = Empty -- TODO: qcsm will match the case below. However we don't expect this to happen! transitions (Buf str) (In _) _ = Buf str -- Dummy response -- error "This shouldn't happen: input transition with full buffer" -- | There are no preconditions for this model. preconditions :: Model Symbolic -> Action Symbolic -> Logic preconditions _ _ = Top -- | Post conditions for the system. postconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic postconditions Empty (In _) InAck = Top postconditions (Buf _) (In _) ErrFull = Top postconditions _ (In _) _ = Bot postconditions Empty Echo ErrEmpty = Top postconditions Empty Echo _ = Bot postconditions (Buf str) Echo (Out out) = str .== out postconditions (Buf _) Echo _ = Bot -- | Generator for symbolic actions. generator :: Model Symbolic -> Maybe (Gen (Action Symbolic)) generator _ = Just $ oneof [ In <$> arbitrary , return Echo ] -- | Trivial shrinker. shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic] shrinker _ _ = [] -- | Here we'd do the dispatch to the actual SUT. semantics :: Env -> Action Concrete -> IO (Response Concrete) semantics env (In str) = do success <- input env str return $ if success then InAck else ErrFull semantics env Echo = maybe ErrEmpty Out <$> output env -- | What is the mock for? mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic) mock Empty (In _) = return InAck mock (Buf _) (In _) = return ErrFull mock Empty Echo = return ErrEmpty mock (Buf str) Echo = return (Out str) deriving anyclass instance ToExpr (Model Concrete) -- | The model contains the last string that was communicated in an input -- action. data Model (r :: Type -> Type) = -- | The model hasn't been initialized. Empty | -- | Last input string (a buffer with size one). Buf String deriving stock (Eq, Show, Generic) -- | Actions supported by the system. data Action (r :: Type -> Type) = -- | Input a string, which should be echoed later. In String -- | Request a string output. | Echo deriving stock (Show, Generic1) deriving anyclass (Rank2.Foldable, Rank2.Traversable, Rank2.Functor, CommandNames) -- | The system gives a single type of output response, containing a string -- with the input previously received. data Response (r :: Type -> Type) = -- | Input acknowledgment. InAck -- | The previous action wasn't an input, so there is no input to echo. -- This is: the buffer is empty. | ErrEmpty -- | There is already a string in the buffer. | ErrFull -- | Output string. | Out String deriving stock (Show, Generic1) deriving anyclass (Rank2.Foldable, Rank2.Traversable, Rank2.Functor)