Safe Haskell | None |
---|---|
Language | Haskell2010 |
Control.State.Transition.Generator
Description
Generators for transition systems.
How should these work? - We start with some initial environment. - We start with some initial base state. - We generate a stream of signals. These might be influenced by some running state - We run each signal through
Synopsis
- class STS s => HasTrace s
- type SignalGenerator s = Environment s -> State s -> Gen (Signal s)
- type family BaseEnv s :: Type
- interpretSTS :: forall a. HasTrace s => BaseEnv s -> BaseM s a -> a
- envGen :: HasTrace s => Word64 -> Gen (Environment s)
- sigGen :: HasTrace s => SignalGenerator s
- traceSigGen :: forall s. HasTrace s => BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)
- genTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> Environment s -> State s -> SignalGenerator s -> Gen (Trace s)
- trace :: HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
- traceWithProfile :: HasTrace s => BaseEnv s -> Word64 -> TraceProfile s -> Gen (Trace s)
- traceOfLength :: HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
- traceOfLengthWithInitState :: HasTrace s => BaseEnv s -> Word64 -> (Environment s -> Gen (State s)) -> Gen (Trace s)
- traceSuchThat :: forall s. HasTrace s => BaseEnv s -> Word64 -> (Trace s -> Bool) -> Gen (Trace s)
- ofLengthAtLeast :: Gen (Trace s) -> Int -> Gen (Trace s)
- suchThatLastState :: forall s. Gen (Trace s) -> (State s -> Bool) -> Gen (Trace s)
- nonTrivialTrace :: forall s. (HasTrace s, HasSizeInfo (Signal s)) => BaseEnv s -> Word64 -> Gen (Trace s)
- class HasSizeInfo sig
- isTrivial :: HasSizeInfo sig => sig -> Bool
- sampleMaxTraceSize :: forall s. HasTrace s => BaseEnv s -> Word64 -> Int -> Word64 -> IO Int
- randomTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
- randomTraceOfSize :: forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
- data TraceLength
- data TraceProfile s = TraceProfile {
- proportionOfValidSignals :: !Int
- failures :: ![(Int, SignalGenerator s)]
- proportionOfInvalidSignals :: TraceProfile s -> Int
- invalidTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)
- classifyTraceLength :: Trace s -> Word64 -> Word64 -> PropertyT IO ()
- classifySize :: (Ord n, Show n, Integral n) => String -> a -> (a -> n) -> n -> n -> PropertyT IO ()
- mkIntervals :: Integral n => n -> n -> n -> [(n, n)]
- ratio :: Integral a => (Trace s -> a) -> Trace s -> Double
- traceLengthsAreClassified :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s)) => BaseEnv s -> Word64 -> Word64 -> Property
- onlyValidSignalsAreGenerated :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) => BaseEnv s -> Word64 -> Property
- onlyValidSignalsAreGeneratedForTrace :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) => BaseEnv s -> Gen (Trace s) -> Property
- invalidSignalsAreGenerated :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) => BaseEnv s -> [(Int, SignalGenerator s)] -> Word64 -> ([[PredicateFailure s]] -> PropertyT IO ()) -> Property
- tinkerWithSigGen :: forall g sts. (HasTrace sts, Goblin g (Signal sts), SeedGoblin (Environment sts), SeedGoblin (State sts)) => GoblinData g -> Environment sts -> State sts -> Gen (Signal sts)
- coverFailures :: forall m s a. (MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) => CoverPercentage -> [PredicateFailure s] -> a -> m ()
Documentation
type SignalGenerator s = Environment s -> State s -> Gen (Signal s) Source #
interpretSTS :: forall a. HasTrace s => BaseEnv s -> BaseM s a -> a Source #
Interpret the action from the base monad into a pure value, given some initial environment. This obviously places some contraints on the nature of the base monad for a trace to be completed.
Arguments
:: HasTrace s | |
=> Word64 | Trace length that will be used by |
-> Gen (Environment s) |
Generate an initial environment that is based on the given trace length.
sigGen :: HasTrace s => SignalGenerator s Source #
Generate a (valid) signal given an environment and a pre-state.
traceSigGen :: forall s. HasTrace s => BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s) Source #
Arguments
:: forall s. HasTrace s | |
=> BaseEnv s | |
-> Word64 | Trace upper bound. This will be linearly scaled as a function of the generator size. |
-> Environment s | Environment, which remains constant in the system. |
-> State s | Initial state. |
-> SignalGenerator s | Signal generator. This generator relies on an environment and a state to generate a signal. |
-> Gen (Trace s) |
Return a (valid) trace generator given an initial state, environment, and signal generator.
traceWithProfile :: HasTrace s => BaseEnv s -> Word64 -> TraceProfile s -> Gen (Trace s) Source #
traceOfLengthWithInitState Source #
Arguments
:: HasTrace s | |
=> BaseEnv s | |
-> Word64 | Desired length of the generated trace. If the signal generator can generate invalid signals then the resulting trace might not have the given length. |
-> (Environment s -> Gen (State s)) | A generator for Initial State, given the STS environment |
-> Gen (Trace s) |
traceSuchThat :: forall s. HasTrace s => BaseEnv s -> Word64 -> (Trace s -> Bool) -> Gen (Trace s) Source #
nonTrivialTrace :: forall s. (HasTrace s, HasSizeInfo (Signal s)) => BaseEnv s -> Word64 -> Gen (Trace s) Source #
Generate a trace that contains at least one non-trivial signal. See
HasSizeInfo
.
class HasSizeInfo sig Source #
Minimal complete definition
Instances
HasSizeInfo [a] Source # | |
Defined in Control.State.Transition.Generator |
isTrivial :: HasSizeInfo sig => sig -> Bool Source #
Arguments
:: forall s. HasTrace s | |
=> BaseEnv s | |
-> Word64 | Trace's upper bound |
-> Int | Generator size |
-> Word64 | Number of samples to take |
-> IO Int |
Sample the maximum trace size, given the generator size and number of samples.
data TraceProfile s Source #
Constructors
TraceProfile | |
Fields
|
proportionOfInvalidSignals :: TraceProfile s -> Int Source #
Invalid trace generation
Arguments
:: forall s. HasTrace s | |
=> BaseEnv s | |
-> Word64 | Maximum length of the generated traces. |
-> [(Int, SignalGenerator s)] | Trace failure profile to be used to get an invalid signal. |
-> Gen (Trace s) |
Generate an invalid trace
Trace classification
Arguments
:: Trace s | |
-> Word64 | Maximum size of the traces |
-> Word64 | Steps used to divide the interval |
-> PropertyT IO () |
Classify the trace length as either:
- being empty
- being a singleton
- having the given maximum size
- belonging to one of the intervals between 2 and the maximum size - 1. The
number of intervals are determined by the
step
parameter.
Arguments
:: (Ord n, Show n, Integral n) | |
=> String | Prefix to be added to the label intervals |
-> a | Value to classify |
-> (a -> n) | Size function |
-> n | Maximum value size |
-> n | Steps used to divide the size interval |
-> PropertyT IO () |
Classify the value size as either:
- being empty
- being a singleton
- having the given maximum size
- belonging to one of the intervals between 2 and the maximum size - 1. The
number of intervals are determined by the
step
parameter.
Arguments
:: Integral n | |
=> n | Interval lower bound |
-> n | Interval upper bound |
-> n | Step size, used to divide the interval in sub-intervals of the same length. |
-> [(n, n)] |
Given a lower bound low
, an upper bound high
and a step size step
(both of which must be positive), divide the interval [0, ub]
into
sub-intervals of step
size.
If any of these values is negative the empty list will be returned.
Examples:
>>>
mkIntervals 0 0 0 :: [(Int, Int)]
[]
>>>
mkIntervals 0 10 2 :: [(Int, Int)]
[(0,2),(2,4),(4,6),(6,8),(8,10)]
>>>
mkIntervals 1 10 2 :: [(Int, Int)]
[(1,3),(3,5),(5,7),(7,9),(9,10)]
>>>
mkIntervals 3 10 3 :: [(Int, Int)]
[(3,6),(6,9),(9,10)]
>>>
mkIntervals 5 2 3 :: [(Int, Int)]
[]
>>>
mkIntervals (-1) 10 3 :: [(Int, Int)]
[]
>>>
mkIntervals 1 (-10) 3 :: [(Int, Int)]
[]
>>>
mkIntervals 1 1000 (-100) :: [(Int, Int)]
[]
ratio :: Integral a => (Trace s -> a) -> Trace s -> Double Source #
Given a function that computes an integral value from a trace, return that value as a ratio of the trace length.
Trace properties
traceLengthsAreClassified Source #
Arguments
:: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s)) | |
=> BaseEnv s | |
-> Word64 | Maximum trace length that the signal generator of |
-> Word64 | Lengths of the intervals in which the lengths range should be split. |
-> Property |
Property that simply classifies the lengths of the generated traces.
onlyValidSignalsAreGenerated Source #
Arguments
:: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) | |
=> BaseEnv s | |
-> Word64 | Maximum trace length. |
-> Property |
Check that the signal generator of s
only generate valid signals.
onlyValidSignalsAreGeneratedForTrace :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) => BaseEnv s -> Gen (Trace s) -> Property Source #
Check that the signal generator of s
only generate valid signals.
invalidSignalsAreGenerated Source #
Arguments
:: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) | |
=> BaseEnv s | |
-> [(Int, SignalGenerator s)] | Failure profile. |
-> Word64 | Maximum trace length. |
-> ([[PredicateFailure s]] -> PropertyT IO ()) | Action to run when the an invalid signal is generated. |
-> Property |
Helpers
tinkerWithSigGen :: forall g sts. (HasTrace sts, Goblin g (Signal sts), SeedGoblin (Environment sts), SeedGoblin (State sts)) => GoblinData g -> Environment sts -> State sts -> Gen (Signal sts) Source #
Arguments
:: forall m s a. (MonadTest m, HasCallStack, Data (PredicateFailure s), Data a) | |
=> CoverPercentage | |
-> [PredicateFailure s] | Target predicate failures |
-> a | Structure containing the failures |
-> m () |