{-# LANGUAGE AllowAmbiguousTypes #-}
{-# 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 UndecidableInstances #-}
module Control.State.Transition.Trace
(
(.-)
, (.->)
, checkTrace
, Trace (..)
, TraceOrder (NewestFirst, OldestFirst)
, mkTrace
, traceEnv
, traceInitState
, traceSignals
, traceStates
, preStatesAndSignals
, SourceSignalTarget (..)
, sourceSignalTargets
, traceLength
, traceInit
, lastState
, lastSignal
, firstAndLastState
, closure
, extractValues
, applySTSTest
)
where
import Control.Monad (void)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.Reader (MonadReader, ReaderT, ask, runReaderT)
import Data.Data (Data, Typeable, cast, gmapQ)
import Data.Functor ((<&>))
import Data.Maybe (catMaybes)
import Data.Sequence.Strict (StrictSeq ((:<|), Empty))
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.Tasty.HUnit (assertFailure, (@?=))
import Control.State.Transition.Extended hiding (Assertion, trans)
data SigState s = SigState !(State s) !(Signal s)
deriving ((forall x. SigState s -> Rep (SigState s) x)
-> (forall x. Rep (SigState s) x -> SigState s)
-> Generic (SigState s)
forall x. Rep (SigState s) x -> SigState s
forall x. SigState s -> Rep (SigState s) x
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 :: (State s -> f (State s)) -> SigState s -> f (SigState s)
transSt = (SigState s -> State s)
-> (SigState s -> State s -> SigState s)
-> Lens (SigState s) (SigState s) (State s) (State s)
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 -> State s -> Signal s -> SigState s
forall s. State s -> Signal s -> SigState s
SigState State s
st Signal s
x)
transSig :: Lens' (SigState s) (Signal s)
transSig :: (Signal s -> f (Signal s)) -> SigState s -> f (SigState s)
transSig = (SigState s -> Signal s)
-> (SigState s -> Signal s -> SigState s)
-> Lens (SigState s) (SigState s) (Signal s) (Signal s)
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 -> State s -> Signal s -> SigState s
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))
data Trace s
= Trace
{ Trace s -> Environment s
_traceEnv :: !(Environment s)
, Trace s -> State s
_traceInitState :: !(State s)
, Trace s -> StrictSeq (SigState s)
_traceTrans :: !(StrictSeq (SigState 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
makeLenses ''Trace
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))
mkTrace :: Environment s -> State s -> [(State s, Signal s)] -> Trace s
mkTrace :: Environment s -> State s -> [(State s, Signal s)] -> Trace s
mkTrace Environment s
env State s
initState [(State s, Signal s)]
sigs = Environment s -> State s -> StrictSeq (SigState s) -> Trace s
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' = (State s -> Signal s -> SigState s)
-> (State s, Signal s) -> SigState s
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry State s -> Signal s -> SigState s
forall s. State s -> Signal s -> SigState s
SigState ((State s, Signal s) -> SigState s)
-> StrictSeq (State s, Signal s) -> StrictSeq (SigState s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(State s, Signal s)] -> StrictSeq (State s, Signal s)
forall a. [a] -> StrictSeq a
StrictSeq.fromList [(State s, Signal s)]
sigs
lastState :: Trace s -> State s
lastState :: 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
lastSignal :: HasCallStack => Trace s -> Signal s
lastSignal :: 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 -> String -> Signal s
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
firstAndLastState :: Trace s -> (State s, State s)
firstAndLastState :: Trace s -> (State s, State s)
firstAndLastState Trace s
tr = (Trace s -> State s
forall s. Trace s -> State s
_traceInitState Trace s
tr, Trace s -> State s
forall s. Trace s -> State s
lastState Trace s
tr)
data TraceOrder = NewestFirst | OldestFirst deriving (TraceOrder -> TraceOrder -> Bool
(TraceOrder -> TraceOrder -> Bool)
-> (TraceOrder -> TraceOrder -> Bool) -> Eq TraceOrder
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 :: TraceOrder -> [a] -> [a]
fromNewestFirst TraceOrder
NewestFirst = [a] -> [a]
forall a. a -> a
id
fromNewestFirst TraceOrder
OldestFirst = [a] -> [a]
forall a. [a] -> [a]
reverse
traceSignals :: TraceOrder -> Trace s -> [Signal s]
traceSignals :: TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
order Trace s
tr = TraceOrder -> [Signal s] -> [Signal s]
forall a. TraceOrder -> [a] -> [a]
fromNewestFirst TraceOrder
order (Trace s
tr Trace s
-> Getting (Endo [Signal s]) (Trace s) (Signal s) -> [Signal s]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (StrictSeq (SigState s)
-> Const (Endo [Signal s]) (StrictSeq (SigState s)))
-> Trace s -> Const (Endo [Signal s]) (Trace s)
forall s. Lens' (Trace s) (StrictSeq (SigState s))
traceTrans ((StrictSeq (SigState s)
-> Const (Endo [Signal s]) (StrictSeq (SigState s)))
-> Trace s -> Const (Endo [Signal s]) (Trace s))
-> ((Signal s -> Const (Endo [Signal s]) (Signal s))
-> StrictSeq (SigState s)
-> Const (Endo [Signal s]) (StrictSeq (SigState s)))
-> Getting (Endo [Signal s]) (Trace s) (Signal s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SigState s -> Const (Endo [Signal s]) (SigState s))
-> StrictSeq (SigState s)
-> Const (Endo [Signal s]) (StrictSeq (SigState s))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((SigState s -> Const (Endo [Signal s]) (SigState s))
-> StrictSeq (SigState s)
-> Const (Endo [Signal s]) (StrictSeq (SigState s)))
-> ((Signal s -> Const (Endo [Signal s]) (Signal s))
-> SigState s -> Const (Endo [Signal s]) (SigState s))
-> (Signal s -> Const (Endo [Signal s]) (Signal s))
-> StrictSeq (SigState s)
-> Const (Endo [Signal s]) (StrictSeq (SigState s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signal s -> Const (Endo [Signal s]) (Signal s))
-> SigState s -> Const (Endo [Signal s]) (SigState s)
forall s. Lens' (SigState s) (Signal s)
transSig)
traceStates :: TraceOrder -> Trace s -> [State s]
traceStates :: TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
order Trace s
tr = TraceOrder -> [State s] -> [State s]
forall a. TraceOrder -> [a] -> [a]
fromNewestFirst TraceOrder
order ([State s]
xs [State s] -> [State s] -> [State s]
forall a. [a] -> [a] -> [a]
++ [State s
x])
where
x :: State s
x = Trace s
tr Trace s -> Getting (State s) (Trace s) (State s) -> State s
forall s a. s -> Getting a s a -> a
^. Getting (State s) (Trace s) (State s)
forall s. Lens' (Trace s) (State s)
traceInitState
xs :: [State s]
xs = Trace s
tr Trace s
-> Getting (Endo [State s]) (Trace s) (State s) -> [State s]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (StrictSeq (SigState s)
-> Const (Endo [State s]) (StrictSeq (SigState s)))
-> Trace s -> Const (Endo [State s]) (Trace s)
forall s. Lens' (Trace s) (StrictSeq (SigState s))
traceTrans ((StrictSeq (SigState s)
-> Const (Endo [State s]) (StrictSeq (SigState s)))
-> Trace s -> Const (Endo [State s]) (Trace s))
-> ((State s -> Const (Endo [State s]) (State s))
-> StrictSeq (SigState s)
-> Const (Endo [State s]) (StrictSeq (SigState s)))
-> Getting (Endo [State s]) (Trace s) (State s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SigState s -> Const (Endo [State s]) (SigState s))
-> StrictSeq (SigState s)
-> Const (Endo [State s]) (StrictSeq (SigState s))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((SigState s -> Const (Endo [State s]) (SigState s))
-> StrictSeq (SigState s)
-> Const (Endo [State s]) (StrictSeq (SigState s)))
-> ((State s -> Const (Endo [State s]) (State s))
-> SigState s -> Const (Endo [State s]) (SigState s))
-> (State s -> Const (Endo [State s]) (State s))
-> StrictSeq (SigState s)
-> Const (Endo [State s]) (StrictSeq (SigState s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State s -> Const (Endo [State s]) (State s))
-> SigState s -> Const (Endo [State s]) (SigState s)
forall s. Lens' (SigState s) (State s)
transSt
traceLength :: Trace s -> Int
traceLength :: Trace s -> Int
traceLength Trace s
tr = Trace s
tr Trace s -> Getting Int (Trace s) Int -> Int
forall s a. s -> Getting a s a -> a
^. (StrictSeq (SigState s) -> Const Int (StrictSeq (SigState s)))
-> Trace s -> Const Int (Trace s)
forall s. Lens' (Trace s) (StrictSeq (SigState s))
traceTrans ((StrictSeq (SigState s) -> Const Int (StrictSeq (SigState s)))
-> Trace s -> Const Int (Trace s))
-> ((Int -> Const Int Int)
-> StrictSeq (SigState s) -> Const Int (StrictSeq (SigState s)))
-> Getting Int (Trace s) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictSeq (SigState s) -> Int)
-> SimpleGetter (StrictSeq (SigState s)) Int
forall s a. (s -> a) -> SimpleGetter s a
to StrictSeq (SigState s) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
traceInit :: HasCallStack => Trace s -> Trace s
traceInit :: 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 -> String -> Trace s
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 }
preStatesAndSignals :: TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals :: TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals TraceOrder
OldestFirst Trace s
tr
= [State s] -> [Signal s] -> [(State s, Signal s)]
forall a b. [a] -> [b] -> [(a, b)]
zip (TraceOrder -> Trace s -> [State s]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace s
tr) (TraceOrder -> Trace s -> [Signal s]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace s
tr)
preStatesAndSignals TraceOrder
NewestFirst Trace s
tr
= [(State s, Signal s)] -> [(State s, Signal s)]
forall a. [a] -> [a]
reverse ([(State s, Signal s)] -> [(State s, Signal s)])
-> [(State s, Signal s)] -> [(State s, Signal s)]
forall a b. (a -> b) -> a -> b
$ TraceOrder -> Trace s -> [(State s, Signal s)]
forall s. TraceOrder -> Trace s -> [(State s, Signal s)]
preStatesAndSignals TraceOrder
OldestFirst Trace s
tr
closure
:: forall s m
. (STS s, m ~ BaseM s)
=> Environment s
-> State s
-> [Signal s]
-> m (Trace s)
closure :: Environment s -> State s -> [Signal s] -> m (Trace s)
closure Environment s
env State s
st0 [Signal s]
sigs = Environment s -> State s -> [(State s, Signal s)] -> Trace s
forall s.
Environment s -> State s -> [(State s, Signal s)] -> Trace s
mkTrace Environment s
env State s
st0 ([(State s, Signal s)] -> Trace s)
-> m [(State s, Signal s)] -> m (Trace s)
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 ([Signal s] -> [Signal s]
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 = [(State s, Signal s)] -> m [(State s, Signal s)]
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 =
RuleContext 'Transition s
-> m (Either [[PredicateFailure s]] (State s))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
applySTSTest @s ((Environment s, State s, Signal s) -> TRC s
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC(Environment s
env, State s
sti, Signal s
sig)) m (Either [[PredicateFailure s]] (State s))
-> (Either [[PredicateFailure s]] (State s)
-> m [(State s, Signal s)])
-> m [(State s, Signal s)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left [[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) (State s, Signal s)
-> [(State s, Signal s)] -> [(State s, Signal s)]
forall a. a -> [a] -> [a]
: [(State s, Signal s)]
acc)
(.-)
:: forall m st sig err
. ( MonadIO m
, MonadReader (st -> sig -> Either err st) m
, Show err
)
=> m st -> sig -> m st
m st
mSt .- :: m st -> sig -> m st
.- sig
sig = do
st
st <- m st
mSt
st -> sig -> Either err st
validate <- m (st -> sig -> Either err st)
forall r (m :: * -> *). MonadReader r m => m r
ask
case st -> sig -> Either err st
validate st
st sig
sig of
Left err
pfs -> IO st -> m st
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO st -> m st) -> (err -> IO st) -> err -> m st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO st
forall a. HasCallStack => String -> IO a
assertFailure (String -> IO st) -> (err -> String) -> err -> IO st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. err -> String
forall a. Show a => a -> String
show (err -> m st) -> err -> m st
forall a b. (a -> b) -> a -> b
$ err
pfs
Right st
st' -> st -> m st
forall (f :: * -> *) a. Applicative f => a -> f a
pure st
st'
(.->)
:: forall m st
. (MonadIO m, Eq st, Show st)
=> m st -> st -> m st
m st
mSt .-> :: m st -> st -> m st
.-> st
stExpected = do
st
stActual <- m st
mSt
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ st
stActual st -> st -> IO ()
forall a. (Eq a, Show a, HasCallStack) => a -> a -> IO ()
@?= st
stExpected
st -> m st
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 [[PredicateFailure s]] (State s))) IO (State s)
-> IO ()
checkTrace :: (forall a. m a -> a)
-> Environment s
-> ReaderT
(State s -> Signal s -> Either [[PredicateFailure s]] (State s))
IO
(State s)
-> IO ()
checkTrace forall a. m a -> a
interp Environment s
env ReaderT
(State s -> Signal s -> Either [[PredicateFailure s]] (State s))
IO
(State s)
act =
IO (State s) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO (State s) -> IO ()) -> IO (State s) -> IO ()
forall a b. (a -> b) -> a -> b
$ ReaderT
(State s -> Signal s -> Either [[PredicateFailure s]] (State s))
IO
(State s)
-> (State s -> Signal s -> Either [[PredicateFailure s]] (State s))
-> IO (State s)
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT
(State s -> Signal s -> Either [[PredicateFailure s]] (State s))
IO
(State s)
act (\State s
st Signal s
sig -> m (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall a. m a -> a
interp (m (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s))
-> m (Either [[PredicateFailure s]] (State s))
-> Either [[PredicateFailure s]] (State s)
forall a b. (a -> b) -> a -> b
$ RuleContext 'Transition s
-> m (Either [[PredicateFailure s]] (State s))
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
applySTSTest ((Environment s, State s, Signal s) -> TRC s
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC(Environment s
env, State s
st, Signal s
sig)))
extractValues :: forall d a . (Data d, Typeable a) => d -> [a]
d
d = [Maybe a] -> [a]
forall a. [Maybe a] -> [a]
catMaybes ((forall d. Data d => d -> Maybe a) -> d -> [Maybe a]
forall a u. Data a => (forall d. Data d => d -> u) -> a -> [u]
gmapQ forall d. Data d => d -> Maybe a
extractValue d
d)
[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((forall d. Data d => d -> [a]) -> d -> [[a]]
forall a u. Data a => (forall d. Data d => d -> u) -> a -> [u]
gmapQ forall d. Data d => d -> [a]
forall d a. (Data d, Typeable a) => d -> [a]
extractValues d
d)
where
extractValue :: forall d1 . (Data d1) => d1 -> Maybe a
extractValue :: d1 -> Maybe a
extractValue d1
d1 = d1 -> Maybe a
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast d1
d1
data SourceSignalTarget a =
SourceSignalTarget {
SourceSignalTarget a -> State a
source :: State a
, SourceSignalTarget a -> State a
target :: State 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)
sourceSignalTargets :: forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets :: Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace a
trace = (State a -> State a -> Signal a -> SourceSignalTarget a)
-> [State a] -> [State a] -> [Signal a] -> [SourceSignalTarget a]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 State a -> State a -> Signal a -> SourceSignalTarget a
forall a. State a -> State a -> Signal a -> SourceSignalTarget a
SourceSignalTarget [State a]
states ([State a] -> [State a]
forall a. [a] -> [a]
tail [State a]
states) [Signal a]
signals
where
states :: [State a]
states = TraceOrder -> Trace a -> [State a]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace a
trace
signals :: [Signal a]
signals = TraceOrder -> Trace a -> [Signal a]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace a
trace
applySTSTest ::
forall s m rtype.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s ->
m (Either [[PredicateFailure s]] (State s))
applySTSTest :: RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
applySTSTest RuleContext rtype s
ctx =
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts
-> RuleContext rtype s -> m (State s, [[PredicateFailure s]])
applySTSOpts ApplySTSOpts
defaultOpts RuleContext rtype s
ctx m (State s, [[PredicateFailure s]])
-> ((State s, [[PredicateFailure s]])
-> Either [[PredicateFailure s]] (State s))
-> m (Either [[PredicateFailure s]] (State s))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
(State s
st, []) -> State s -> Either [[PredicateFailure s]] (State s)
forall a b. b -> Either a b
Right State s
st
(State s
_, [[PredicateFailure s]]
pfs) -> [[PredicateFailure s]] -> Either [[PredicateFailure s]] (State s)
forall a b. a -> Either a b
Left [[PredicateFailure s]]
pfs
where
defaultOpts :: ApplySTSOpts
defaultOpts =
ApplySTSOpts :: AssertionPolicy -> ValidationPolicy -> ApplySTSOpts
ApplySTSOpts
{ asoAssertions :: AssertionPolicy
asoAssertions = AssertionPolicy
AssertionsAll,
asoValidation :: ValidationPolicy
asoValidation = ValidationPolicy
ValidateAll
}