Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Traces of transition systems and associated operators.
This module also includes a minimal domain-specific-language to specify expectations on traces.
Synopsis
- data SigState s = SigState !(State s) !(Signal s)
- (.-) ∷ ∀ m st sig err. (MonadIO m, MonadReader (st → sig → Either err st) m, Show err, HasCallStack) ⇒ m st → sig → m st
- (.->) ∷ ∀ m st. (MonadIO m, Eq st, Show st, HasCallStack) ⇒ m st → st → m st
- (.->>) ∷ ∀ m st. (MonadIO m, Eq st, ToExpr st, HasCallStack) ⇒ m st → st → m st
- 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 ()
- data Trace s = Trace {
- _traceEnv ∷ !(Environment s)
- _traceInitState ∷ !(State s)
- _traceTrans ∷ !(StrictSeq (SigState s))
- data TraceOrder
- mkTrace ∷ Environment s → State s → [(State s, Signal s)] → Trace s
- traceEnv ∷ ∀ s. Lens' (Trace s) (Environment s)
- traceInitState ∷ ∀ s. Lens' (Trace s) (State s)
- traceSignals ∷ TraceOrder → Trace s → [Signal s]
- traceStates ∷ TraceOrder → Trace s → [State s]
- preStatesAndSignals ∷ TraceOrder → Trace s → [(State s, Signal s)]
- data SourceSignalTarget a = SourceSignalTarget {}
- sourceSignalTargets ∷ ∀ a. Trace a → [SourceSignalTarget a]
- traceLength ∷ Trace s → Int
- traceInit ∷ HasCallStack ⇒ Trace s → Trace s
- lastState ∷ Trace s → State s
- lastSignal ∷ HasCallStack ⇒ Trace s → Signal s
- firstAndLastState ∷ Trace s → (State s, State s)
- closure ∷ ∀ s m. (STS s, m ~ BaseM s) ⇒ Environment s → State s → [Signal s] → m (Trace s)
- extractValues ∷ ∀ d a. (Data d, Typeable a) ⇒ d → [a]
- applySTSTest ∷ ∀ s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) ⇒ RuleContext rtype s → m (Either (NonEmpty (PredicateFailure s)) (State s))
- getEvents ∷ ∀ sts. STS sts ⇒ Trace sts → BaseM sts [[Event sts]]
- splitTrace ∷ (State s → State s → Bool) → Trace s → [Trace s]
Documentation
Instances
Generic (SigState s) Source # | |
(Show (State s), Show (Signal s)) ⇒ Show (SigState s) Source # | |
(Eq (State s), Eq (Signal s)) ⇒ Eq (SigState s) Source # | |
(NoThunks (State s), NoThunks (Signal s)) ⇒ NoThunks (SigState s) Source # | |
type Rep (SigState s) Source # | |
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 ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (State s)) :*: S1 ('MetaSel ('Nothing ∷ Maybe 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
A successful trace of a transition system.
Trace | |
|
Instances
data TraceOrder Source #
Instances
Eq TraceOrder Source # | |
Defined in Test.Control.State.Transition.Trace (==) ∷ TraceOrder → TraceOrder → Bool Source # (/=) ∷ TraceOrder → TraceOrder → Bool Source # |
mkTrace ∷ Environment s → State s → [(State s, Signal s)] → Trace s Source #
Make a trace given an environment and initial state.
traceSignals ∷ TraceOrder → Trace 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"]
traceStates ∷ TraceOrder → Trace 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]
preStatesAndSignals ∷ TraceOrder → Trace 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")]
data SourceSignalTarget a Source #
Instances
(Show (State a), Show (Signal a)) ⇒ Show (SourceSignalTarget a) Source # | |
Defined in Test.Control.State.Transition.Trace | |
(Eq (State a), Eq (Signal a)) ⇒ Eq (SourceSignalTarget a) Source # | |
Defined in Test.Control.State.Transition.Trace (==) ∷ SourceSignalTarget a → SourceSignalTarget a → Bool Source # (/=) ∷ SourceSignalTarget a → SourceSignalTarget a → Bool Source # |
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"}]
traceLength ∷ Trace 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
traceInit ∷ HasCallStack ⇒ Trace 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"]}}
lastState ∷ Trace 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
lastSignal ∷ HasCallStack ⇒ Trace 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"
firstAndLastState ∷ Trace 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)
∷ ∀ 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.