{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Invalid transition system traces.
--
-- An invalid trace consists of an valid prefix, and a last signal that
-- __might__ be invalid. The validity of the signal depends on the probability
-- of the trace generators of generating invalid signals.
--
module Control.State.Transition.Invalid.Trace where

import           NoThunks.Class (NoThunks(..))
import           Control.State.Transition (Environment, PredicateFailure, Signal, State)
import qualified Control.State.Transition.Trace as Trace
import           GHC.Generics (Generic)


data Trace s
  = Trace
    { Trace s -> Trace s
validPrefix :: !(Trace.Trace s)
    , Trace s -> Signal s
signal :: !(Signal s)
    -- ^ Last signal in the trace. This might cause a predicate failure, but it
    -- isn't guaranteed to do so, since invalid trace generation is
    -- probabilistic.
    , Trace s -> Either [[PredicateFailure s]] (State s)
errorOrLastState :: !(Either [[PredicateFailure s]] (State s))
    } deriving (forall x. Trace s -> Rep (Trace s) x)
-> (forall x. Rep (Trace s) x -> Trace s) -> Generic (Trace s)
forall x. Rep (Trace s) x -> Trace s
forall x. Trace s -> Rep (Trace s) x
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

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

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

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