{-# 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
  { 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
(Pid -> Pid -> Bool) -> (Pid -> Pid -> Bool) -> Eq Pid
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
(Int -> Pid -> ShowS)
-> (Pid -> String) -> ([Pid] -> ShowS) -> Show Pid
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
Eq Pid
-> (Pid -> Pid -> Ordering)
-> (Pid -> Pid -> Bool)
-> (Pid -> Pid -> Bool)
-> (Pid -> Pid -> Bool)
-> (Pid -> Pid -> Bool)
-> (Pid -> Pid -> Pid)
-> (Pid -> Pid -> Pid)
-> Ord 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
$cp1Ord :: Eq Pid
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 :: History' cmd resp -> [(Pid, cmd Concrete)]
takeInvocations []                               = []
takeInvocations ((Pid
pid, Invocation cmd Concrete
cmd Set Var
_) : History' cmd resp
hist) = (Pid
pid, cmd Concrete
cmd) (Pid, cmd Concrete)
-> [(Pid, cmd Concrete)] -> [(Pid, cmd Concrete)]
forall a. a -> [a] -> [a]
: History' cmd resp -> [(Pid, cmd Concrete)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [(Pid, cmd Concrete)]
takeInvocations History' cmd resp
hist
takeInvocations ((Pid
_,   Response resp Concrete
_)       : History' cmd resp
_)    = []
takeInvocations ((Pid
_,   Exception String
_)      : History' cmd resp
_)    = []

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

    filter1 :: (a -> Bool) -> [a] -> [a]
    filter1 :: (a -> Bool) -> [a] -> [a]
filter1 a -> Bool
_ []                   = []
    filter1 a -> Bool
p (a
x : [a]
xs) | a -> Bool
p a
x       = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> Bool) -> [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 :: Forest (Operation cmd resp) -> [Operation cmd resp]
operationsPath = [Operation cmd resp]
-> Forest (Operation cmd resp) -> [Operation cmd resp]
forall a. [a] -> Forest a -> [a]
go []
    where
      go :: [a] -> Forest a -> [a]
      go :: [a] -> Forest a -> [a]
go [a]
acc []             = [a] -> [a]
forall a. [a] -> [a]
reverse [a]
acc
      go [a]
acc (Node a
a Forest a
f : Forest a
_) = [a] -> Forest a -> [a]
forall a. [a] -> Forest a -> [a]
go (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
acc) Forest a
f

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

crashingInvocations :: History' cmd resp -> History' cmd resp
crashingInvocations :: History' cmd resp -> History' cmd resp
crashingInvocations = [Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go [] [] (History' cmd resp -> History' cmd resp)
-> (History' cmd resp -> History' cmd resp)
-> History' cmd resp
-> History' cmd resp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History' cmd resp -> History' cmd resp
forall a. [a] -> [a]
reverse
  where
    go :: [Pid] -> History' cmd resp -> History' cmd resp -> History' cmd resp
    go :: [Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go [Pid]
_crashedPids History' cmd resp
crashedInvs [] = History' cmd resp -> History' cmd resp
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 Pid -> [Pid] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Pid]
crashedPids = String -> History' cmd resp
forall a. HasCallStack => String -> a
error String
"impossible, a process cannot crash more than once."
      | Bool
otherwise              = [Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go (Pid
pid Pid -> [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 Pid -> [Pid] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Pid]
crashedPids = [Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
go ([Pid]
crashedPids [Pid] -> [Pid] -> [Pid]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Pid
pid]) ((Pid, HistoryEvent cmd resp)
e (Pid, HistoryEvent cmd resp)
-> History' cmd resp -> History' cmd resp
forall a. a -> [a] -> [a]
: History' cmd resp
crashedInvs) History' cmd resp
es
      | Bool
otherwise              = [Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
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) =
      [Pid]
-> History' cmd resp -> History' cmd resp -> History' cmd resp
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 :: (cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist = History' cmd resp -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History (History' cmd resp
hist' History' cmd resp -> History' cmd resp -> History' cmd resp
forall a. [a] -> [a] -> [a]
++ History' cmd resp
forall (cmd :: (* -> *) -> *). [(Pid, HistoryEvent cmd resp)]
resps)
  where
    hist' :: History' cmd resp
hist' = History cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory History cmd resp
hist
    resps :: [(Pid, HistoryEvent cmd resp)]
resps = [ (Pid
pid, resp Concrete -> HistoryEvent cmd resp
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) <- History' cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History' cmd resp
crashingInvocations History' cmd resp
hist'
            ]