{-# 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
  { forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
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 { Pid -> Int
unPid :: Int }
  deriving stock (Pid -> Pid -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Pid -> Pid -> Bool
$c/= :: Pid -> Pid -> Bool
== :: Pid -> Pid -> Bool
$c== :: Pid -> Pid -> Bool
Eq, Int -> Pid -> ShowS
[Pid] -> ShowS
Pid -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Pid] -> ShowS
$cshowList :: [Pid] -> ShowS
show :: Pid -> String
$cshow :: Pid -> String
showsPrec :: Int -> Pid -> ShowS
$cshowsPrec :: Int -> Pid -> ShowS
Show, Eq Pid
Pid -> Pid -> Bool
Pid -> Pid -> Ordering
Pid -> Pid -> Pid
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Pid -> Pid -> Pid
$cmin :: Pid -> Pid -> Pid
max :: Pid -> Pid -> Pid
$cmax :: Pid -> Pid -> Pid
>= :: Pid -> Pid -> Bool
$c>= :: Pid -> Pid -> Bool
> :: Pid -> Pid -> Bool
$c> :: Pid -> Pid -> Bool
<= :: Pid -> Pid -> Bool
$c<= :: Pid -> Pid -> Bool
< :: Pid -> Pid -> Bool
$c< :: Pid -> Pid -> Bool
compare :: Pid -> Pid -> Ordering
$ccompare :: Pid -> Pid -> Ordering
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 :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [(Pid, cmd Concrete)]
takeInvocations []                               = []
takeInvocations ((Pid
pid, Invocation cmd Concrete
cmd Set Var
_) : [(Pid, HistoryEvent cmd resp)]
hist) = (Pid
pid, cmd Concrete
cmd) forall a. a -> [a] -> [a]
: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [(Pid, cmd Concrete)]
takeInvocations [(Pid, HistoryEvent cmd resp)]
hist
takeInvocations ((Pid
_,   Response resp Concrete
_)       : [(Pid, HistoryEvent cmd resp)]
_)    = []
takeInvocations ((Pid
_,   Exception String
_)      : [(Pid, HistoryEvent cmd resp)]
_)    = []

findResponse :: Pid -> History' cmd resp -> [(resp Concrete, History' cmd resp)]
findResponse :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Pid -> History' cmd resp -> [(resp Concrete, History' cmd resp)]
findResponse Pid
_   []                                         = []
findResponse Pid
pid ((Pid
pid', Response resp Concrete
resp) : [(Pid, HistoryEvent cmd resp)]
es) | Pid
pid forall a. Eq a => a -> a -> Bool
== Pid
pid' = [(resp Concrete
resp, [(Pid, HistoryEvent cmd resp)]
es)]
findResponse Pid
pid ((Pid, HistoryEvent cmd resp)
e                     : [(Pid, HistoryEvent cmd resp)]
es)               =
  [ (resp Concrete
resp, (Pid, HistoryEvent cmd resp)
e forall a. a -> [a] -> [a]
: [(Pid, HistoryEvent cmd resp)]
es') | (resp Concrete
resp, [(Pid, HistoryEvent cmd resp)]
es') <- forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Pid -> History' cmd resp -> [(resp Concrete, History' cmd resp)]
findResponse Pid
pid [(Pid, HistoryEvent cmd resp)]
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 :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [Operation cmd resp]
makeOperations [] = []
makeOperations [(Pid
pid1, Invocation cmd Concrete
cmd Set Var
_), (Pid
pid2, Exception String
err)]
  | Pid
pid1 forall a. Eq a => a -> a -> Bool
== Pid
pid2 = [forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Concrete -> String -> Pid -> Operation cmd resp
Crash cmd Concrete
cmd String
err Pid
pid1]
  | Bool
otherwise    = forall a. HasCallStack => String -> a
error String
"makeOperations: impossible, pid mismatch."
makeOperations ((Pid
pid1, Invocation cmd Concrete
cmd Set Var
_) : (Pid
pid2, Response resp Concrete
resp) : [(Pid, HistoryEvent cmd resp)]
hist)
  | Pid
pid1 forall a. Eq a => a -> a -> Bool
== Pid
pid2 = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Concrete -> resp Concrete -> Pid -> Operation cmd resp
Operation cmd Concrete
cmd resp Concrete
resp Pid
pid1 forall a. a -> [a] -> [a]
: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [Operation cmd resp]
makeOperations [(Pid, HistoryEvent cmd resp)]
hist
  | Bool
otherwise    = forall a. HasCallStack => String -> a
error String
"makeOperations: impossible, pid mismatch."
makeOperations [(Pid, HistoryEvent cmd resp)]
_ = forall a. HasCallStack => String -> a
error String
"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 :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> Forest (Operation cmd resp)
interleavings [] = []
interleavings [(Pid, HistoryEvent cmd resp)]
es =
  [ forall a. a -> [Tree a] -> Tree a
Node (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Concrete -> resp Concrete -> Pid -> Operation cmd resp
Operation cmd Concrete
cmd resp Concrete
resp Pid
pid) (forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> Forest (Operation cmd resp)
interleavings [(Pid, HistoryEvent cmd resp)]
es')
  | (Pid
pid, cmd Concrete
cmd)  <- forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [(Pid, cmd Concrete)]
takeInvocations [(Pid, HistoryEvent cmd resp)]
es
  , (resp Concrete
resp, [(Pid, HistoryEvent cmd resp)]
es') <- forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Pid -> History' cmd resp -> [(resp Concrete, History' cmd resp)]
findResponse Pid
pid (forall a. (a -> Bool) -> [a] -> [a]
filter1 (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {cmd :: (* -> *) -> *} {resp :: (* -> *) -> *}.
Eq a =>
a -> (a, HistoryEvent cmd resp) -> Bool
matchInvocation Pid
pid) [(Pid, HistoryEvent cmd resp)]
es)
  ]
  where
    matchInvocation :: a -> (a, HistoryEvent cmd resp) -> Bool
matchInvocation a
pid (a
pid', Invocation cmd Concrete
_ Set Var
_) = a
pid forall a. Eq a => a -> a -> Bool
== a
pid'
    matchInvocation a
_   (a, HistoryEvent cmd resp)
_                      = Bool
False

    filter1 :: (a -> Bool) -> [a] -> [a]
    filter1 :: forall a. (a -> Bool) -> [a] -> [a]
filter1 a -> Bool
_ []                   = []
    filter1 a -> Bool
p (a
x : [a]
xs) | a -> Bool
p a
x       = a
x forall a. a -> [a] -> [a]
: forall a. (a -> Bool) -> [a] -> [a]
filter1 a -> Bool
p [a]
xs
                       | Bool
otherwise = [a]
xs

operationsPath :: Forest (Operation cmd resp) -> [Operation cmd resp]
operationsPath :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Forest (Operation cmd resp) -> [Operation cmd resp]
operationsPath = forall a. [a] -> Forest a -> [a]
go []
    where
      go :: [a] -> Forest a -> [a]
      go :: forall a. [a] -> Forest a -> [a]
go [a]
acc []             = forall a. [a] -> [a]
reverse [a]
acc
      go [a]
acc (Node a
a [Tree a]
f : [Tree a]
_) = forall a. [a] -> Forest a -> [a]
go (a
aforall a. a -> [a] -> [a]
:[a]
acc) [Tree a]
f

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

crashingInvocations :: History' cmd resp -> History' cmd resp
crashingInvocations :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History' cmd resp
crashingInvocations = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go [] [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse
  where
    go :: [Pid] -> History' cmd resp -> History' cmd resp -> History' cmd resp
    go :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go [Pid]
_crashedPids History' cmd resp
crashedInvs [] = forall a. [a] -> [a]
reverse History' cmd resp
crashedInvs
    go  [Pid]
crashedPids History' cmd resp
crashedInvs ((Pid
pid, Exception String
_err) : History' cmd resp
es)
      | Pid
pid forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Pid]
crashedPids = forall a. HasCallStack => String -> a
error String
"impossible, a process cannot crash more than once."
      | Bool
otherwise              = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go (Pid
pid forall a. a -> [a] -> [a]
: [Pid]
crashedPids) History' cmd resp
crashedInvs History' cmd resp
es
    go [Pid]
crashedPids History' cmd resp
crashedInvs (e :: (Pid, HistoryEvent cmd resp)
e@(Pid
pid, Invocation {}) : History' cmd resp
es)
      | Pid
pid forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Pid]
crashedPids = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go ([Pid]
crashedPids forall a. Eq a => [a] -> [a] -> [a]
\\ [Pid
pid]) ((Pid, HistoryEvent cmd resp)
e forall a. a -> [a] -> [a]
: History' cmd resp
crashedInvs) History' cmd resp
es
      | Bool
otherwise              = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go [Pid]
crashedPids History' cmd resp
crashedInvs History' cmd resp
es
    go [Pid]
crashedPids History' cmd resp
crashedInvs ((Pid
_pid, Response {}) : History' cmd resp
es) =
      forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go [Pid]
crashedPids History' cmd resp
crashedInvs History' cmd resp
es

completeHistory :: (cmd Concrete -> resp Concrete) -> History cmd resp
                -> History cmd resp
completeHistory :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History ([(Pid, HistoryEvent cmd resp)]
hist' forall a. [a] -> [a] -> [a]
++ forall {cmd :: (* -> *) -> *}. [(Pid, HistoryEvent cmd resp)]
resps)
  where
    hist' :: [(Pid, HistoryEvent cmd resp)]
hist' = forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory History cmd resp
hist
    resps :: [(Pid, HistoryEvent cmd resp)]
resps = [ (Pid
pid, forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
resp Concrete -> HistoryEvent cmd resp
Response (cmd Concrete -> resp Concrete
complete cmd Concrete
cmd))
            | (Pid
pid, Invocation cmd Concrete
cmd Set Var
_vars) <- forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History' cmd resp
crashingInvocations [(Pid, HistoryEvent cmd resp)]
hist'
            ]