{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Traces of transition systems and associated operators.
--
-- This module also includes a minimal domain-specific-language to specify
-- expectations on traces.
module Test.Control.State.Transition.Trace (
  SigState (..),

  -- * Trace checking
  (.-),
  (.->),
  (.->>),
  checkTrace,

  -- * Trace
  Trace (..),
  TraceOrder (NewestFirst, OldestFirst),
  mkTrace,
  traceEnv,
  traceInitState,
  traceSignals,
  traceStates,
  preStatesAndSignals,
  SourceSignalTarget (..),
  sourceSignalTargets,
  traceLength,
  traceInit,
  lastState,
  lastSignal,
  firstAndLastState,
  closure,

  -- * Miscellaneous utilities
  extractValues,
  applySTSTest,
  getEvents,
  splitTrace,
)
where

import Control.DeepSeq (NFData)
import Control.Monad (void)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)
import Control.State.Transition.Extended hiding (Assertion, trans)
import Data.Data (Data, Typeable, cast, gmapQ)
import Data.Foldable (toList)
import Data.List.NonEmpty (NonEmpty)
import Data.Maybe (catMaybes)
import Data.Sequence.Strict (StrictSeq (Empty, (:<|), (:|>)))
import qualified Data.Sequence.Strict as SS
import qualified Data.Sequence.Strict as StrictSeq
import GHC.Generics (Generic)
import GHC.Stack (HasCallStack)
import Lens.Micro (Lens', lens, to, (^.), (^..))
import Lens.Micro.TH (makeLenses)
import NoThunks.Class (NoThunks (..))
import Test.Cardano.Ledger.Binary.TreeDiff (ToExpr, assertExprEqualWithMessage)
import Test.Tasty.HUnit (assertFailure, (@?=))

-- Signal and resulting state.
--
-- Strict in both arguments, unlike a tuple.
data SigState s = SigState !(State s) !(Signal s)
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s x. Rep (SigState s) x -> SigState s
forall s x. SigState s -> Rep (SigState s) x
$cto :: forall s x. Rep (SigState s) x -> SigState s
$cfrom :: forall s x. SigState s -> Rep (SigState s) x
Generic)

transSt :: Lens' (SigState s) (State s)
transSt :: forall s. Lens' (SigState s) (State s)
transSt = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (\(SigState State s
st Signal s
_) -> State s
st) (\(SigState State s
_ Signal s
x) State s
st -> forall s. State s -> Signal s -> SigState s
SigState State s
st Signal s
x)

transSig :: Lens' (SigState s) (Signal s)
transSig :: forall s. Lens' (SigState s) (Signal s)
transSig = forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (\(SigState State s
_ Signal s
sig) -> Signal s
sig) (\(SigState State s
x Signal s
_) Signal s
sig -> forall s. State s -> Signal s -> SigState s
SigState State s
x Signal s
sig)

deriving instance
  (Eq (State s), Eq (Signal s)) => (Eq (SigState s))

deriving instance
  (Show (State s), Show (Signal s)) => (Show (SigState s))

instance
  ( NoThunks (State s)
  , NoThunks (Signal s)
  ) =>
  (NoThunks (SigState s))

-- | A successful trace of a transition system.
data Trace s = Trace
  { forall s. Trace s -> Environment s
_traceEnv :: !(Environment s)
  -- ^ Environment under which the trace was run.
  , forall s. Trace s -> State s
_traceInitState :: !(State s)
  -- ^ Initial state in the trace
  , forall s. Trace s -> StrictSeq (SigState s)
_traceTrans :: !(StrictSeq (SigState s))
  -- ^ Signals and resulting states observed in the trace. New elements are
  -- put in front of the list.
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s x. Rep (Trace s) x -> Trace s
forall s x. Trace s -> Rep (Trace s) x
$cto :: forall s x. Rep (Trace s) x -> Trace s
$cfrom :: forall s x. Trace s -> Rep (Trace s) x
Generic)

makeLenses ''Trace

deriving instance
  ( NFData (Environment s)
  , NFData (State s)
  , NFData (SigState s)
  ) =>
  (NFData (Trace s))

deriving instance
  (Eq (State s), Eq (Signal s), Eq (Environment s)) => (Eq (Trace s))

