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.

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.

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.

A successful trace of a transition system.

Make a trace given an environment and initial state.

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

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]

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

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

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

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

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

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"

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)

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

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"

Apply STS checking assertions.

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

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.