libraft-0.2.0.0: test/QuickCheckStateMachine.hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE StandaloneDeriving #-}
module QuickCheckStateMachine where
import Control.Concurrent (threadDelay)
import Control.Exception (bracket)
import Control.Monad.IO.Class (liftIO)
import Data.Bifunctor (bimap)
import Data.Char (isDigit)
import Data.List (isInfixOf, (\\))
import Data.Maybe (isJust, isNothing)
import qualified Data.Set as Set
import Data.TreeDiff (ToExpr)
import GHC.Generics (Generic, Generic1)
import Prelude hiding (notElem)
import System.Directory (removePathForcibly)
import System.IO (BufferMode (NoBuffering),
Handle, IOMode (WriteMode),
hClose, hGetLine, hPutStrLn,
hPutStrLn, hSetBuffering,
openFile)
import System.Process (ProcessHandle, StdStream (CreatePipe, UseHandle),
callCommand, createProcess_,
getPid, getProcessExitCode, waitForProcess,
proc, std_err, std_in, std_out,
terminateProcess)
import System.Timeout (timeout)
import Test.QuickCheck (Gen, Property, arbitrary,
elements, frequency,
noShrinking, shrink,
verboseCheck, withMaxSuccess,
(===))
import Test.QuickCheck.Monadic (monadicIO)
import Test.StateMachine (Concrete, GenSym, Logic (..),
Opaque (..), Reason (Ok),
Reference, StateMachine (..),
Symbolic, forAllCommands, notElem,
genSym, opaque, prettyCommands,
reference, runCommands, (.&&),
(.//), (.<), (.==), (.>=))
import Test.StateMachine.Types (Command(..), Commands (..), Reference(..), Symbolic(..), Var(..))
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Text.Read (readEither)
import qualified Data.Functor.Classes
import Debug.Trace (trace)
------------------------------------------------------------------------
type Port = Int
data Persistence = Fresh | Existing
deriving (Show)
data ClientHandleRefs (r :: * -> *) = ClientHandleRefs
{ client_hin :: Reference (Opaque Handle) r
, client_hout :: Reference (Opaque Handle) r
} deriving (Show, Generic, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
deriving instance ToExpr (ClientHandleRefs Concrete)
type ProcessHandleRef r = Reference (Opaque ProcessHandle) r
data Action (r :: * -> *)
= SpawnNode Port Persistence
| SpawnClient Port
| KillNode (Port, ProcessHandleRef r)
| Set (ClientHandleRefs r) Integer
| Read (ClientHandleRefs r)
| Incr (ClientHandleRefs r)
| BreakConnection (Port, ProcessHandleRef r)
| FixConnection (Port, ProcessHandleRef r)
deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
data Response (r :: * -> *)
= SpawnedNode (ProcessHandleRef r)
| SpawnedClient (ClientHandleRefs r) (ProcessHandleRef r)
| SpawnFailed Port
| BrokeConnection
| FixedConnection
| Ack
| Timeout
| Value (Either String Integer)
deriving (Show, Generic1, Rank2.Foldable)
data Model (r :: * -> *) = Model
{ nodes :: [(Port, ProcessHandleRef r)]
, client :: Maybe (ClientHandleRefs r, ProcessHandleRef r)
, started :: Bool
, value :: Maybe Integer
, isolated :: [(Port, ProcessHandleRef r)]
}
deriving (Show, Generic)
deriving instance ToExpr (Model Concrete)
initModel :: Model r
initModel = Model [] Nothing False Nothing []
transition :: Data.Functor.Classes.Show1 r => Model r -> Action r -> Response r -> Model r
transition Model {..} act resp = case (act, resp) of
(SpawnNode port _, SpawnedNode ph) ->
let newNodes = nodes ++ [(port, ph)]
in if length newNodes == 3
then Model { nodes = newNodes, started = True, .. }
else Model { nodes = newNodes, .. }
(SpawnNode {}, SpawnFailed _) -> Model {..}
(SpawnClient {}, SpawnedClient chrs cph) -> Model { client = Just (chrs, cph), .. }
(SpawnClient {}, SpawnFailed _) -> Model {..}
(KillNode (port, _ph), Ack) -> Model { nodes = filter ((/= port) . fst) nodes, isolated = filter ((/= port) . fst) isolated, .. }
(Set _ i, Ack) -> Model { value = Just i, .. }
(Read {}, Value _i) -> Model {..}
(Incr {}, Ack) -> Model { value = succ <$> value, ..}
(BreakConnection node, BrokeConnection) -> Model { isolated = node:isolated, .. }
(FixConnection (port,_), FixedConnection) -> Model { isolated = filter ((/= port) . fst) isolated, .. }
(Read {}, Timeout) -> Model {..}
(Set {}, Timeout) -> Model {..}
(Incr {}, Timeout) -> Model {..}
unaccounted -> trace (show unaccounted) $ error "transition"
-- TODO I don't think the precondition is being checked...
precondition :: Model Symbolic -> Action Symbolic -> Logic
precondition Model {..} act = case act of
SpawnNode {} -> length nodes .< 3
SpawnClient {} -> length nodes .== 3 .&& Boolean (isNothing client)
KillNode {} -> length nodes .== 3
Set _ i -> length nodes .== 3 .&& i .>= 0
Read _ -> length nodes .== 3 .&& Boolean (isJust value)
Incr _ -> length nodes .== 3 .&& Boolean (isJust value)
BreakConnection (port, _) -> length nodes .== 3 .&& port `notElem` map fst isolated
FixConnection {} -> length nodes .== 3 .&& Boolean (not (null isolated))
postcondition :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
postcondition Model {..} act resp = case (act, resp) of
(Read _, Value (Right i)) -> Just i .== value
(Read _, Value (Left e)) -> Bot .// e
(SpawnNode {}, SpawnedNode {}) -> Top
(SpawnNode {}, SpawnFailed {}) -> Bot .// "SpawnFailed - Node"
(SpawnClient {}, SpawnedClient {}) -> Top
(SpawnClient {}, SpawnFailed {}) -> Bot .// "SpawnFailed - Client"
(KillNode {}, Ack) -> Top
(Set {}, Ack) -> Top
(Incr {}, Ack) -> Top
(BreakConnection {}, BrokeConnection) -> Top
(FixConnection {}, FixedConnection) -> Top
(Read _, Timeout) -> Boolean (not (null isolated)) .// "Read timeout"
(Set {}, Timeout) -> Boolean (not (null isolated)) .// "Set timeout"
(Incr {}, Timeout) -> Boolean (not (null isolated)) .// "Incr timeout"
(_, _) -> Bot .// "postcondition"
command :: Handle -> ClientHandleRefs Concrete -> String -> IO (Int, Maybe String)
command h chs@ClientHandleRefs{..} cmd = go 3 0
where
go 0 unex = pure (unex, Nothing)
go n unex = do
eRes <- do
hPutStrLn h cmd
hPutStrLn (opaque client_hin) cmd
mresp <- getResponse (opaque client_hout)
case mresp of
Nothing -> do
hPutStrLn h "'getResponse' timed out"
pure (Just (unex, Nothing))
Just resp ->
if "Timeout" `isInfixOf` resp
then do
hPutStrLn h ("Command timed out, retrying: " ++ show resp)
pure (Just (unex, Nothing))
else if "Unexpected" `isInfixOf` resp
then do
hPutStrLn h ("Unexpected read/write response, retrying: " ++ show resp)
pure (Just (unex + 1, Nothing))
else do
hPutStrLn h ("got response `" ++ resp ++ "'")
pure (Just (unex, Just resp))
case eRes of
Nothing -> pure (unex, Nothing)
-- Recurse if command successful
Just (unex, Nothing) -> threadDelay 1000000 >> go (n-1) unex
Just (unex, Just resp) -> pure (unex, Just resp)
getResponse :: Handle -> IO (Maybe String)
getResponse hout = do
mline <- timeout 10000000 (hGetLine hout)
case mline of
Nothing -> return Nothing
Just line
| "New leader found" `isInfixOf` line -> getResponse hout
| otherwise -> return (Just line)
semantics :: Handle -> Action Concrete -> IO (Response Concrete)
semantics h (SpawnNode port1 p) = do
hPutStrLn h ("Spawning node on port " ++ show port1)
removePathForcibly ("/tmp/raft-log-" ++ show port1 ++ ".txt")
h' <- openFile ("/tmp/raft-log-" ++ show port1 ++ ".txt") WriteMode
let port2, port3 :: Int
(port2, port3) = case port1 of
3000 -> (3001, 3002)
3001 -> (3000, 3002)
3002 -> (3000, 3001)
_ -> error "semantics: invalid port1"
let persistence Fresh = "fresh"
persistence Existing = "existing"
(_, _, _, ph) <- createProcess_ "raft node"
(proc "fiu-run" [ "-x", "stack", "exec", "raft-example", "node"
, persistence p, "postgres", show port1
, "localhost:" ++ show port1
, "localhost:" ++ show port2
, "localhost:" ++ show port3
])
{ std_out = UseHandle h'
, std_err = UseHandle h'
}
threadDelay 1500000
mec <- getProcessExitCode ph
case mec of
Nothing -> return (SpawnedNode (reference (Opaque ph)))
Just ec -> do
hPutStrLn h (show ec)
return (SpawnFailed port1)
semantics h (SpawnClient cport) = do
hPutStrLn h "Spawning client"
(Just hin, Just hout, _, ph) <- createProcess_ "raft client"
(proc "stack" [ "exec", "raft-example", "client" ])
{ std_out = CreatePipe
, std_in = CreatePipe
, std_err = CreatePipe
}
threadDelay 1000000
mec <- getProcessExitCode ph
case mec of
Just ec -> do
hPutStrLn h (show ec)
return (SpawnFailed cport)
Nothing -> do
threadDelay 100000
hSetBuffering hin NoBuffering
hSetBuffering hout NoBuffering
hPutStrLn hin "addNode localhost:3000"
hPutStrLn hin "addNode localhost:3001"
hPutStrLn hin "addNode localhost:3002"
let refClient_hin = reference (Opaque hin)
refClient_hout = reference (Opaque hout)
clientHandleRefs = ClientHandleRefs refClient_hin refClient_hout
return (SpawnedClient clientHandleRefs (reference (Opaque ph)))
semantics h (KillNode (_port, ph)) = do
hPutStrLn h $ "Attempting to kill node on port " ++ show _port ++ "..."
terminateProcess (opaque ph)
waitForProcess (opaque ph)
hPutStrLn h $ "Successfully killed node on port " ++ show _port
return Ack
semantics h (Set chs i) = do
(_, mresp) <- command h chs ("set x " ++ show i)
case mresp of
Nothing -> return Timeout
Just _resp -> return Ack
semantics h (Read chs) = do
(ue, mresp) <- command h chs "read"
case mresp of
Nothing -> return Timeout
Just resp -> do
let parse = readEither
. takeWhile isDigit
. drop 1
. snd
. break (== ',')
return (Value (bimap (++ (": " ++ resp)) id (parse resp)))
semantics h (Incr chs) = do
(_, mresp) <- command h chs "incr x"
case mresp of
Nothing -> return Timeout
Just resp -> return Ack
semantics h (BreakConnection (port, ph)) = do
hPutStrLn h ("Break connection, port: " ++ show port)
Just pid <- getPid (opaque ph)
callCommand ("fiu-ctrl -c \"enable name=posix/io/net/send\" " ++ show pid)
callCommand ("fiu-ctrl -c \"enable name=posix/io/net/recv\" " ++ show pid)
threadDelay 2000000
return BrokeConnection
semantics h (FixConnection (port, ph)) = do
hPutStrLn h ("Fix connection, port: " ++ show port)
Just pid <- getPid (opaque ph)
callCommand ("fiu-ctrl -c \"disable name=posix/io/net/send\" " ++ show pid)
callCommand ("fiu-ctrl -c \"disable name=posix/io/net/recv\" " ++ show pid)
threadDelay 2000000
return FixedConnection
generator :: Model Symbolic -> Gen (Action Symbolic)
generator Model {..}
| length nodes < 3 =
if started
then flip SpawnNode Existing <$> elements ([3000..3002] \\ map fst nodes)
else flip SpawnNode Fresh <$> elements ([3000..3002] \\ map fst nodes)
| otherwise =
case client of
Nothing -> SpawnClient <$> elements [3003..3010]
Just (chs, _) ->
case value of
Nothing -> Set chs <$> arbitrary
Just _
| length isolated <= 1 -> frequency $
[ (1, Set chs <$> arbitrary)
, (5, pure (Incr chs))
, (3, pure (Read chs))
, (1, KillNode <$> elements nodes)
, (1, BreakConnection <$> elements nodes)
] ++ case isolated of
[] -> []
_ -> [(1, FixConnection <$> elements isolated)]
| otherwise ->
let notIsolated = filter (\(p,_) -> not (p `elem` map fst isolated)) nodes
in frequency $
[ (1, KillNode <$> elements nodes)
] ++ case notIsolated of
[] -> []
_ -> [(1, BreakConnection <$> elements notIsolated )]
++ case isolated of
[] -> []
_ -> [(1, FixConnection <$> elements isolated)]
shrinker :: Action Symbolic -> [Action Symbolic]
shrinker (Set cph i) = [ Set cph i' | i' <- shrink i ]
shrinker _ = []
mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
mock _m SpawnNode {} = SpawnedNode <$> genSym
mock _m SpawnClient {} = SpawnedClient <$> (ClientHandleRefs <$> genSym <*> genSym) <*> genSym
mock _m KillNode {} = pure Ack
mock _m Set {} = pure Ack
mock _m Read {} = pure (Value (Right 0))
mock _m Incr {} = pure Ack
mock _m BreakConnection {} = pure BrokeConnection
mock _m FixConnection {} = pure FixedConnection
setup :: IO Handle
setup = do
removePathForcibly "/tmp/raft-log.txt"
h <- openFile "/tmp/raft-log.txt" WriteMode
hSetBuffering h NoBuffering
return h
sm :: Handle -> StateMachine Model Action IO Response
sm h = StateMachine initModel transition precondition postcondition
Nothing generator Nothing shrinker (semantics h) mock
prop_sequential :: Property
prop_sequential = withMaxSuccess 10 $ noShrinking $
forAllCommands (sm undefined) (Just 20) $ \cmds -> monadicIO $ do
h <- liftIO setup
let sm' = sm h
(hist, model, res) <- runCommands sm' cmds
prettyCommands sm' hist (res === Ok)
liftIO (hClose h)
-- Terminate node processes
liftIO (mapM_ (terminateProcess . opaque . snd) (nodes model))
-- Terminate client process
case client model of
Nothing -> pure ()
Just (ClientHandleRefs chin chout, cph) -> do
liftIO (terminateProcess (opaque cph))
liftIO (hClose (opaque chin) >> hClose (opaque chout))
------------------------------------------------------------------------
runMany :: Commands Action -> Handle -> Property
runMany cmds log = monadicIO $ do
(hist, model, res) <- runCommands (sm log) cmds
prettyCommands (sm log) hist (res === Ok)
-- Terminate node processes
liftIO (mapM_ (terminateProcess . opaque . snd) (nodes model))
-- Terminate client process
case client model of
Nothing -> pure ()
Just (ClientHandleRefs chin chout, cph) -> do
liftIO (terminateProcess (opaque cph))
liftIO (hClose (opaque chin) >> hClose (opaque chout))
-------------------------------------------------------------------------------
-- unit_exampleUnit :: IO ()
-- unit_exampleUnit = bracket setup hClose (verboseCheck . exampleUnit)
--
-- exampleUnit :: Handle -> Property
-- exampleUnit = runMany cmds
-- where
-- cmds = Commands
-- [ -- Commands go here...
-- ]