Echo.hs

Echo.hs

#!/usr/bin/env cabal
{- cabal:
  build-depends:
    base,
    quickcheck-state-machine,
    QuickCheck,
    unliftio,
    transformers,
    tasty,
    tasty-quickcheck
-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DerivingStrategies  #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# 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 Main
  ( main )
  where

import           Data.Bifunctor
import           Data.Kind                     (Type)
import           GHC.Generics                  (Generic, Generic1)
import           GHC.List                      (List)
import           Prelude
import           Test.QuickCheck
import           Test.QuickCheck.Monadic
import           Test.StateMachine
import           Test.StateMachine.TreeDiff
import           Test.StateMachine.Types       as QC
import qualified Test.StateMachine.Types.Rank2 as Rank2
import           Test.StateMachine.Utils
import           Test.Tasty
import           Test.Tasty.QuickCheck
import           UnliftIO

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

main :: IO ()
main = defaultMain
   $ testGroup "Tests"
   [ testProperty "Sequential" prop_echoOK
   , testProperty "Parallel" prop_echoParallelOK
   , testProperty "NParallel" (prop_echoNParallelOK 100)
   ]

-- | Spec for echo.

-- | This one will work as there is only one machine running
prop_echoOK :: Property
prop_echoOK = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do
    (tracer, getTraces) <- run $ recordingTracerIORef
    (hist, _, res) <- runCommandsWithSetup (echoSM tracer) cmds
    let l = howManyInsS cmds
    traces <- run $ getTraces
    liftProperty $
        counterexample ("More traces than in commands: " <> show (length traces) <> " vs " <> show l) $ boolean $ length traces .== l
    prettyCommands smUnused hist (res === Ok)

-- | Defining the tracer outside of the machine:
-- NOTE This will return wrong results! 10 vs 1
prop_echoParallelOK :: Property
prop_echoParallelOK = forAllParallelCommands smUnused Nothing $ \cmds ->
    monadicIO $ do
      (tracer, getTraces) <- run $ recordingTracerIORef
      h <- runParallelCommandsWithSetup (echoSM tracer) cmds
      let l = howManyInsP cmds
      traces <- run $ getTraces
      liftProperty $
        counterexample ("More traces than in commands: " <> show (length traces) <> " vs " <> show l) $ boolean $ length traces .== l
      prettyParallelCommands cmds h

-- | Defining the tracer inside of the machine:
-- I cannot even define this one! see `echoSM'`
prop_echoParallelOK' :: Property
prop_echoParallelOK' = forAllParallelCommands smUnused Nothing $ \cmds ->
    monadicIO $ do
      h <- runParallelCommandsWithSetup echoSM' cmds
      let l = howManyInsP cmds
      traces :: [String] <- undefined -- can't define this!!
      liftProperty $
        counterexample ("More traces than in commands: " <> show (length traces) <> " vs " <> show l) $ boolean $ length traces .== l
      prettyParallelCommands cmds h

-- | Same as prop_echoParallelOK
prop_echoNParallelOK :: Int -> Property
prop_echoNParallelOK np = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do
    (tracer, getTraces) <- run $ recordingTracerIORef
    h <- runNParallelCommandsWithSetup (echoSM tracer) cmds
    let l = howManyInsNP cmds
    traces <- run $ getTraces
    liftProperty $
      counterexample ("More traces than in commands: " <> show (length traces) <> " vs " <> show l) $ boolean $ length traces .== l
    prettyNParallelCommands cmds h

-- | 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.
o :: Env -> IO (Maybe String)
o (Env mBuf) = atomically $ do
    res <- readTVar mBuf
    writeTVar mBuf Nothing
    return res

-- | Create a 'Tracer' that stores all events in an 'IORef' that is atomically
-- updated. The second return value lets you obtain the events recorded so far
-- (from oldest to newest). Obtaining the events does not erase them.
recordingTracerIORef :: IO (ev -> IO (), IO [ev])
recordingTracerIORef = newIORef [] >>= \ref -> return
    ( \ev -> atomicModifyIORef' ref $ \evs -> (ev:evs, ())
    , reverse <$> readIORef ref
    )

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



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 = Main.generator
    , invariant = Nothing
    , QC.shrinker = Main.shrinker
    , QC.semantics = e
    , QC.mock = Main.mock
    , cleanup = noCleanup
    }
  where
    e = error "SUT must not be used"

echoSM :: (String -> IO ()) -> IO (StateMachine Model Action IO Response)
echoSM tr = do
  env <- mkEnv
  pure $ StateMachine
    { initModel = Empty -- At the beginning of time nothing was received.
    , transition = transitions
    , precondition = preconditions
    , postcondition = postconditions
    , QC.generator = Main.generator
    , invariant = Nothing
    , QC.shrinker = Main.shrinker
    , QC.semantics = Main.semantics env tr
    , QC.mock = Main.mock
    , cleanup = noCleanup
    }

echoSM' :: IO (StateMachine Model Action IO Response)
echoSM' = do
  env <- mkEnv
  (tracer, _getTraces) <- recordingTracerIORef -- don't have a way to return
                                              -- `getTraces`, I won't be able to
                                              -- check anything on them!
  pure $ StateMachine
    { initModel = Empty -- At the beginning of time nothing was received.
    , transition = transitions
    , precondition = preconditions
    , postcondition = postconditions
    , QC.generator = Main.generator
    , invariant = Nothing
    , QC.shrinker = Main.shrinker
    , QC.semantics = Main.semantics env tracer
    , QC.mock = Main.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 -> (String -> IO ()) -> Action Concrete -> IO (Response Concrete)
semantics env tr (In str) = do
    tr "Hi"
    success <- input env str
    return $ if success
               then InAck
               else ErrFull
semantics env _ Echo = maybe ErrEmpty Out <$> o 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)

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

-- | See how many `In` commands were issued
howManyInsS :: Commands Action resp -> Int
howManyInsS cmds =
  length
  $ filter (\case
               In{} -> True
               _ -> False)
  $ map getCommand
  $ unCommands cmds

-- | See how many `In` commands were issued
howManyInsP :: ParallelCommandsF Pair Action resp -> Int
howManyInsP cmds =
  length
  $ filter (\case
               In{} -> True
               _ -> False)
  $ map getCommand
  $ unCommands (prefix cmds)
  ++ concatMap (uncurry (++) . bimap unCommands unCommands . fromPair) (suffixes cmds)

-- | See how many `In` commands were issued
howManyInsNP :: forall resp. ParallelCommandsF List Action resp -> Int
howManyInsNP cmds =
  length
  $ filter (\case
               In{} -> True
               _ -> False)
  $ map getCommand
  $ unCommands (prefix cmds)
  ++ concat (concat (map (map unCommands) $ suffixes cmds))