deriving instance
  (Show (State s), Show (Signal s), Show (Environment s)) => (Show (Trace s))

instance
  ( NoThunks (Environment s)
  , NoThunks (State s)
  , NoThunks (Signal s)
  ) =>
  (NoThunks (Trace s))

-- | Make a trace given an environment and initial state.
mkTrace :: Environment s -> State s -> [(State s, Signal s)] -> Trace s
mkTrace :: forall s.
Environment s -> State s -> [(State s, Signal s)] -> Trace s
mkTrace Environment s
env State s
initState [(State s, Signal s)]
sigs = forall s.
Environment s -> State s -> StrictSeq (SigState s) -> Trace s
Trace Environment s
env State s
initState StrictSeq (SigState s)
sigs'
  where
    sigs' :: StrictSeq (SigState s)
sigs' = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall s. State s -> Signal s -> SigState s
SigState forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> StrictSeq a
StrictSeq.fromList [(State s, Signal s)]
sigs

-- $setup
-- |
-- >>> :set -XTypeFamilies
-- >>> import Control.State.Transition (initialRules, transitionRules)
-- >>> import Control.State.Transition.Extended (STS (..))
-- >>> :{
-- data DUMMY
-- data DummyPredicateFailure = CeciNEstPasUnePredicateFailure deriving (Eq, Show)
-- instance STS DUMMY where
--   type Environment DUMMY = Bool
--   type State DUMMY = Int
--   type Signal DUMMY = String
--   type PredicateFailure DUMMY = DummyPredicateFailure
--   initialRules = []
--   transitionRules = []
-- :}

-- | Extract the last state of a trace. Since a trace has at least an initial
-- state, the last state of a trace is always defined.
--
-- Examples:
--
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> lastState tr0
-- 0
--
-- >>> tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
-- >>> lastState tr01
-- 1
--
-- >>> tr012 = mkTrace True 0 [(2, "two"), (1, "one")] :: Trace DUMMY
-- >>> lastState tr012
-- 2
lastState :: Trace s -> State s
lastState :: forall s. Trace s -> State s
lastState Trace {State s
_traceInitState :: State s
_traceInitState :: forall s. Trace s -> State s
_traceInitState, StrictSeq (SigState s)
_traceTrans :: StrictSeq (SigState s)
_traceTrans :: forall s. Trace s -> StrictSeq (SigState s)
_traceTrans} =
  case StrictSeq (SigState s)
_traceTrans of
    SigState State s
st Signal s
_ :<| StrictSeq (SigState s)
_ -> State s
st
    StrictSeq (SigState s)
_ -> State s
_traceInitState

-- | Get the last applied signal in a trace (this is, the newest signal).
--
--
-- Examples:
--
-- >>> :set -XScopedTypeVariables
-- >>> import Control.Exception (catch, ErrorCall)
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> print (lastSignal tr0) `catch` (\(_ :: ErrorCall) -> putStrLn "error!")
-- "error!
--
-- dnadales: In the example above I don't know why the doctests is swallowing
-- the last @"@.
--
-- >>> tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
-- >>> lastSignal tr01
-- "one"
--
-- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
-- >>> lastSignal tr0123
-- "three"
lastSignal :: HasCallStack => Trace s -> Signal s
lastSignal :: forall s. HasCallStack => Trace s -> Signal s
lastSignal Trace {StrictSeq (SigState s)
_traceTrans :: StrictSeq (SigState s)
_traceTrans :: forall s. Trace s -> StrictSeq (SigState s)
_traceTrans} =
  case StrictSeq (SigState s)
_traceTrans of
    StrictSeq (SigState s)
Empty -> forall a. HasCallStack => String -> a
error String
"lastSignal was called with a trace without signals"
    SigState State s
_st Signal s
signal :<| StrictSeq (SigState s)
_ -> Signal s
signal

-- | Return the first and last state of the trace.
--
-- The first state is returned in the first component of the result tuple.
--
-- Examples:
--
--
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> firstAndLastState tr0
-- (0,0)
--
-- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
-- >>> firstAndLastState tr0123
-- (0,3)
firstAndLastState :: Trace s -> (State s, State s)
firstAndLastState :: forall s. Trace s -> (State s, State s)
firstAndLastState Trace s
tr = (forall s. Trace s -> State s
_traceInitState Trace s
tr, forall s. Trace s -> State s
lastState Trace s
tr)

