Created
February 28, 2024 15:34
-
-
Save jasagredo/f0f3fea4b14811fb0df7fdf8d8dac91c to your computer and use it in GitHub Desktop.
Echo.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment