content: {-# LANGUAGE DerivingStrategies #-}
  {-# LANGUAGE FlexibleContexts   #-}
  {-# LANGUAGE StandaloneDeriving #-}
  
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Test.StateMachine.Types.History
  -- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
  -- License     :  BSD-style (see the file LICENSE)
  --
  -- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
  -- Stability   :  provisional
  -- Portability :  non-portable (GHC extensions)
  --
  -- This module contains the notion of a history of an execution of a
  -- (parallel) program.
  --
  -----------------------------------------------------------------------------
  
  module Test.StateMachine.Types.History
    ( History(..)
    , History'
    , Pid(..)
    , HistoryEvent(..)
    , Operation(..)
    , makeOperations
    , interleavings
    , operationsPath
    , completeHistory
    )
    where
  
  import           Data.List
                     ((\\))
  import           Data.Set
                     (Set)
  import           Data.Tree
                     (Forest, Tree(Node))
  import           Prelude
  
  import           Test.StateMachine.Types.References
  
  ------------------------------------------------------------------------
  
  newtype History cmd resp = History
    { unHistory :: History' cmd resp }
  
  deriving stock instance (Eq (cmd Concrete), Eq (resp Concrete)) =>
    Eq (History cmd resp)
  
  deriving stock instance (Show (cmd Concrete), Show (resp Concrete)) =>
    Show (History cmd resp)
  
  type History' cmd resp = [(Pid, HistoryEvent cmd resp)]
  
  newtype Pid = Pid { unPid :: Int }
    deriving stock (Eq, Show, Ord)
  
  data HistoryEvent cmd resp
    = Invocation !(cmd  Concrete) !(Set Var)
    | Response   !(resp Concrete)
    | Exception  !String
  
  deriving stock instance (Eq (cmd Concrete), Eq (resp Concrete)) =>
    Eq (HistoryEvent cmd resp)
  
  deriving stock instance (Show (cmd Concrete), Show (resp Concrete)) =>
    Show (HistoryEvent cmd resp)
  
  ------------------------------------------------------------------------
  
  takeInvocations :: History' cmd resp -> [(Pid, cmd Concrete)]
  takeInvocations []                               = []
  takeInvocations ((pid, Invocation cmd _) : hist) = (pid, cmd) : takeInvocations hist
  takeInvocations ((_,   Response _)       : _)    = []
  takeInvocations ((_,   Exception _)      : _)    = []
  
  findResponse :: Pid -> History' cmd resp -> [(resp Concrete, History' cmd resp)]
  findResponse _   []                                         = []
  findResponse pid ((pid', Response resp) : es) | pid == pid' = [(resp, es)]
  findResponse pid (e                     : es)               =
    [ (resp, e : es') | (resp, es') <- findResponse pid es ]
  
  ------------------------------------------------------------------------
  
  -- | An operation packs up an invocation event with its corresponding
  --   response event.
  data Operation cmd resp
    = Operation (cmd Concrete) (resp Concrete) Pid
    | Crash     (cmd Concrete) String Pid
  
  deriving stock instance (Show (cmd Concrete), Show (resp Concrete)) =>
    Show (Operation cmd resp)
  
  -- | Given a sequential history, group invocation and response events into
  --   operations.
  makeOperations :: History' cmd resp -> [Operation cmd resp]
  makeOperations [] = []
  makeOperations [(pid1, Invocation cmd _), (pid2, Exception err)]
    | pid1 == pid2 = [Crash cmd err pid1]
    | otherwise    = error "makeOperations: impossible, pid mismatch."
  makeOperations ((pid1, Invocation cmd _) : (pid2, Response resp) : hist)
    | pid1 == pid2 = Operation cmd resp pid1 : makeOperations hist
    | otherwise    = error "makeOperations: impossible, pid mismatch."
  makeOperations _ = error "makeOperations: impossible."
  
  -- | Given a parallel history, return all possible interleavings of invocations
  --   and corresponding response events.
  interleavings :: History' cmd resp -> Forest (Operation cmd resp)
  interleavings [] = []
  interleavings es =
    [ Node (Operation cmd resp pid) (interleavings es')
    | (pid, cmd)  <- takeInvocations es
    , (resp, es') <- findResponse pid (filter1 (not . matchInvocation pid) es)
    ]
    where
      matchInvocation pid (pid', Invocation _ _) = pid == pid'
      matchInvocation _   _                      = False
  
      filter1 :: (a -> Bool) -> [a] -> [a]
      filter1 _ []                   = []
      filter1 p (x : xs) | p x       = x : filter1 p xs
                         | otherwise = xs
  
  operationsPath :: Forest (Operation cmd resp) -> [Operation cmd resp]
  operationsPath = go []
      where
        go :: [a] -> Forest a -> [a]
        go acc []             = reverse acc
        go acc (Node a f : _) = go (a:acc) f
  
  ------------------------------------------------------------------------
  
  crashingInvocations :: History' cmd resp -> History' cmd resp
  crashingInvocations = go [] [] . reverse
    where
      go :: [Pid] -> History' cmd resp -> History' cmd resp -> History' cmd resp
      go _crashedPids crashedInvs [] = reverse crashedInvs
      go  crashedPids crashedInvs ((pid, Exception _err) : es)
        | pid `elem` crashedPids = error "impossible, a process cannot crash more than once."
        | otherwise              = go (pid : crashedPids) crashedInvs es
      go crashedPids crashedInvs (e@(pid, Invocation {}) : es)
        | pid `elem` crashedPids = go (crashedPids \\ [pid]) (e : crashedInvs) es
        | otherwise              = go crashedPids crashedInvs es
      go crashedPids crashedInvs ((_pid, Response {}) : es) =
        go crashedPids crashedInvs es
  
  completeHistory :: (cmd Concrete -> resp Concrete) -> History cmd resp
                  -> History cmd resp
  completeHistory complete hist = History (hist' ++ resps)
    where
      hist' = unHistory hist
      resps = [ (pid, Response (complete cmd))
              | (pid, Invocation cmd _vars) <- crashingInvocations hist'
              ]
  