data TraceOrder = NewestFirst | OldestFirst deriving (TraceOrder -> TraceOrder -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TraceOrder -> TraceOrder -> Bool
$c/= :: TraceOrder -> TraceOrder -> Bool
== :: TraceOrder -> TraceOrder -> Bool
$c== :: TraceOrder -> TraceOrder -> Bool
Eq)

fromNewestFirst :: TraceOrder -> [a] -> [a]
fromNewestFirst :: forall a. TraceOrder -> [a] -> [a]
fromNewestFirst TraceOrder
NewestFirst = forall a. a -> a
id
fromNewestFirst TraceOrder
OldestFirst = forall a. [a] -> [a]
reverse

-- | Retrieve all the signals in the trace, in the order specified.
--
-- Examples:
--
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> traceSignals NewestFirst tr0
-- []
--
-- >>> tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
-- >>> traceSignals NewestFirst tr01
-- ["one"]
--
-- >>> traceSignals OldestFirst tr01
-- ["one"]
--
-- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
-- >>> traceSignals NewestFirst tr0123
-- ["three","two","one"]
--
-- >>> traceSignals OldestFirst tr0123
-- ["one","two","three"]
traceSignals :: TraceOrder -> Trace s -> [Signal s]
traceSignals :: forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
order Trace s
tr = forall a. TraceOrder -> [a] -> [a]
fromNewestFirst TraceOrder
order (Trace s
tr forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall s. Lens' (Trace s) (StrictSeq (SigState s))
traceTrans forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Lens' (SigState s) (Signal s)
transSig)

-- | Retrieve all the states in the trace, in the order specified.
--
-- Examples:
--
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> traceStates NewestFirst tr0
-- [0]
--
-- >>> traceStates OldestFirst tr0
-- [0]
--
-- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
-- >>> traceStates NewestFirst tr0123
-- [3,2,1,0]
--
-- >>> traceStates OldestFirst tr0123
-- [0,1,2,3]
traceStates :: TraceOrder -> Trace s -> [State s]
traceStates :: forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
order Trace s
tr = forall a. TraceOrder -> [a] -> [a]
fromNewestFirst TraceOrder
order ([State s]
xs forall a. [a] -> [a] -> [a]
++ [State s
x])
  where
    x :: State s
x = Trace s
tr forall s a. s -> Getting a s a -> a
^. forall s. Lens' (Trace s) (State s)
traceInitState
    xs :: [State s]
xs = Trace s
tr forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. forall s. Lens' (Trace s) (StrictSeq (SigState s))
traceTrans forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Lens' (SigState s) (State s)
transSt

-- | Compute the length of a trace, defined as the number of signals it
-- contains.
--
-- Examples:
--
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> traceLength tr0
-- 0
--
-- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
-- >>> traceLength tr0123
-- 3
traceLength :: Trace s -> Int
traceLength :: forall s. Trace s -> Int
traceLength Trace s
tr = Trace s
tr forall s a. s -> Getting a s a -> a
^. forall s. Lens' (Trace s) (StrictSeq (SigState s))
traceTrans forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. (s -> a) -> SimpleGetter s a
to forall (t :: * -> *) a. Foldable t => t a -> Int
length

-- | Take all but the newest signal in the trace.
--
-- Precondition: the trace must contain at least one signal
--
-- Examples:
--
--
-- >>> :set -XScopedTypeVariables
-- >>> import Control.Exception (catch, ErrorCall)
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> print (traceInit tr0) `catch` (\(_ :: ErrorCall) -> print "error!")
-- "error!"
--
-- >>> tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
-- >>> traceInit tr01
-- Trace {_traceEnv = True, _traceInitState = 0, _traceTrans = StrictSeq {fromStrict = fromList []}}
--
-- >>> tr012 = mkTrace True 0 [(2, "two"), (1, "one")] :: Trace DUMMY
-- >>> traceInit tr012
-- Trace {_traceEnv = True, _traceInitState = 0, _traceTrans = StrictSeq {fromStrict = fromList [SigState 1 "one"]}}
traceInit :: HasCallStack => Trace s -> Trace s
traceInit :: forall s. HasCallStack => Trace s -> Trace s
traceInit tr :: Trace s
tr@Trace {StrictSeq (SigState s)
_traceTrans :: StrictSeq (SigState s)
_traceTrans :: forall s. Trace s -> StrictSeq (SigState s)
_traceTrans} =
  case StrictSeq (SigState s)
