content: {-# LANGUAGE DeriveAnyClass       #-}
  {-# LANGUAGE DeriveGeneric        #-}
  {-# LANGUAGE DeriveTraversable    #-}
  {-# LANGUAGE DerivingStrategies   #-}
  {-# LANGUAGE FlexibleContexts     #-}
  {-# LANGUAGE FlexibleInstances    #-}
  {-# LANGUAGE PackageImports       #-}
  {-# LANGUAGE PolyKinds            #-}
  {-# LANGUAGE RankNTypes           #-}
  {-# LANGUAGE RecordWildCards      #-}
  {-# LANGUAGE ScopedTypeVariables  #-}
  {-# LANGUAGE StandaloneDeriving   #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  module RQlite (
        Level (..)
      , prop_sequential_rqlite
      , prop_parallel_rqlite
      , prop_nparallel_rqlite
      , runCmds
      ) where
  
  import           Control.Concurrent
                     (threadDelay)
  import           Control.Concurrent.MVar
  import           Control.Exception
                     (bracketOnError, try)
  import           Control.Monad
                     (void, when)
  import           Control.Monad.IO.Class
                     (liftIO)
  import           Data.Aeson                         hiding
                     (Result)
  import           Data.Foldable
  import           Data.Functor.Classes
  import           Data.Kind
  import           Data.List
  import           Data.Map
                     (Map)
  import qualified Data.Map                           as M
  import           Data.Maybe
  import           Data.TreeDiff
  import           GHC.Generics
  import           Prelude
  import           "hs-rqlite" Rqlite
  import           "hs-rqlite" Rqlite.Status
  import           System.Directory
  import           System.IO
  import           System.Process
  import           System.Random
  import           Test.QuickCheck                    hiding
                     (Result)
  import           Test.QuickCheck.Monadic
  import           Test.StateMachine
  import           Test.StateMachine.DotDrawing
  import           Test.StateMachine.Types
                     (History(..), ParallelCommandsF(..), interleavings)
  import qualified Test.StateMachine.Types.Rank2      as Rank2
  import           Test.StateMachine.Types.References
  
  ------------------------------------------------------------------------
  
  newtype At t r = At { unAt :: t (NodeRef r) }
    deriving stock (Generic)
  
  instance Show (t (NodeRef r)) => Show (At t r) where
    show = show . unAt
  
  data Person = Person
    { name :: String
    , age  :: Int
    }
    deriving stock (Show, Read, Eq, Generic)
  
  -- HTTP requests utilities
  
  instance FromJSON Person where
      parseJSON j = do
          (n, a) <- parseJSON j
          return $ Person n a
  
  createQ :: String
  createQ =  "CREATE TABLE Person (name text, age Int)"
  
  insertQuery :: String -> Person -> IO PostResult
  insertQuery host Person{..} =
      postQuery True host $ "INSERT INTO Person(name, age) VALUES('" ++ name ++ "', " ++ show age ++ ")"
  
  selectQuery :: Maybe Level -> String -> IO (GetResult Person)
  selectQuery lvl host = do
      putStrLnM $ "querying " ++ host
      getQuery lvl host True "SELECT * FROM Person"
  
  createQuery :: String -> IO PostResult
  createQuery host = postQuery True host createQ
  
  ------------------------
  
  -- Docker utilities
  
  data Container = Container {
          counter  :: Int
        , cn       :: Int
        , nodeName :: String
        , cport    :: Int
  } deriving stock (Generic)
  
  instance Eq Container where
      n1 == n2 = counter n1 == counter n2
  
  instance Show Container where
      show Container{..} = "Node@" ++ show cport
  
  instance ToExpr Container where
      toExpr Container{..} = App ("Node@" ++ show cport) []
  
  ignoreIOError :: IO a -> IO ()
  ignoreIOError action = do
      (_ :: Either IOError a) <- try action
      return ()
  
  stopContainer :: String -> IO ()
  stopContainer ndName = do
      stdErr <- openFile "/dev/null" AppendMode
      -- stopping or removing a non-existing container should be a no-op
      ignoreIOError $ readCreateProcess (proc "docker"
        [ "stop"
        , ndName
        ]) {std_err = UseHandle stdErr}
        ""
      ignoreIOError $ readCreateProcess (proc "docker"
        [ "rm"
        , ndName
        ]) {std_err = UseHandle stdErr}
        ""
  
  mkNodeTime :: Int -> Int -> Timeout -> Timeout -> Maybe Int -> IO Container
  mkNodeTime c n timeout elTimeout mjoin = do
      (ndName, p) <- setupNode n timeout elTimeout mjoin
      return $ Container c n ndName p
  
  stopNode :: Container -> IO ()
  stopNode Container {..} = stopContainer nodeName
  
  setupNode :: Int -> Timeout -> Timeout -> Maybe Int -> IO (String, Int)
  setupNode n timeout elTimeout mjoin = do
    r :: Word <- randomIO
    let p   = leaderPort + 2 * n
        p'  = 4002 + 2 * n
        ip  = "172.19.0." ++ show (10 + n) -- http
        ip' = "172.18.0." ++ show (10 + n)
        mjoin' = fmap (\j -> "http://" ++ httpHost j) mjoin
        ndName = mkNodeName r
        jls = case mjoin' of
          Nothing   -> []
          Just join -> ["-join", join]
    stopContainer ndName
  
    void $ readProcess "docker"
          ([ "create"
          , "--net"
          , "rqlite-http"
          , "--ip"
          , ip
          , "-p"
          , show p ++ ":" ++ show p
          , "--name"
          , ndName
          , "rqlite/rqlite:4.5.0"
          , "-http-addr"
          , ip ++ ":" ++ show p
          , "-raft-addr"
          , ip' ++ ":" ++ show p'
          , "-raft-timeout"
          , show timeout
          , "-raft-election-timeout"
          , show elTimeout
          ] ++ jls) ""
  
    -- connect the container to the rqlite network.
    void $ readProcess "docker"
          [ "network"
          , "connect"
          , "--ip"
          , ip'
          , "rqlite-network"
          , ndName
          ] ""
  
    stdOut' <- openFile (testPath ++ "/out-" ++ show n) AppendMode
    stdErr' <- openFile (testPath ++ "/err-" ++ show n) AppendMode
    stdIn'  <- openFile "/dev/null" ReadMode
    -- we don't use readProcess here, because we don't want to block.
    void $ createProcess (proc "docker"
          [ "start"
          , "-a" -- this attaches the stdout and stderr to the one we specify.
          , ndName
          ]) {std_in = UseHandle stdIn', std_out = UseHandle stdOut', std_err = UseHandle stdErr'}
  
    putStrLnM "RAN"
    return (ndName, p)
  
  
  pauseNode :: Container -> IO ()
  pauseNode Container{..} =
      void $ readProcess "docker"
          [ "pause"
          , nodeName
          ] ""
  
  unPauseNode :: Container -> IO ()
  unPauseNode Container{..} =
      void $ readProcess "docker"
          [ "unpause"
          , nodeName
          ] ""
  
  mkNodeName :: Word -> String
  mkNodeName n = "rqlite-node-" ++ show n
  
  disconnectNode :: String -> IO ()
  disconnectNode ndName =
      void $ readProcess "docker"
          [ "network"
          , "disconnect"
          , "rqlite-network"
          , ndName
          ] ""
  
  connectNode :: Container -> IO ()
  connectNode Container {..} =
      void $ readProcess "docker"
          [ "network"
          , "connect"
          , "--ip"
          , "172.18.0." ++ show (10 + cn)
          , "rqlite-network"
          , nodeName
          ] ""
  
  createRQNetworks :: IO ()
  createRQNetworks = do
      -- this way we don't "polute" test output with messages (i.e. network
      -- may already be present).
      stdErr  <- openFile "/dev/null" AppendMode
      void $ ignoreIOError $ readCreateProcess (proc "docker"
          [ "network"
          , "create"
          , "--subnet"
          , "172.19.0.0/16"
          , "rqlite-http"]) {std_err = UseHandle stdErr}
          ""
      void $ ignoreIOError $ readCreateProcess (proc "docker"
          [ "network"
          , "create"
          , "--subnet"
          , "172.18.0.0/16"
          , "rqlite-network"]) {std_err = UseHandle stdErr}
          ""
  
  -- retryUntilElections :: IO a -> IO a
  -- retryUntilElections action = go 20
  --     where
  --     go n = do
  --         res <- try action
  --         let retry e = if n > 0 then do
  --                 putStrLnM "LeadershipLost. Retrying"
  --                 threadDelay 500000
  --                 go (n-1)
  --             else throwIO e
  --         case res of
  --             Right a -> return a
  --             Left e@(LeadershipLost _) -> retry e
  --             Left e@NotLeader -> retry e
  --             Left e -> throwIO e
  
  
  ------------------------
  
  sameElements :: Eq a => [a] -> [a] -> Bool
  sameElements x y = null (x \\ y) && null (y \\ x)
  
  type NodeRef =  Reference Container
  
  data Model r = Model {
          dbModel :: DBModel
        , nodes   :: [(NodeRef r, Int)]
        } deriving stock (Generic, Show)
  
  data DBModel = DBModel {
        persons   :: [Person]
      , nodeState :: Map Int NodeState
      , cutLines  :: [(Int, Int)]
      , cWhere    :: Int
      , cRef      :: Int
      } deriving stock (Generic, Show)
  
  type Join = Maybe Int
  
  data Timeout =
        Ms Int
      | Sec Int
  
  instance Show Timeout where
      show (Ms n)  = show n ++ "ms"
      show (Sec n) = show n ++ "s"
  
  data Cmd node =
        Spawn Int Timeout Timeout Join
      | ReSpawn Int Int Timeout Timeout Join
      | Disconnect node
      | Connect node
      | Stop node
      | Insert node Person
      | Get node (Maybe Level)
      | Pause node
      | UnPause node
      | Delay Int
      deriving stock (Generic, Show, Functor, Foldable, Traversable)
  
  newtype Resp node = Resp (Either SomeError (Success node))
      deriving stock (Show, Eq, Functor, Foldable, Traversable, Generic)
  
  newtype SomeError = SomeError String
      deriving stock (Show, Eq)
  
  data Success node =
        Unit
      | Spawned node
      | Got [Person]
      deriving stock (Show, Functor, Foldable, Traversable, Generic)
  
  deriving stock    instance Generic1          (At Cmd)
  deriving anyclass instance Rank2.Functor     (At Cmd)
  deriving anyclass instance Rank2.Foldable    (At Cmd)
  deriving anyclass instance Rank2.Traversable (At Cmd)
  
  deriving anyclass instance ToExpr DBModel
  deriving anyclass instance ToExpr (Model Concrete)
  deriving anyclass instance ToExpr Person
  
  deriving stock    instance Generic1          (At Resp)
  deriving anyclass instance Rank2.Functor     (At Resp)
  deriving anyclass instance Rank2.Foldable    (At Resp)
  deriving anyclass instance Rank2.Traversable (At Resp)
  
  instance Eq node => Eq (Success node) where
      Unit == Unit          = True
      (Got ps) == (Got ps') = sameElements ps ps'
      Spawned n == Spawned n' = n == n'
      _ == _                = False
  
  instance CommandNames (At Cmd) where
      cmdName (At Spawn {})      = "Spawn"
      cmdName (At ReSpawn {})    = "ReSpawn"
      cmdName (At Connect {})    = "Connect"
      cmdName (At Disconnect {}) = "Disconnect"
      cmdName (At Stop {})       = "Stop"
      cmdName (At Insert {})     = "Insert"
      cmdName (At Get {})        = "Get"
      cmdName (At Pause {})      = "Pause"
      cmdName (At UnPause {})    = "UnPause"
      cmdName (At Delay {})      = "Delay"
  
  unitResp :: Resp node
  unitResp = Resp (Right Unit)
  
  data Event (r :: Type -> Type) = Event
    { eventBefore   :: Model  r
    , eventCmd      :: At Cmd r
    , eventAfter    :: Model  r
    , eventMockResp :: Resp Int
    }
  
  lockstep :: forall  (r :: Type -> Type).
              (Eq1 r, Show1 r)
           => Model   r
           -> At Cmd  r
           -> At Resp r
           -> Event   r
  lockstep model@Model {..} cmd (At resp) = Event
      { eventBefore   = model
      , eventCmd      = cmd
      , eventAfter    = model'
      , eventMockResp = mockResp
      }
    where
      (mockResp, dbModel') = step model cmd
      newNodes = zip (toList resp) (toList mockResp)
      model' = Model {
            dbModel = dbModel'
          , nodes   = nodes `union'` newNodes
          }
  
  union' :: forall k v. (Eq k, Eq v, Show k, Show v)
                => [(k, v)] -- Mapping known to have duplicate keys
                -> [(k, v)] -- With potential duplicates
                -> [(k, v)]
  union' acc []             = acc
  union' acc ((k, v) : kvs) =
      case lookup k acc of
        Just v' | v /= v' -> error $ renderError v'
        _otherwise        -> union' ((k, v) : acc) kvs
    where
      renderError :: v -> String
      renderError v' = unwords [
            "Key"
          , show k
          , "with two different values"
          , show v
          , "and"
          , show v'
          ]
  
  (!) :: Eq1 r => [(NodeRef r, v)] -> NodeRef r -> v
  env ! r = case lookup r env of
              Just a  -> a
              Nothing -> error "(!): key not found"
  
  step :: Eq1 r => Model r -> At Cmd r -> (Resp Int, DBModel)
  step (Model m@DBModel{..} nodes) (At cmd) = case cmd of
      Insert _ p      -> (unitResp, m {persons = p : persons})
      Get _ _         -> (Resp $ Right $ Got $ persons, m)
      Spawn wh _ _ _  -> ( Resp $ Right $ Spawned cRef, m {
                            nodeState = M.insert cRef (Running wh) nodeState
                          , cWhere = wh + 1 -- while shrinking, node locations may not be consecutive.
                          , cRef = cRef + 1
                          })
      ReSpawn pRef wh _ _ _ ->
                          ( Resp $ Right $ Spawned cRef, m {
                            nodeState = M.union (M.fromList [(cRef, Running wh), (pRef, Done)]) nodeState
                          , cRef = cRef + 1
                          })
      Connect ref       -> (unitResp, m {
                            nodeState = M.update connectST (nodes ! ref) nodeState
                          })
      Disconnect ref    -> (unitResp, m {
                            nodeState = M.update disconnectST (nodes ! ref) nodeState
                          })
      Stop ref          -> (unitResp, m {
                            nodeState = M.update stopST (nodes ! ref) nodeState
                          })
      Pause ref         -> (unitResp, m {
                            nodeState = M.update pauseST (nodes ! ref) nodeState
                          })
      UnPause ref         -> (unitResp, m {
                            nodeState = M.update unPauseST (nodes ! ref) nodeState
                          })
      Delay _           -> (unitResp, m)
  
  data NodeState
    = Running Int
    | Disconnected Int
    | Stopped Int
    | Paused Int
    | Done
    deriving stock (Show, Generic)
    deriving anyclass ToExpr
  
  connectST :: NodeState -> Maybe NodeState
  connectST (Disconnected wh) = Just $ Running wh
  connectST st = error $ "is not dicsonnected but " ++ show st
  
  disconnectST :: NodeState -> Maybe NodeState
  disconnectST (Running wh) = Just $ Disconnected wh
  disconnectST st           = error $ "is not running but " ++ show st
  
  stopST :: NodeState -> Maybe NodeState
  stopST (Running wh) = Just $ Stopped wh
  stopST st           = error $ "is not running but " ++ show st
  
  pauseST :: NodeState -> Maybe NodeState
  pauseST (Running wh) = Just $ Paused wh
  pauseST st           = error $ "is not running but " ++ show st
  
  unPauseST :: NodeState -> Maybe NodeState
  unPauseST (Paused wh) = Just $ Running wh
  unPauseST st          = error $ "is not paused but " ++ show st
  
  runsMp :: Int -> Map Int NodeState -> Bool
  runsMp n mp = case M.lookup n mp of
      Just (Running _) -> True
      _                -> False
  
  pausedMP :: Int -> Map Int NodeState -> Bool
  pausedMP n mp = case M.lookup n mp of
      Just (Paused _) -> True
      _               -> False
  
  disconnectedMP :: Int -> Map Int NodeState -> Bool
  disconnectedMP n mp = case M.lookup n mp of
      Just (Disconnected _) -> True
      _                     -> False
  
  stoppedMp :: Int -> Map Int NodeState -> Bool
  stoppedMp n mp = case M.lookup n mp of
      Just (Stopped _) -> True
      _                -> False
  
  getRunning :: Map Int NodeState -> [(Int, Int)]
  getRunning = mapMaybe f . M.toList
      where
          f (a, Running wh) = Just (a, wh)
          f _               = Nothing
  
  getNotRunning :: Map Int NodeState -> [Int]
  getNotRunning = mapMaybe f . M.toList
      where
          f (a, Stopped _)      = Just a
          f (a, Done)           = Just a
          f (a, Disconnected _) = Just a
          f (a, Paused _)       = Just a
          f _                   = Nothing
  
  isStopped :: NodeState -> Bool
  isStopped (Stopped _) = True
  isStopped _           = False
  
  isDisconnected :: NodeState -> Bool
  isDisconnected (Disconnected _) = True
  isDisconnected _                = False
  
  initModel :: Model r
  initModel = Model (DBModel [] M.empty [] 0 0) []
  
  transition :: forall r. (Eq1 r, Show1 r) => Model r -> At Cmd r -> At Resp r -> Model r
  transition model cmd =  eventAfter . lockstep model cmd
  
  precondition :: Model Symbolic -> At Cmd Symbolic -> Logic
  precondition (Model DBModel{..} nodes) (At cmd) = case cmd of
      Spawn n _ _ j
                 -> Boolean $ length (getRunning nodeState) <= 2
                           && (not (null (getRunning nodeState)) || n == 0)
                           && joinsRunning j nodeState
                           && n < 3
      ReSpawn prevRef _ _ _ j
                 -> Boolean $ elem prevRef (snd <$> nodes)
                           && stoppedMp prevRef nodeState
                           && length (getRunning nodeState) <= 2
                           && joinsRunning j nodeState
      Stop n     -> Boolean $ elem n (fst <$> nodes)
                           && runsMp (nodes ! n) nodeState
                           && nodes ! n /= 0
                           && null (getNotRunning nodeState)
                           && length (getRunning nodeState) == 3
      Disconnect n
                 -> Boolean $ elem n (fst <$> nodes)
                           && runsMp (nodes ! n) nodeState
                           && null (getNotRunning nodeState)
                           && nodes ! n /= 0
                           && length (getRunning nodeState) == 3
      Connect n  -> Boolean $ elem n (fst <$> nodes)
                           && disconnectedMP (nodes ! n) nodeState
      Insert n _ -> Boolean $ elem n (fst <$> nodes)
                           && runsMp (nodes ! n) nodeState
      Get n _    -> Boolean $ elem n (fst <$> nodes)
                           && runsMp (nodes ! n) nodeState
      Pause n    -> Boolean $ elem n (fst <$> nodes)
                           && runsMp (nodes ! n) nodeState
      UnPause n  -> Boolean $ elem n (fst <$> nodes)
                           && pausedMP (nodes ! n) nodeState
      Delay _    -> Top
  
  postcondition :: Model Concrete -> At Cmd Concrete -> At Resp Concrete -> Logic
  postcondition m@Model{..} cmd resp =
      toMock (eventAfter ev) resp .== eventMockResp ev
      where
          ev = lockstep m cmd resp
  
  toMock :: Eq1 r => Model r -> At Resp r ->  Resp Int
  toMock Model{..} (At r) = fmap
      (\n -> fromMaybe (error "could not find person ref") $ Prelude.lookup n nodes) r
  
  shrinker :: Model Symbolic -> At Cmd Symbolic -> [At Cmd Symbolic]
  shrinker _ _ = []
  
  semantics :: MVar Int -> At Cmd Concrete -> IO (At Resp Concrete)
  semantics counter (At cmd) = At . Resp <$> case cmd of
      Insert node p -> do
          _ <- insertQuery (httpHost $ cn $ concrete node) p
          return $ Right Unit
      Get node lvl -> do
          res <- selectQuery lvl $ httpHost $ cn $ concrete node
          return $ case res of
              GetResult p -> Right $ Got p
              GetError e  -> Left $ SomeError $ show e
      Spawn n t elt join -> do
              putStrLnM $ "Starting at " ++ show n ++ " joining " ++ show join
              c <- modifyMVar counter $ \m -> return (m + 1, m)
              bracketOnError (mkNodeTime c n t elt join)
                              stopNode
                              $ \rqNode -> do
                  threadDelay 500000
                  _ <- retryUntilAlive $ httpHost n
                  _ <- createQuery $ httpHost n
                  return $ Right $ Spawned $ reference rqNode
      ReSpawn n _ t elt join -> do
              putStrLnM $ "Restarting at " ++ show n ++ " joining " ++ show join
              c <- modifyMVar counter $ \m -> return (m + 1, m)
              bracketOnError (mkNodeTime c n t elt join)
                              stopNode
                              $ \rqNode -> do
                  threadDelay 500000
                  _ <- retryUntilAlive $ httpHost n
                  return $ Right $ Spawned $ reference rqNode
      Stop node -> do
          putStrLnM $ "Stopping at " ++ show (cport $ concrete node)
          stopNode $ concrete node
          return $ Right Unit
      Disconnect node -> do
          disconnectNode $ nodeName $ concrete node
          return $ Right Unit
      Connect node -> do
          connectNode $ concrete node
          _ <- retryUntilAlive $ httpHost $ cn $ concrete node
          return $ Right Unit
      Pause node -> do
          pauseNode $ concrete node
          return $ Right Unit
      UnPause node -> do
          unPauseNode $ concrete node
          return $ Right Unit
      Delay n -> do
          threadDelay n
          return $ Right Unit
  
  httpHost :: Int -> String
  httpHost n = "172.19.0." ++ show (10 + n) ++ ":" ++ show (leaderPort + 2 * n)
  
  mock :: Model Symbolic -> At Cmd Symbolic -> GenSym (At Resp Symbolic)
  mock (Model DBModel{..} _) (At cmd) = At <$> case cmd of
      Spawn {}      -> Resp . Right . Spawned <$> genSym
      ReSpawn {}    -> Resp . Right . Spawned <$> genSym
      Stop {}       -> return unitResp
      Disconnect {} -> return unitResp
      Connect {}    -> return unitResp
      Insert {}     -> return unitResp
      Get {}        -> return $ Resp $ Right $ Got persons
      Pause {}      -> return unitResp
      UnPause {}    -> return unitResp
      Delay {}      -> return unitResp
  
  sm :: MVar Int -> Maybe Level -> StateMachine Model (At Cmd) IO (At Resp)
  sm counter lvl = StateMachine initModel transition precondition postcondition
      Nothing (generatorImpl lvl) shrinker (semantics counter) mock garbageCollect
  
  prop_sequential_rqlite :: Maybe Level -> Property
  prop_sequential_rqlite lvl =
      forAllCommands (sm undefined lvl) (Just 7) $ \cmds -> checkCommandNames cmds $ monadicIO $ do
          liftIO $ do
              createRQNetworks
              removePathForcibly testPath
              createDirectory testPath
              threadDelay 10000
          c <- liftIO $ newMVar 0
          (hist, _, res) <- runCommands (sm c lvl) cmds
          prettyCommands (sm undefined lvl) hist $ res === Ok
  
  prop_parallel_rqlite :: Maybe Level -> Property
  prop_parallel_rqlite lvl =
      forAllParallelCommands (sm undefined lvl) (Just 7) $ \cmds -> checkCommandNamesParallel cmds $ monadicIO $ do
          liftIO $ do
              createRQNetworks
              removePathForcibly testPath
              createDirectory testPath
              threadDelay 10000
          c <- liftIO $ newMVar 0
          prettyParallelCommandsWithOpts cmds (Just $ GraphOptions "rqlite-test-output.png" Png)
                  =<< runParallelCommandsNTimes 2 (sm c lvl) cmds
  
  prop_nparallel_rqlite :: Int -> Maybe Level -> Property
  prop_nparallel_rqlite np lvl =
      forAllNParallelCommands (sm undefined lvl) np $ \cmds ->
        monadicIO $ do
          liftIO $ do
              removePathForcibly testPath
              createDirectory testPath
              threadDelay 10000
          c <- liftIO $ newMVar 0
          prettyNParallelCommandsWithOpts cmds (Just $ GraphOptions "rqlite-test-output.png" Png)
                  =<< runNParallelCommandsNTimes 1 (sm c lvl) cmds
  
  
  runCmds :: ParallelCommandsF [] (At Cmd) (At Resp) -> Property
  runCmds cmds = withMaxSuccess 1 $ noShrinking $ monadicIO $ do
      liftIO $ do
              removePathForcibly testPath
              createDirectory testPath
      c <- liftIO $ newMVar 0
      ls <- runNParallelCommandsNTimes 1 (sm c $ Just Weak) cmds
      prettyNParallelCommandsWithOpts cmds (Just $ GraphOptions "rqlite-test-output.png" Png) ls
      liftIO $ print $ fst $ head ls
      liftIO $ print $ interleavings $ unHistory $ fst $ head ls
  
  garbageCollect :: Model Concrete -> IO ()
  garbageCollect (Model _ nodes) =
      forM_ nodes $ \(Reference (Concrete node), p) -> do
          putStrLnM $ "stopping " ++ show p
          stopNode node
  
  generatorImpl :: Maybe Level -> Model Symbolic -> Maybe (Gen (At Cmd Symbolic))
  generatorImpl _ (Model _ [])    = Just $ return $ At initCmd
  generatorImpl lvl (Model DBModel{..} nodes) = Just $ At <$> do
      node <- fst <$> elements nodes
      let
          reconnect :: (Int, Gen (Cmd (NodeRef Symbolic)))
          reconnect = case find (isDisconnected . snd) (M.toList nodeState) of
              (Just (_, Disconnected _)) ->
                  (100, return $ Connect node)
              _                       -> (0, undefined)
      frequency
          [ (5, Insert node <$> arbitrary)
          , (5, return $ Get node lvl)
          , (if cWhere <= 3 then 20 else 0, return $ mkSpawn Nothing cWhere $ joinNode False nodeState)
          , (if cWhere == 3 then 20 else 0, return $ Stop node)
          , (if cWhere == 3 then 20 else 0, return $ Disconnect node)
          , respawn
          , reconnect]
          where
  
          respawn :: (Int, Gen (Cmd (NodeRef Symbolic)))
          respawn = case find (isStopped . snd) (M.toList nodeState) of
              (Just (ref, Stopped n)) ->
                  -- Sometimes, when a node respawns the rqlite files are not found
                  -- and the test fails. I'm not sure why this happens.
                  -- Until this is properly fixed, we disable this command.
                  (0, return $ mkSpawn (Just ref) n $ joinNode True nodeState)
              _                       -> (0, undefined)
  
  joinNode :: Bool -> Map Int NodeState -> Maybe Int
  joinNode avoid0 ndState =
      case snd <$> getRunning ndState of
          [] -> Nothing
          rs -> Just $ case (elem 0 rs, delete 0 rs, avoid0) of
              (False, _, _)     -> head rs
              (True, _, False)  -> 0
              (True, rs', True) -> head rs'
  
  joinsRunning :: Maybe Int -> Map Int NodeState -> Bool
  joinsRunning Nothing _   = True
  joinsRunning (Just n) mp = elem n $ snd <$> getRunning mp
  
  initCmd :: Cmd node
  initCmd = Spawn 0 (Sec 1) (Sec 1) Nothing
  
  mkSpawn :: Maybe Int -> Int -> Maybe Int -> Cmd node
  mkSpawn respawm n =
      (case respawm of
          Nothing  -> Spawn
          Just ref -> ReSpawn ref) n (Sec 1) (Sec 1)
  
  testPath :: String
  testPath = "rqlite-test-output"
  
  names :: [String]
  names = ["John", "Stevan", "Kostas", "Curry", "Robert"]
  
  leaderPort :: Int
  leaderPort = 4001
  
  instance Arbitrary Person where
      arbitrary = do
          n <- elements names
          a <- choose (0, 100)
          return $ Person n a
  
  putStrLnM :: String -> IO ()
  putStrLnM str = when isDebugging $ putStrLn str
  
  isDebugging :: Bool
  isDebugging = False
  