{-# 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 <stevan.andjelkovic@strath.ac.uk>
-- 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, liftIO, newTVarIO, readTVar,
writeTVar)
import Test.StateMachine
import Test.StateMachine.Types
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
env <- liftIO $ mkEnv
let echoSM' = echoSM env
(hist, _, res) <- runCommands echoSM' cmds
prettyCommands echoSM' hist (res === Ok)
prop_echoParallelOK :: Bool -> Property
prop_echoParallelOK problem = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do
env <- liftIO $ mkEnv
let echoSM' = echoSM env
let n | problem = 2
| otherwise = 1
prettyParallelCommands cmds =<< runParallelCommandsNTimes n echoSM' cmds
prop_echoNParallelOK :: Int -> Bool -> Property
prop_echoNParallelOK np problem = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do
env <- liftIO $ mkEnv
let echoSM' = echoSM env
let n | problem = 2
| otherwise = 1
prettyNParallelCommands cmds =<< runNParallelCommandsNTimes n echoSM' cmds
smUnused :: StateMachine Model Action IO Response
smUnused = echoSM $ error "used env during command generation"
echoSM :: Env -> StateMachine Model Action IO Response
echoSM env = StateMachine
{ initModel = Empty
-- ^ At the beginning of time nothing was received.
, transition = mTransitions
, precondition = mPreconditions
, postcondition = mPostconditions
, generator = mGenerator
, invariant = Nothing
, shrinker = mShrinker
, semantics = mSemantics
, mock = mMock
, cleanup = noCleanup
}
where
mTransitions :: Model r -> Action r -> Response r -> Model r
mTransitions Empty (In str) _ = Buf str
mTransitions (Buf _) Echo _ = Empty
mTransitions Empty Echo _ = Empty
-- TODO: qcsm will match the case below. However we don't expect this to happen!
mTransitions (Buf str) (In _) _ = Buf str -- Dummy response
-- error "This shouldn't happen: input transition with full buffer"
-- | There are no preconditions for this model.
mPreconditions :: Model Symbolic -> Action Symbolic -> Logic
mPreconditions _ _ = Top
-- | Post conditions for the system.
mPostconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
mPostconditions Empty (In _) InAck = Top
mPostconditions (Buf _) (In _) ErrFull = Top
mPostconditions _ (In _) _ = Bot
mPostconditions Empty Echo ErrEmpty = Top
mPostconditions Empty Echo _ = Bot
mPostconditions (Buf str) Echo (Out out) = str .== out
mPostconditions (Buf _) Echo _ = Bot
-- | Generator for symbolic actions.
mGenerator :: Model Symbolic -> Maybe (Gen (Action Symbolic))
mGenerator _ = Just $ oneof
[ In <$> arbitrary
, return Echo
]
-- | Trivial shrinker.
mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
mShrinker _ _ = []
-- | Here we'd do the dispatch to the actual SUT.
mSemantics :: Action Concrete -> IO (Response Concrete)
mSemantics (In str) = do
success <- input env str
return $ if success
then InAck
else ErrFull
mSemantics Echo = maybe ErrEmpty Out <$> output env
-- | What is the mock for?
mMock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
mMock Empty (In _) = return InAck
mMock (Buf _) (In _) = return ErrFull
mMock Empty Echo = return ErrEmpty
mMock (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)