_traceTrans of
    StrictSeq (SigState s)
Empty -> forall a. HasCallStack => String -> a
error String
"traceInit was called with a trace without signals"
    SigState s
_ :<| StrictSeq (SigState s)
trans -> Trace s
tr {_traceTrans :: StrictSeq (SigState s)
_traceTrans = StrictSeq (SigState s)
trans}

-- | Retrieve all the signals in the trace paired with the state prior to the
-- application of the signal.
--
-- Note that the last state in the trace will not be returned, since there is
-- no corresponding signal, i.e. the last state is not the pre-state of any
-- signal in the trace.
--
-- Examples
--
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> preStatesAndSignals NewestFirst tr0
-- []
--
-- >>> preStatesAndSignals OldestFirst tr0
-- []
--
-- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
-- >>> preStatesAndSignals OldestFirst tr0123
-- [(0,"one"),(1,"two"),(2,"three")]
--
-- >>> preStatesAndSignals NewestFirst tr0123
-- [(2,"three"),(1,"two"),(0,"one")]
preStatesAndSignals :: TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals :: forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals TraceOrder
OldestFirst Trace s
tr =
  forall a b. [a] -> [b] -> [(a, b)]
zip (forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace s
tr) (forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace s
tr)
preStatesAndSignals TraceOrder
NewestFirst Trace s
tr =
  forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals TraceOrder
OldestFirst Trace s
tr

-- | Apply the signals in the list and elaborate a trace with the resulting
-- states.
--
-- If any of the signals cannot be applied, then it is discarded, and the next
-- signal is tried.
--
-- >>> :set -XTypeFamilies
-- >>> :set -XTypeApplications
-- >>> import Control.State.Transition (initialRules, transitionRules, judgmentContext)
-- >>> import Control.State.Transition.Extended (TRC (..))
-- >>> import Data.Functor.Identity
-- >>> :{
-- data ADDER
-- data AdderPredicateFailure = NoFailuresPossible deriving (Eq, Show)
-- instance STS ADDER where
--   type Environment ADDER = ()
--   type State ADDER = Int
--   type Signal ADDER = Int
--   type PredicateFailure ADDER = AdderPredicateFailure
--   initialRules = [ pure 0 ]
--   transitionRules =
--     [ do
--         TRC ((), st, inc) <- judgmentContext
--         pure $! st + inc
--     ]
-- :}
--
-- >>> runIdentity $ closure @ADDER () 0 [3, 2, 1]
-- Trace {_traceEnv = (), _traceInitState = 0, _traceTrans = StrictSeq {fromStrict = fromList [SigState 6 3,SigState 3 2,SigState 1 1]}}
--
-- >>> runIdentity $ closure @ADDER () 10 [-3, -2, -1]
-- Trace {_traceEnv = (), _traceInitState = 10, _traceTrans = StrictSeq {fromStrict = fromList [SigState 4 (-3),SigState 7 (-2),SigState 9 (-1)]}}
closure ::
  forall s m.
  (STS s, m ~ BaseM s) =>
  Environment s ->
  State s ->
  -- | List of signals to apply, where the newest signal comes first.
  [Signal s] ->
  m (Trace s)
closure :: forall s (m :: * -> *).
(STS s, m ~ BaseM s) =>
Environment s -> State s -> [Signal s] -> m (Trace s)
closure Environment s
env State s
st0 [Signal s]
sigs = forall s.
Environment s -> State s -> [(State s, Signal s)] -> Trace s
mkTrace Environment s
env State s
st0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State s
-> [Signal s] -> [(State s, Signal s)] -> m [(State s, Signal s)]
loop State s
st0 (forall a. [a] -> [a]
reverse [Signal s]
sigs) []
  where
    loop :: State s
-> [Signal s] -> [(State s, Signal s)] -> m [(State s, Signal s)]
loop State s
_ [] [(State s, Signal s)]
acc = forall (f :: * -> *) a. Applicative f => a -> f a
pure [(State s, Signal s)]
acc
    loop State s
