small-steps-1.1.0.1: Small step semantics
Safe HaskellSafe-Inferred
LanguageHaskell2010

Test.Control.State.Transition.Trace

Description

Traces of transition systems and associated operators.

This module also includes a minimal domain-specific-language to specify expectations on traces.

Synopsis

Documentation

data SigState s Source #

Constructors

SigState !(State s) !(Signal s) 

Instances

Instances details
Generic (SigState s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

Associated Types

type Rep (SigState s) ∷ TypeType Source #

Methods

fromSigState s → Rep (SigState s) x Source #

toRep (SigState s) x → SigState s Source #

(Show (State s), Show (Signal s)) ⇒ Show (SigState s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

(Eq (State s), Eq (Signal s)) ⇒ Eq (SigState s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

Methods

(==)SigState s → SigState s → Bool Source #

(/=)SigState s → SigState s → Bool Source #

(NoThunks (State s), NoThunks (Signal s)) ⇒ NoThunks (SigState s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

type Rep (SigState s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

type Rep (SigState s) = D1 ('MetaData "SigState" "Test.Control.State.Transition.Trace" "small-steps-1.1.0.1-inplace-testlib" 'False) (C1 ('MetaCons "SigState" 'PrefixI 'False) (S1 ('MetaSel ('NothingMaybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (State s)) :*: S1 ('MetaSel ('NothingMaybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Signal s))))

Trace checking

(.-) ∷ ∀ m st sig err. (MonadIO m, MonadReader (st → sig → Either err st) m, Show err, HasCallStack) ⇒ m st → sig → m st Source #

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.

(.->) ∷ ∀ m st. (MonadIO m, Eq st, Show st, HasCallStack) ⇒ m st → st → m st Source #

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.

(.->>) ∷ ∀ m st. (MonadIO m, Eq st, ToExpr st, HasCallStack) ⇒ m st → st → m st Source #

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.

checkTrace ∷ ∀ s m. (STS s, BaseM s ~ m) ⇒ (∀ a. m a → a) → Environment s → ReaderT (State s → Signal s → Either (NonEmpty (PredicateFailure s)) (State s)) IO (State s) → IO () Source #

Trace

data Trace s Source #

A successful trace of a transition system.

Constructors

Trace 

Fields

Instances

Instances details
Generic (Trace s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

Associated Types

type Rep (Trace s) ∷ TypeType Source #

Methods

fromTrace s → Rep (Trace s) x Source #

toRep (Trace s) x → Trace s Source #

(Show (State s), Show (Signal s), Show (Environment s)) ⇒ Show (Trace s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

Methods

showsPrecIntTrace s → ShowS Source #

showTrace s → String Source #

showList ∷ [Trace s] → ShowS Source #

(NFData (Environment s), NFData (State s), NFData (SigState s)) ⇒ NFData (Trace s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

Methods

rnfTrace s → () Source #

(Eq (State s), Eq (Signal s), Eq (Environment s)) ⇒ Eq (Trace s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

Methods

(==)Trace s → Trace s → Bool Source #

(/=)Trace s → Trace s → Bool Source #

(NoThunks (Environment s), NoThunks (State s), NoThunks (Signal s)) ⇒ NoThunks (Trace s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

type Rep (Trace s) Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

type Rep (Trace s) = D1 ('MetaData "Trace" "Test.Control.State.Transition.Trace" "small-steps-1.1.0.1-inplace-testlib" 'False) (C1 ('MetaCons "Trace" 'PrefixI 'True) (S1 ('MetaSel ('Just "_traceEnv") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Environment s)) :*: (S1 ('MetaSel ('Just "_traceInitState") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (State s)) :*: S1 ('MetaSel ('Just "_traceTrans") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (StrictSeq (SigState s))))))

data TraceOrder Source #

Constructors

NewestFirst 
OldestFirst 

Instances

Instances details
Eq TraceOrder Source # 
Instance details

Defined in Test.Control.State.Transition.Trace

mkTraceEnvironment s → State s → [(State s, Signal s)] → Trace s Source #

Make a trace given an environment and initial state.

traceEnv ∷ ∀ s. Lens' (Trace s) (Environment s) Source #

traceInitState ∷ ∀ s. Lens' (Trace s) (State s) Source #

traceSignalsTraceOrderTrace s → [Signal s] Source #

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"]

traceStatesTraceOrderTrace s → [State s] Source #

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]

preStatesAndSignalsTraceOrderTrace s → [(State s, Signal s)] Source #

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")]

sourceSignalTargets ∷ ∀ a. Trace a → [SourceSignalTarget a] Source #

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"}]

traceLengthTrace s → Int Source #

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

traceInitHasCallStackTrace s → Trace s Source #

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"]}}

lastStateTrace s → State s Source #

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

lastSignalHasCallStackTrace s → Signal s Source #

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"

firstAndLastStateTrace s → (State s, State s) Source #

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)

closure Source #

Arguments

∷ ∀ s m. (STS s, m ~ BaseM s) 
Environment s 
State s 
→ [Signal s]

List of signals to apply, where the newest signal comes first.

→ m (Trace s) 

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)]}}

Miscellaneous utilities

extractValues ∷ ∀ d a. (Data d, Typeable a) ⇒ d → [a] Source #

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"

applySTSTest ∷ ∀ s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) ⇒ RuleContext rtype s → m (Either (NonEmpty (PredicateFailure s)) (State s)) Source #

Apply STS checking assertions.

getEvents ∷ ∀ sts. STS sts ⇒ Trace sts → BaseM sts [[Event sts]] Source #

Extract the Events from a trace, by re-applying the signal with assertions and vaidations turned off, but events turned on.

splitTrace ∷ (State s → State s → Bool) → Trace s → [Trace s] Source #

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.