{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DerivingStrategies  #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Test.StateMachine.Labelling
-- Copyright   :  (C) 2019, Edsko de Vries
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module exports helpers that are useful for labelling properties.
--
-----------------------------------------------------------------------------

module Test.StateMachine.Labelling
  ( Predicate(..)
  , predicate
  , maximum
  , classify
  , Event(..)
  , execCmds
  , execHistory
  )
  where

import           Data.Either
                   (partitionEithers)
import           Data.Kind
                   (Type)
import           Data.Maybe
                   (mapMaybe)
import           Prelude                 hiding
                   (maximum)

import           Test.StateMachine.Types
                   (Command(..), Commands(..), Concrete, History,
                   Operation(..), StateMachine(..), Symbolic,
                   makeOperations, unHistory)

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

data Predicate a b = Predicate {
    -- | Given an @a@, either successfully classify as @b@ or continue looking
    Predicate a b -> a -> Either b (Predicate a b)
predApply  :: a -> Either b (Predicate a b)

    -- | End of the string
    --
    -- The predicate is given a final chance to return a value.
  , Predicate a b -> Maybe b
predFinish :: Maybe b
  }

instance Functor (Predicate a) where
  fmap :: (a -> b) -> Predicate a a -> Predicate a b
fmap a -> b
f Predicate{Maybe a
a -> Either a (Predicate a a)
predFinish :: Maybe a
predApply :: a -> Either a (Predicate a a)
predFinish :: forall a b. Predicate a b -> Maybe b
predApply :: forall a b. Predicate a b -> a -> Either b (Predicate a b)
..} = Predicate :: forall a b.
(a -> Either b (Predicate a b)) -> Maybe b -> Predicate a b
Predicate {
        predApply :: a -> Either b (Predicate a b)
predApply  = (a -> Either b (Predicate a b))
-> (Predicate a a -> Either b (Predicate a b))
-> Either a (Predicate a a)
-> Either b (Predicate a b)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> Either b (Predicate a b)
forall a b. a -> Either a b
Left (b -> Either b (Predicate a b))
-> (a -> b) -> a -> Either b (Predicate a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) (Predicate a b -> Either b (Predicate a b)
forall a b. b -> Either a b
Right (Predicate a b -> Either b (Predicate a b))
-> (Predicate a a -> Predicate a b)
-> Predicate a a
-> Either b (Predicate a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> Predicate a a -> Predicate a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) (Either a (Predicate a a) -> Either b (Predicate a b))
-> (a -> Either a (Predicate a a)) -> a -> Either b (Predicate a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either a (Predicate a a)
predApply
      , predFinish :: Maybe b
predFinish = a -> b
f (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
predFinish
      }

-- | Construct simply predicate that returns 'Nothing' on termination
predicate :: (a -> Either b (Predicate a b)) -> Predicate a b
predicate :: (a -> Either b (Predicate a b)) -> Predicate a b
predicate a -> Either b (Predicate a b)
f = (a -> Either b (Predicate a b)) -> Maybe b -> Predicate a b
forall a b.
(a -> Either b (Predicate a b)) -> Maybe b -> Predicate a b
Predicate a -> Either b (Predicate a b)
f Maybe b
forall a. Maybe a
Nothing

-- | Maximum value found, if any
maximum :: forall a b. Ord b => (a -> Maybe b) -> Predicate a b
maximum :: (a -> Maybe b) -> Predicate a b
maximum a -> Maybe b
f = Maybe b -> Predicate a b
go Maybe b
forall a. Maybe a
Nothing
  where
    go :: Maybe b -> Predicate a b
    go :: Maybe b -> Predicate a b
go Maybe b
maxSoFar = Predicate :: forall a b.
(a -> Either b (Predicate a b)) -> Maybe b -> Predicate a b
Predicate {
          predApply :: a -> Either b (Predicate a b)
predApply  = Predicate a b -> Either b (Predicate a b)
forall a b. b -> Either a b
Right (Predicate a b -> Either b (Predicate a b))
-> (a -> Predicate a b) -> a -> Either b (Predicate a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe b -> Predicate a b
go (Maybe b -> Predicate a b) -> (a -> Maybe b) -> a -> Predicate a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe b -> Maybe b -> Maybe b
upd Maybe b
maxSoFar (Maybe b -> Maybe b) -> (a -> Maybe b) -> a -> Maybe b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
f
        , predFinish :: Maybe b
predFinish = Maybe b
maxSoFar
        }

    upd :: Maybe b -> Maybe b -> Maybe b
    upd :: Maybe b -> Maybe b -> Maybe b
upd Maybe b
Nothing         Maybe b
mb       = Maybe b
mb
    upd (Just b
maxSoFar) Maybe b
Nothing  = b -> Maybe b
forall a. a -> Maybe a
Just b
maxSoFar
    upd (Just b
maxSoFar) (Just b
b) = b -> Maybe b
forall a. a -> Maybe a
Just (b -> b -> b
forall a. Ord a => a -> a -> a
max b
maxSoFar b
b)

-- | Do a linear scan over the list, returning all successful classifications
classify :: forall a b. [Predicate a b] -> [a] -> [b]
classify :: [Predicate a b] -> [a] -> [b]
classify = [b] -> [Predicate a b] -> [a] -> [b]
go []
  where
    go :: [b] -> [Predicate a b] -> [a] -> [b]
    go :: [b] -> [Predicate a b] -> [a] -> [b]
go [b]
acc [Predicate a b]
ps [] = [b]
acc [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
bs
      where
        bs :: [b]
bs = (Predicate a b -> Maybe b) -> [Predicate a b] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Predicate a b -> Maybe b
forall a b. Predicate a b -> Maybe b
predFinish [Predicate a b]
ps
    go [b]
acc [Predicate a b]
ps (a
a : [a]
as) = [b] -> [Predicate a b] -> [a] -> [b]
go ([b]
acc [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b]
bs) [Predicate a b]
ps' [a]
as
      where
        ([b]
bs, [Predicate a b]
ps') = [Either b (Predicate a b)] -> ([b], [Predicate a b])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either b (Predicate a b)] -> ([b], [Predicate a b]))
-> [Either b (Predicate a b)] -> ([b], [Predicate a b])
forall a b. (a -> b) -> a -> b
$ (Predicate a b -> Either b (Predicate a b))
-> [Predicate a b] -> [Either b (Predicate a b)]
forall a b. (a -> b) -> [a] -> [b]
map (Predicate a b -> a -> Either b (Predicate a b)
forall a b. Predicate a b -> a -> Either b (Predicate a b)
`predApply` a
a) [Predicate a b]
ps

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

data Event model cmd resp (r :: Type -> Type) = Event
  { Event model cmd resp r -> model r
eventBefore :: model r
  , Event model cmd resp r -> cmd r
eventCmd    :: cmd   r
  , Event model cmd resp r -> model r
eventAfter  :: model r
  , Event model cmd resp r -> resp r
eventResp   :: resp  r
  }
  deriving stock Int -> Event model cmd resp r -> ShowS
[Event model cmd resp r] -> ShowS
Event model cmd resp r -> String
(Int -> Event model cmd resp r -> ShowS)
-> (Event model cmd resp r -> String)
-> ([Event model cmd resp r] -> ShowS)
-> Show (Event model cmd resp r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
(Show (model r), Show (cmd r), Show (resp r)) =>
Int -> Event model cmd resp r -> ShowS
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
(Show (model r), Show (cmd r), Show (resp r)) =>
[Event model cmd resp r] -> ShowS
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
(Show (model r), Show (cmd r), Show (resp r)) =>
Event model cmd resp r -> String
showList :: [Event model cmd resp r] -> ShowS
$cshowList :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
(Show (model r), Show (cmd r), Show (resp r)) =>
[Event model cmd resp r] -> ShowS
show :: Event model cmd resp r -> String
$cshow :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
(Show (model r), Show (cmd r), Show (resp r)) =>
Event model cmd resp r -> String
showsPrec :: Int -> Event model cmd resp r -> ShowS
$cshowsPrec :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
(Show (model r), Show (cmd r), Show (resp r)) =>
Int -> Event model cmd resp r -> ShowS
Show

-- | Step the model using a 'Command' (i.e., a command associated with an
-- explicit set of variables).
execCmd :: StateMachine model cmd m resp
        -> model Symbolic -> Command cmd resp -> Event model cmd resp Symbolic
execCmd :: StateMachine model cmd m resp
-> model Symbolic
-> Command cmd resp
-> Event model cmd resp Symbolic
execCmd StateMachine { forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition } model Symbolic
model (Command cmd Symbolic
cmd resp Symbolic
resp [Var]
_vars) =
  Event :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
model r -> cmd r -> model r -> resp r -> Event model cmd resp r
Event
    { eventBefore :: model Symbolic
eventBefore = model Symbolic
model
    , eventCmd :: cmd Symbolic
eventCmd    = cmd Symbolic
cmd
    , eventAfter :: model Symbolic
eventAfter  = model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
cmd resp Symbolic
resp
    , eventResp :: resp Symbolic
eventResp   = resp Symbolic
resp
    }

-- | 'execCmds' is just the repeated form of 'execCmd'.
execCmds :: forall model cmd m resp. StateMachine model cmd m resp
         -> Commands cmd resp -> [Event model cmd resp Symbolic]
execCmds :: StateMachine model cmd m resp
-> Commands cmd resp -> [Event model cmd resp Symbolic]
execCmds sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } = model Symbolic
-> [Command cmd resp] -> [Event model cmd resp Symbolic]
go model Symbolic
forall (r :: * -> *). model r
initModel ([Command cmd resp] -> [Event model cmd resp Symbolic])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Event model cmd resp Symbolic]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
  where
    go :: model Symbolic -> [Command cmd resp] -> [Event model cmd resp Symbolic]
    go :: model Symbolic
-> [Command cmd resp] -> [Event model cmd resp Symbolic]
go model Symbolic
_ []       = []
    go model Symbolic
m (Command cmd resp
c : [Command cmd resp]
cs) = let ev :: Event model cmd resp Symbolic
ev = StateMachine model cmd m resp
-> model Symbolic
-> Command cmd resp
-> Event model cmd resp Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic
-> Command cmd resp
-> Event model cmd resp Symbolic
execCmd StateMachine model cmd m resp
sm model Symbolic
m Command cmd resp
c in Event model cmd resp Symbolic
ev Event model cmd resp Symbolic
-> [Event model cmd resp Symbolic]
-> [Event model cmd resp Symbolic]
forall a. a -> [a] -> [a]
: model Symbolic
-> [Command cmd resp] -> [Event model cmd resp Symbolic]
go (Event model cmd resp Symbolic -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> model r
eventAfter Event model cmd resp Symbolic
ev) [Command cmd resp]
cs

execOp :: StateMachine model cmd m resp -> model Concrete -> Operation cmd resp
       -> Maybe (Event model cmd resp Concrete)
execOp :: StateMachine model cmd m resp
-> model Concrete
-> Operation cmd resp
-> Maybe (Event model cmd resp Concrete)
execOp StateMachine model cmd m resp
_sm                        model Concrete
_model (Crash cmd Concrete
_cmd String
_err Pid
_pid)    = Maybe (Event model cmd resp Concrete)
forall a. Maybe a
Nothing
execOp StateMachine { forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition } model Concrete
model (Operation cmd Concrete
cmd resp Concrete
resp Pid
_pid) = Event model cmd resp Concrete
-> Maybe (Event model cmd resp Concrete)
forall a. a -> Maybe a
Just (Event model cmd resp Concrete
 -> Maybe (Event model cmd resp Concrete))
-> Event model cmd resp Concrete
-> Maybe (Event model cmd resp Concrete)
forall a b. (a -> b) -> a -> b
$
  Event :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
model r -> cmd r -> model r -> resp r -> Event model cmd resp r
Event
    { eventBefore :: model Concrete
eventBefore = model Concrete
model
    , eventCmd :: cmd Concrete
eventCmd    = cmd Concrete
cmd
    , eventAfter :: model Concrete
eventAfter  = model Concrete -> cmd Concrete -> resp Concrete -> model Concrete
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
model cmd Concrete
cmd resp Concrete
resp
    , eventResp :: resp Concrete
eventResp   = resp Concrete
resp
    }

execHistory :: forall model cmd m resp. StateMachine model cmd m resp
            -> History cmd resp -> [Event model cmd resp Concrete]
execHistory :: StateMachine model cmd m resp
-> History cmd resp -> [Event model cmd resp Concrete]
execHistory sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } = model Concrete
-> [Operation cmd resp] -> [Event model cmd resp Concrete]
go model Concrete
forall (r :: * -> *). model r
initModel ([Operation cmd resp] -> [Event model cmd resp Concrete])
-> (History cmd resp -> [Operation cmd resp])
-> History cmd resp
-> [Event model cmd resp Concrete]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History' cmd resp -> [Operation cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> [Operation cmd resp]
makeOperations (History' cmd resp -> [Operation cmd resp])
-> (History cmd resp -> History' cmd resp)
-> History cmd resp
-> [Operation cmd resp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History cmd resp -> History' cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
  where
    go :: model Concrete -> [Operation cmd resp] -> [Event model cmd resp Concrete]
    go :: model Concrete
-> [Operation cmd resp] -> [Event model cmd resp Concrete]
go model Concrete
_ []       = []
    go model Concrete
m (Operation cmd resp
o : [Operation cmd resp]
os) = let mev :: Maybe (Event model cmd resp Concrete)
mev = StateMachine model cmd m resp
-> model Concrete
-> Operation cmd resp
-> Maybe (Event model cmd resp Concrete)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Concrete
-> Operation cmd resp
-> Maybe (Event model cmd resp Concrete)
execOp StateMachine model cmd m resp
sm model Concrete
m Operation cmd resp
o in
      case (Maybe (Event model cmd resp Concrete)
mev, [Operation cmd resp]
os) of
        (Maybe (Event model cmd resp Concrete)
Nothing, []) -> []
        (Maybe (Event model cmd resp Concrete)
Nothing, [Operation cmd resp]
_)  -> String -> [Event model cmd resp Concrete]
forall a. HasCallStack => String -> a
error String
"execHistory: impossible, there are no more ops after a crash."
        (Just Event model cmd resp Concrete
ev, [Operation cmd resp]
_)  -> Event model cmd resp Concrete
ev Event model cmd resp Concrete
-> [Event model cmd resp Concrete]
-> [Event model cmd resp Concrete]
forall a. a -> [a] -> [a]
: model Concrete
-> [Operation cmd resp] -> [Event model cmd resp Concrete]
go (Event model cmd resp Concrete -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *) (r :: * -> *).
Event model cmd resp r -> model r
eventAfter Event model cmd resp Concrete
ev) [Operation cmd resp]
os