sti (Signal s
sig : [Signal s]
sigs') [(State s, Signal s)]
acc =
      forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest @s (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment s
env, State s
sti, Signal s
sig)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Left NonEmpty (PredicateFailure s)
_ -> State s
-> [Signal s] -> [(State s, Signal s)] -> m [(State s, Signal s)]
loop State s
sti [Signal s]
sigs' [(State s, Signal s)]
acc
        Right State s
sti' -> State s
-> [Signal s] -> [(State s, Signal s)] -> m [(State s, Signal s)]
loop State s
sti' [Signal s]
sigs' ((State s
sti', Signal s
sig) forall a. a -> [a] -> [a]
: [(State s, Signal s)]
acc)

--------------------------------------------------------------------------------
-- Minimal DSL to specify expectations on traces
--------------------------------------------------------------------------------

-- | Bind the state inside the first argument, and apply the transition
-- function in the @Reader@ environment to that state and given signal,
-- obtaining the resulting state, or an assertion failure if the transition
-- function fails.
(.-) ::
  forall m st sig err.
  ( MonadIO m
  , MonadReader (st -> sig -> Either err st) m
  , Show err
  , HasCallStack
  ) =>
  m st ->
  sig ->
  m st
m st
mSt .- :: forall (m :: * -> *) st sig err.
(MonadIO m, MonadReader (st -> sig -> Either err st) m, Show err,
 HasCallStack) =>
m st -> sig -> m st
.- sig
sig = do
  st
st <- m st
mSt
  st -> sig -> Either err st
validation <- forall r (m :: * -> *). MonadReader r m => m r
ask -- Get the validation function from the environment
  case st -> sig -> Either err st
validation st
st sig
sig of
    Left err
pfs -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => String -> IO a
assertFailure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ err
pfs
    Right st
st' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure st
st'

-- | Bind the state inside the first argument, and check whether it is equal to
-- the expected state, given in the second argument. If it isn't raise an Assertion that
-- uses a tree-diff to describe the differences.
(.->>) ::
  forall m st.
  (MonadIO m, Eq st, ToExpr st, HasCallStack) =>
  m st ->
  st ->
  m st
m st
mSt .->> :: forall (m :: * -> *) st.
(MonadIO m, Eq st, ToExpr st, HasCallStack) =>
m st -> st -> m st
.->> st
stExpected = do
  st
stActual <- m st
mSt
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a.
(ToExpr a, Eq a, HasCallStack) =>
String -> a -> a -> Assertion
assertExprEqualWithMessage String
"Check trace with (.->>) fails" st
stExpected st
stActual
  forall (m :: * -> *) a. Monad m => a -> m a
return st
stActual

-- | Bind the state inside the first argument, and check whether it is equal to
-- the expected state, given in the second argument. raises an Assertion if it does not.
(.->) ::
  forall m st.
  (MonadIO m, Eq st, Show st, HasCallStack) =>
  m st ->
  st ->
  m st
m st
mSt .-> :: forall (m :: * -> *) st.
(MonadIO m, Eq st, Show st, HasCallStack) =>
m st -> st -> m st
.-> st
stExpected = do
  st
stActual <- m st
mSt
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ st
stActual forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= st
stExpected
  forall (m :: * -> *) a. Monad m => a -> m a
return st
stActual

checkTrace ::
  forall s m.
  (STS s, BaseM s ~ m) =>
  (forall a. m a -> a) ->
  Environment s ->
  ReaderT
    ( State s ->
      Signal s ->
      Either (NonEmpty (PredicateFailure s)) (State s)
    )
    IO
    (State s) ->
  IO ()
checkTrace :: forall s (m :: * -> *).
(STS s, BaseM s ~ m) =>
(forall a. m a -> a)
-> Environment s
-> ReaderT
     (State s
      -> Signal s -> Either (NonEmpty (PredicateFailure s)) (State s))
     IO
     (State s)
-> Assertion
checkTrace forall a. m a -> a
interp Environment s
env ReaderT
  (State s
   -> Signal s -> Either (NonEmpty (PredicateFailure s)) (State s))
  IO
  (State s)
act =
  forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT
  (State s
   -> Signal s -> Either (NonEmpty (PredicateFailure s)) (State s))
  IO
  (State s)
act (\State s
st Signal s
sig -> forall a. m a -> a
interp forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest @s (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment s
env, State s
st, Signal s
sig)))

-- | Extract all the values of a given type.
--
-- Examples:
--
-- >>> extractValues "hello" :: [Char]
-- "hello"
--
-- >>> extractValues ("hello", " " ,"world") :: [Char]
-- "hello world"
--
-- >>> extractValues "hello" :: [Int]
-- []
--
-- >>> extractValues ([('a', 0 :: Int), ('b', 1)] :: [(Char, Int)]) :: [Int]
-- [0,1]
--
-- >>> extractValues (["hello"] :: [[Char]], 1, 'z') :: [[Char]]
-- ["hello","ello","llo","lo","o",""]
--
-- >>> extractValues ("hello", 'z') :: [Char]
-- "zhello"
extractValues :: forall d a. (Data d, Typeable a) => d -> [a]
extractValues :: forall d a. (Data d, Typeable a) => d -> [a]
extractValues d
d =
  forall a. [Maybe a] -> [a]
catMaybes (forall a u. Data a => (forall d. Data d => d -> u) -> a -> [u]
gmapQ forall d1. Data d1 => d1 -> Maybe a
extractValue d
d)
    forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a u. Data a => (forall d. Data d => d -> u) -> a -> [u]
gmapQ forall d a. (Data d, Typeable a) => d -> [a]
extractValues d
d)
  where
    extractValue :: forall d1. Data d1 => d1 -> Maybe a
    extractValue :: forall d1. Data d1 => d1 -> Maybe a
extractValue d1
d1 = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast d1
d1

data SourceSignalTarget a = SourceSignalTarget
  { forall a. SourceSignalTarget a -> State a
source :: State a
  , forall a. SourceSignalTarget a -> State a
target :: State a
  , forall a. SourceSignalTarget a -> Signal a
signal :: Signal a
  }

deriving instance (Eq (State a), Eq (Signal a)) => Eq (SourceSignalTarget a)

deriving instance (Show (State a), Show (Signal a)) => Show (SourceSignalTarget a)

-- | Extract triplets of the form [SourceSignalTarget {source = s, signal = sig, target =
-- t)] from a trace. For a valid trace, each source state can reach a target
-- state via the given signal.
--
-- Examples
--
--
-- >>> tr0 = mkTrace True 0 [] :: Trace DUMMY
-- >>> sourceSignalTargets tr0
-- []
--
-- >>> tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
-- >>> sourceSignalTargets tr0123
-- [SourceSignalTarget {source = 0, target = 1, signal = "one"},SourceSignalTarget {source = 1, target = 2, signal = "two"},SourceSignalTarget {source = 2, target = 3, signal = "three"}]
sourceSignalTargets :: forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets :: forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace a
trace = forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 forall a. State a -> State a -> Signal a -> SourceSignalTarget a
SourceSignalTarget [State a]
states [State a]
statesTail [Signal a]
signals
  where
    signals :: [Signal a]
signals = forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace a
trace
    states :: [State a]
states = forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace a
trace
    statesTail :: [State a]
statesTail =
      case [State a]
states of
        [] -> forall a. HasCallStack => String -> a
error String
"Control.State.Transition.Trace.sourceSignalTargets: Unexpected empty list"
        (State a
_ : [State a]
xs) -> [State a]
xs

-- | Apply STS checking assertions.
applySTSTest ::
  forall s m rtype.
  (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
  RuleContext rtype s ->
  m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest :: forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest = forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either
        (NonEmpty (PredicateFailure s)) (EventReturnType ep s (State s)))
applySTSOptsEither ApplySTSOpts 'EventPolicyDiscard
defaultOpts
  where
    defaultOpts :: ApplySTSOpts 'EventPolicyDiscard
defaultOpts =
      ApplySTSOpts
        { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsAll
        , asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateAll
        , asoEvents :: SingEP 'EventPolicyDiscard
asoEvents = SingEP 'EventPolicyDiscard
EPDiscard
        }

-- | Extract the Events from a trace, by re-applying the signal with
--   assertions and vaidations turned off, but events turned on.
getEvents :: forall sts. STS sts => Trace sts -> BaseM sts [[Event sts]]
getEvents :: forall sts. STS sts => Trace sts -> BaseM sts [[Event sts]]
getEvents (Trace Environment sts
env State sts
s0 StrictSeq (SigState sts)
pairs) = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Environment sts, State sts, Signal sts) -> BaseM sts [Event sts]
action (forall a b. (a -> b) -> [a] -> [b]
map (State sts, Signal sts) -> (Environment sts, State sts, Signal sts)
make [(State sts, Signal sts)]
pairs2)
  where
    pairs2 :: [(State sts, Signal sts)]
pairs2 = forall s. State s -> [SigState s] -> [(State s, Signal s)]
unstagger State sts
s0 (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (SigState sts)
pairs)
    make :: (State sts, Signal sts) -> (Environment sts, State sts, Signal sts)
make (State sts
state, Signal sts
sig) = (Environment sts
env, State sts
state, Signal sts
sig)
    defaultOpts :: ApplySTSOpts 'EventPolicyReturn
defaultOpts =
      ApplySTSOpts
        { asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsOff
        , asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateNone
        , asoEvents :: SingEP 'EventPolicyReturn
asoEvents = SingEP 'EventPolicyReturn
EPReturn
        }
    action :: (Environment sts, State sts, Signal sts) -> BaseM sts [Event sts]
    action :: (Environment sts, State sts, Signal sts) -> BaseM sts [Event sts]
action (Environment sts, State sts, Signal sts)
x = do
      Either (NonEmpty (PredicateFailure sts)) (State sts, [Event sts])
item <- forall s (m :: * -> *) (rtype :: RuleType) (ep :: EventPolicy).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ep
-> RuleContext rtype s
-> m (Either
        (NonEmpty (PredicateFailure s)) (EventReturnType ep s (State s)))
applySTSOptsEither @sts @(BaseM sts) @'Transition ApplySTSOpts 'EventPolicyReturn
defaultOpts (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (Environment sts, State sts, Signal sts)
x)
      case Either (NonEmpty (PredicateFailure sts)) (State sts, [Event sts])
item of
        Left NonEmpty (PredicateFailure sts)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        Right (State sts
_, [Event sts]
events) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [a] -> [a]
reverse [Event sts]
events)
    -- A Trace stores pairs of State and Signal (called a SigState). The pairs
    -- consist of the state that came about by appying the signal, so the index
    -- of the two parts don't match up. For example here is a sample
    -- [(s_n+1,dn), ... ,(s5,d4),(s4,d3),(s3,d2),(s2,d1)] si is a state and dj is a signal.
    -- Note how the indexes don't matchup. When we compute events we want the indices to align.
    -- We want it to look like this [(sn,dn), ... ,(s5,d5),(s4,d4),(s3,d3),(s2,d2),(s1,d1)]
    -- We call this transformation, the unstagger transformation.
    unstagger :: State s -> [SigState s] -> [(State s, Signal s)]
    unstagger :: forall s. State s -> [SigState s] -> [(State s, Signal s)]
unstagger State s
_ [] = []
    unstagger State s
s1 [(SigState State s
_s2 Signal s
d1)] = [(State s
s1, Signal s
d1)]
    unstagger State s
s1 ((SigState State s
_s4 Signal s
d3) : (more :: [SigState s]
more@((SigState State s
s3 Signal s
_d2) : [SigState s]
_))) = (State s
s3, Signal s
d3) forall a. a -> [a] -> [a]
: forall s. State s -> [SigState s] -> [(State s, Signal s)]
unstagger State s
s1 [SigState s]
more

-- | Given a StrictSeq of SigState (as found in a Trace, where earlier things are to the right), and
--   Given 'p' that compares later states to earlier states, split at the boundary where
--   the 'p' detects a change. Used to make a list of shorter Traces from a big Trace. Usually
--   'p' dectects changes in the Epoch (this marks the epoch boundary), but might have other uses.
--   Note that the last sub-Trace might be ill-formed, because we run out of Trace elements,
--   rather than detecting the changes guarded by 'p'
splitAtChange ::
  (State s -> State s -> Bool) ->
  StrictSeq (SigState s) ->
  State s ->
  StrictSeq (SigState s) ->
  [(StrictSeq (SigState s), State s)] ->
  [(StrictSeq (SigState s), State s)]
splitAtChange :: forall s.
(State s -> State s -> Bool)
-> StrictSeq (SigState s)
-> State s
-> StrictSeq (SigState s)
-> [(StrictSeq (SigState s), State s)]
-> [(StrictSeq (SigState s), State s)]
splitAtChange State s -> State s -> Bool
_p StrictSeq (SigState s)
SS.Empty State s
a0 StrictSeq (SigState s)
ans1 [(StrictSeq (SigState s), State s)]
ans2 = (StrictSeq (SigState s)
ans1, State s
a0) forall a. a -> [a] -> [a]
: [(StrictSeq (SigState s), State s)]
ans2 -- Might be ill-formed
splitAtChange State s -> State s -> Bool
p (xs :: StrictSeq (SigState s)
xs@(StrictSeq (SigState s)
_ :|> SigState s
x1) :|> SigState s
x0) State s
a0 StrictSeq (SigState s)
ans1 [(StrictSeq (SigState s), State s)]
ans2 =
  if State s -> State s -> Bool
p State s
s1 State s
s0
    then forall s.
(State s -> State s -> Bool)
-> StrictSeq (SigState s)
-> State s
-> StrictSeq (SigState s)
-> [(StrictSeq (SigState s), State s)]
-> [(StrictSeq (SigState s), State s)]
splitAtChange State s -> State s -> Bool
p StrictSeq (SigState s)
xs State s
a0 (SigState s
x0 forall a. a -> StrictSeq a -> StrictSeq a
:<| StrictSeq (SigState s)
ans1) [(StrictSeq (SigState s), State s)]
ans2
    else forall s.
(State s -> State s -> Bool)
-> StrictSeq (SigState s)
-> State s
-> StrictSeq (SigState s)
-> [(StrictSeq (SigState s), State s)]
-> [(StrictSeq (SigState s), State s)]
splitAtChange State s -> State s -> Bool
p StrictSeq (SigState s)
xs State s
s0 forall a. StrictSeq a
SS.Empty ((SigState s
x1 forall a. a -> StrictSeq a -> StrictSeq a
:<| (SigState s
x0 forall a. a -> StrictSeq a -> StrictSeq a
:<| StrictSeq (SigState s)
ans1), State s
a0) forall a. a -> [a] -> [a]
: [(StrictSeq (SigState s), State s)]
ans2)
  where
    (SigState State s
s1 Signal s
_) = SigState s
x1
    (SigState State s
s0 Signal s
_) = SigState s
x0
splitAtChange State s -> State s -> Bool
_p (StrictSeq (SigState s)
SS.Empty :|> SigState s
x1) State s
a0 StrictSeq (SigState s)
ans1 [(StrictSeq (SigState s), State s)]
ans2 = (((SigState s
x1 forall a. a -> StrictSeq a -> StrictSeq a
:<| StrictSeq (SigState s)
ans1), State s
a0) forall a. a -> [a] -> [a]
: [(StrictSeq (SigState s), State s)]
ans2) -- Might be ill-formed

-- | Split a Trace into several shorter traces. The leftmost Trace
--   (at the front of the list) might be ill-formed, depending on what 'p' does.
splitTrace :: (State s -> State s -> Bool) -> Trace s -> [Trace s]
splitTrace :: forall s. (State s -> State s -> Bool) -> Trace s -> [Trace s]
splitTrace State s -> State s -> Bool
p (Trace Environment s
env State s
s0 StrictSeq (SigState s)
sigstates) = forall a b. (a -> b) -> [a] -> [b]
map (StrictSeq (SigState s), State s) -> Trace s
f [(StrictSeq (SigState s), State s)]
xs
  where
    f :: (StrictSeq (SigState s), State s) -> Trace s
f (StrictSeq (SigState s)
sigstates2, State s
s) = forall s.
Environment s -> State s -> StrictSeq (SigState s) -> Trace s
Trace Environment s
env State s
s StrictSeq (SigState s)
sigstates2
    xs :: [(StrictSeq (SigState s), State s)]
xs = forall s.
(State s -> State s -> Bool)
-> StrictSeq (SigState s)
-> State s
-> StrictSeq (SigState s)
-> [(StrictSeq (SigState s), State s)]
-> [(StrictSeq (SigState s), State s)]
splitAtChange State s -> State s -> Bool
p StrictSeq (SigState s)
sigstates State s
s0 forall a. StrictSeq a
Empty []