-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Small step semantics testing library
--   
--   Small step semantics testing library
@package small-steps-test
@version 0.1.0.0


-- | Traces of transition systems and associated operators.
--   
--   This module also includes a minimal domain-specific-language to
--   specify expectations on traces.
module Control.State.Transition.Trace

-- | Bind the state inside the first argument, and apply the transition
--   function in the <tt>Reader</tt> environment to that state and given
--   signal, obtaining the resulting state, or an assertion failure if the
--   transition function fails.
(.-) :: forall m st sig err. (MonadIO m, MonadReader (st -> sig -> Either err st) m, Show err) => m st -> sig -> m st

-- | Bind the state inside the first argument, and check whether it is
--   equal to the expected state, given in the second argument.
(.->) :: forall m st. (MonadIO m, Eq st, Show st) => m st -> st -> m st
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 ()

-- | A successful trace of a transition system.
data Trace s
Trace :: !Environment s -> !State s -> !StrictSeq (SigState s) -> Trace s

-- | Environment under which the trace was run.
[_traceEnv] :: Trace s -> !Environment s

-- | Initial state in the trace
[_traceInitState] :: Trace s -> !State s

-- | Signals and resulting states observed in the trace. New elements are
--   put in front of the list.
[_traceTrans] :: Trace s -> !StrictSeq (SigState s)
data TraceOrder
NewestFirst :: TraceOrder
OldestFirst :: TraceOrder

-- | Make a trace given an environment and initial state.
mkTrace :: Environment s -> State s -> [(State s, Signal s)] -> Trace s
traceEnv :: forall s_agww. Lens' (Trace s_agww) (Environment s_agww)
traceInitState :: forall s_agww. Lens' (Trace s_agww) (State s_agww)

-- | Retrieve all the signals in the trace, in the order specified.
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceSignals NewestFirst tr0
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceSignals NewestFirst tr01
--   ["one"]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; traceSignals OldestFirst tr01
--   ["one"]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceSignals NewestFirst tr0123
--   ["three","two","one"]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; traceSignals OldestFirst tr0123
--   ["one","two","three"]
--   </pre>
traceSignals :: TraceOrder -> Trace s -> [Signal s]

-- | Retrieve all the states in the trace, in the order specified.
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceStates NewestFirst tr0
--   [0]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; traceStates OldestFirst tr0
--   [0]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceStates NewestFirst tr0123
--   [3,2,1,0]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; traceStates OldestFirst tr0123
--   [0,1,2,3]
--   </pre>
traceStates :: TraceOrder -> Trace s -> [State s]

-- | 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
--   
--   <pre>
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; preStatesAndSignals NewestFirst tr0
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; preStatesAndSignals OldestFirst tr0
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; preStatesAndSignals OldestFirst tr0123
--   [(0,"one"),(1,"two"),(2,"three")]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; preStatesAndSignals NewestFirst tr0123
--   [(2,"three"),(1,"two"),(0,"one")]
--   </pre>
preStatesAndSignals :: TraceOrder -> Trace s -> [(State s, Signal s)]
data SourceSignalTarget a
SourceSignalTarget :: State a -> State a -> Signal a -> SourceSignalTarget a
[source] :: SourceSignalTarget a -> State a
[target] :: SourceSignalTarget a -> State a
[signal] :: SourceSignalTarget a -> Signal a

-- | 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
--   
--   <pre>
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; sourceSignalTargets tr0
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; sourceSignalTargets tr0123
--   [SourceSignalTarget {source = 0, target = 1, signal = "one"},SourceSignalTarget {source = 1, target = 2, signal = "two"},SourceSignalTarget {source = 2, target = 3, signal = "three"}]
--   </pre>
sourceSignalTargets :: forall a. Trace a -> [SourceSignalTarget a]

-- | Compute the length of a trace, defined as the number of signals it
--   contains.
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceLength tr0
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceLength tr0123
--   3
--   </pre>
traceLength :: Trace s -> Int

-- | Take all but the newest signal in the trace.
--   
--   Precondition: the trace must contain at least one signal
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; :set -XScopedTypeVariables
--   
--   &gt;&gt;&gt; import Control.Exception (catch, ErrorCall)
--   
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; print (traceInit tr0) `catch` (\(_ :: ErrorCall) -&gt; print "error!")
--   "error!"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceInit tr01
--   Trace {_traceEnv = True, _traceInitState = 0, _traceTrans = StrictSeq {fromStrict = fromList []}}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr012 = mkTrace True 0 [(2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; traceInit tr012
--   Trace {_traceEnv = True, _traceInitState = 0, _traceTrans = StrictSeq {fromStrict = fromList [SigState 1 "one"]}}
--   </pre>
traceInit :: HasCallStack => Trace s -> Trace s

-- | 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:
--   
--   <pre>
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; lastState tr0
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; lastState tr01
--   1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr012 = mkTrace True 0 [(2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; lastState tr012
--   2
--   </pre>
lastState :: Trace s -> State s

-- | Get the last applied signal in a trace (this is, the newest signal).
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; :set -XScopedTypeVariables
--   
--   &gt;&gt;&gt; import Control.Exception (catch, ErrorCall)
--   
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; print (lastSignal tr0) `catch` (\(_ :: ErrorCall) -&gt; putStrLn "error!")
--   "error!
--   </pre>
--   
--   dnadales: In the example above I don't know why the doctests is
--   swallowing the last <tt>"</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; tr01 = mkTrace True 0 [(1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; lastSignal tr01
--   "one"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; lastSignal tr0123
--   "three"
--   </pre>
lastSignal :: HasCallStack => Trace s -> Signal s

-- | Return the first and last state of the trace.
--   
--   The first state is returned in the first component of the result
--   tuple.
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; tr0 = mkTrace True 0 [] :: Trace DUMMY
--   
--   &gt;&gt;&gt; firstAndLastState tr0
--   (0,0)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; tr0123 = mkTrace True 0 [(3, "three"), (2, "two"), (1, "one")] :: Trace DUMMY
--   
--   &gt;&gt;&gt; firstAndLastState tr0123
--   (0,3)
--   </pre>
firstAndLastState :: Trace s -> (State s, State 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.
--   
--   <pre>
--   &gt;&gt;&gt; :set -XTypeFamilies
--   
--   &gt;&gt;&gt; :set -XTypeApplications
--   
--   &gt;&gt;&gt; import Control.State.Transition (initialRules, transitionRules, judgmentContext)
--   
--   &gt;&gt;&gt; import Data.Functor.Identity
--   
--   &gt;&gt;&gt; :{
--   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) &lt;- judgmentContext
--           pure $! st + inc
--       ]
--   :}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; runIdentity $ closure @ADDER () 0 [3, 2, 1]
--   Trace {_traceEnv = (), _traceInitState = 0, _traceTrans = StrictSeq {fromStrict = fromList [SigState 6 3,SigState 3 2,SigState 1 1]}}
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; runIdentity $ closure @ADDER () 10 [-3, -2, -1]
--   Trace {_traceEnv = (), _traceInitState = 10, _traceTrans = StrictSeq {fromStrict = fromList [SigState 4 (-3),SigState 7 (-2),SigState 9 (-1)]}}
--   </pre>
closure :: forall s m. (STS s, m ~ BaseM s) => Environment s -> State s -> [Signal s] -> m (Trace s)

-- | Extract all the values of a given type.
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; extractValues "hello" :: [Char]
--   "hello"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; extractValues ("hello", " " ,"world") :: [Char]
--   "hello world"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; extractValues "hello" :: [Int]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; extractValues ([('a', 0 :: Int), ('b', 1)] :: [(Char, Int)]) :: [Int]
--   [0,1]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; extractValues (["hello"] :: [[Char]], 1, 'z') :: [[Char]]
--   ["hello","ello","llo","lo","o",""]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; extractValues ("hello", 'z') :: [Char]
--   "zhello"
--   </pre>
extractValues :: forall d a. (Data d, Typeable a) => d -> [a]

-- | Apply STS checking assertions.
applySTSTest :: forall s m rtype. (STS s, RuleTypeRep rtype, m ~ BaseM s) => RuleContext rtype s -> m (Either [[PredicateFailure s]] (State s))
instance GHC.Classes.Eq Control.State.Transition.Trace.TraceOrder
instance (GHC.Classes.Eq (Control.State.Transition.Extended.State s), GHC.Classes.Eq (Control.State.Transition.Extended.Signal s), GHC.Classes.Eq (Control.State.Transition.Extended.Environment s)) => GHC.Classes.Eq (Control.State.Transition.Trace.Trace s)
instance (GHC.Show.Show (Control.State.Transition.Extended.State s), GHC.Show.Show (Control.State.Transition.Extended.Signal s), GHC.Show.Show (Control.State.Transition.Extended.Environment s)) => GHC.Show.Show (Control.State.Transition.Trace.Trace s)
instance (GHC.Classes.Eq (Control.State.Transition.Extended.State a), GHC.Classes.Eq (Control.State.Transition.Extended.Signal a)) => GHC.Classes.Eq (Control.State.Transition.Trace.SourceSignalTarget a)
instance (GHC.Show.Show (Control.State.Transition.Extended.State a), GHC.Show.Show (Control.State.Transition.Extended.Signal a)) => GHC.Show.Show (Control.State.Transition.Trace.SourceSignalTarget a)
instance (NoThunks.Class.NoThunks (Control.State.Transition.Extended.Environment s), NoThunks.Class.NoThunks (Control.State.Transition.Extended.State s), NoThunks.Class.NoThunks (Control.State.Transition.Extended.Signal s)) => NoThunks.Class.NoThunks (Control.State.Transition.Trace.Trace s)
instance GHC.Generics.Generic (Control.State.Transition.Trace.SigState s)
instance GHC.Generics.Generic (Control.State.Transition.Trace.Trace s)
instance (GHC.Classes.Eq (Control.State.Transition.Extended.State s), GHC.Classes.Eq (Control.State.Transition.Extended.Signal s)) => GHC.Classes.Eq (Control.State.Transition.Trace.SigState s)
instance (GHC.Show.Show (Control.State.Transition.Extended.State s), GHC.Show.Show (Control.State.Transition.Extended.Signal s)) => GHC.Show.Show (Control.State.Transition.Trace.SigState s)
instance (NoThunks.Class.NoThunks (Control.State.Transition.Extended.State s), NoThunks.Class.NoThunks (Control.State.Transition.Extended.Signal s)) => NoThunks.Class.NoThunks (Control.State.Transition.Trace.SigState s)


-- | Invalid transition system traces.
--   
--   An invalid trace consists of an valid prefix, and a last signal that
--   <b>might</b> be invalid. The validity of the signal depends on the
--   probability of the trace generators of generating invalid signals.
module Control.State.Transition.Invalid.Trace
data Trace s
Trace :: !Trace s -> !Signal s -> !Either [[PredicateFailure s]] (State s) -> Trace s
[validPrefix] :: Trace s -> !Trace s

-- | Last signal in the trace. This might cause a predicate failure, but it
--   isn't guaranteed to do so, since invalid trace generation is
--   probabilistic.
[signal] :: Trace s -> !Signal s
[errorOrLastState] :: Trace s -> !Either [[PredicateFailure s]] (State s)
instance GHC.Generics.Generic (Control.State.Transition.Invalid.Trace.Trace s)
instance (GHC.Classes.Eq (Control.State.Transition.Extended.Environment s), GHC.Classes.Eq (Control.State.Transition.Extended.State s), GHC.Classes.Eq (Control.State.Transition.Extended.Signal s), GHC.Classes.Eq (Control.State.Transition.Extended.PredicateFailure s)) => GHC.Classes.Eq (Control.State.Transition.Invalid.Trace.Trace s)
instance (GHC.Show.Show (Control.State.Transition.Extended.Environment s), GHC.Show.Show (Control.State.Transition.Extended.State s), GHC.Show.Show (Control.State.Transition.Extended.Signal s), GHC.Show.Show (Control.State.Transition.Extended.PredicateFailure s)) => GHC.Show.Show (Control.State.Transition.Invalid.Trace.Trace s)
instance (NoThunks.Class.NoThunks (Control.State.Transition.Extended.Environment s), NoThunks.Class.NoThunks (Control.State.Transition.Extended.State s), NoThunks.Class.NoThunks (Control.State.Transition.Extended.Signal s), NoThunks.Class.NoThunks (Control.State.Transition.Extended.PredicateFailure s)) => NoThunks.Class.NoThunks (Control.State.Transition.Invalid.Trace.Trace s)

module Control.State.Transition.Trace.Generator.QuickCheck

-- | State transition systems for which traces can be generated, given a
--   trace generation environment.
--   
--   The trace generation environment allows to pass relevant data to the
--   trace generation algorithm.
class STS sts => HasTrace sts traceGenEnv where {
    type family BaseEnv sts :: Type;
    type BaseEnv s = ();
}

-- | 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.
interpretSTS :: forall a. HasTrace sts traceGenEnv => BaseEnv sts -> BaseM sts a -> a

-- | 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.
interpretSTS :: (HasTrace sts traceGenEnv, BaseM sts ~ Identity) => forall a. BaseEnv sts -> BaseM sts a -> a
envGen :: HasTrace sts traceGenEnv => traceGenEnv -> Gen (Environment sts)
sigGen :: HasTrace sts traceGenEnv => traceGenEnv -> Environment sts -> State sts -> Gen (Signal sts)
shrinkSignal :: HasTrace sts traceGenEnv => Signal sts -> [Signal sts]

-- | Generate a random trace starting in the given environment and initial
--   state.
traceFrom :: forall sts traceGenEnv. HasTrace sts traceGenEnv => BaseEnv sts -> Word64 -> traceGenEnv -> Environment sts -> State sts -> Gen (Trace sts)

-- | Generate a random trace given a generator for initial state.
--   
--   Takes an optional generator for initial state, or defaults to
--   <tt>applySTS</tt> if no initial state is required by the STS.
traceFromInitState :: forall sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts)) => BaseEnv sts -> Word64 -> traceGenEnv -> Maybe (IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts))) -> Gen (Trace sts)

-- | Generate a random trace.
trace :: forall sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts)) => BaseEnv sts -> Word64 -> traceGenEnv -> Gen (Trace sts)

-- | Shrink a trace by shrinking the list of signals and reconstructing
--   traces from these shrunk lists of signals.
--   
--   When shrinking a trace that is failing some property (often stated in
--   terms of a signal in the trace) then the most recent signal is likely
--   crucial to the failure of the property and must be preserved in the
--   shrunk traces.
shrinkTrace :: forall sts traceGenEnv. HasTrace sts traceGenEnv => BaseEnv sts -> Trace sts -> [Trace sts]

-- | Check a property on the <tt>sts</tt> traces.
forAllTrace :: forall sts traceGenEnv prop. (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts)) => BaseEnv sts -> Word64 -> traceGenEnv -> (Trace sts -> prop) -> Property

-- | Check a property on the <tt>sts</tt> traces.
--   
--   Takes an optional generator for initial state of the STS.
forAllTraceFromInitState :: forall sts traceGenEnv prop. (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts)) => BaseEnv sts -> Word64 -> traceGenEnv -> Maybe (IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts))) -> (Trace sts -> prop) -> Property

-- | Property that asserts that only valid signals are generated.
onlyValidSignalsAreGenerated :: forall sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts)) => BaseEnv sts -> Word64 -> traceGenEnv -> Property

-- | Property that asserts that only valid signals are generated.
--   
--   Takes an optional generator for initial state of the STS.
onlyValidSignalsAreGeneratedFromInitState :: forall sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts)) => BaseEnv sts -> Word64 -> traceGenEnv -> Maybe (IRC sts -> Gen (Either [[PredicateFailure sts]] (State sts))) -> Property

-- | Property that simply classifies the lengths of the generated traces.
traceLengthsAreClassified :: forall sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts)) => BaseEnv sts -> Word64 -> Word64 -> traceGenEnv -> Property

-- | Classify the trace length as either:
--   
--   <ul>
--   <li>being empty</li>
--   <li>being a singleton</li>
--   <li>having the given maximum size</li>
--   <li>belonging to one of the intervals between 2 and the maximum size -
--   1. The number of intervals are determined by the <tt>step</tt>
--   parameter.</li>
--   </ul>
classifyTraceLength :: Word64 -> Word64 -> Trace s -> Property

-- | Classify the value size as either:
--   
--   <ul>
--   <li>being empty</li>
--   <li>being a singleton</li>
--   <li>having the given maximum size</li>
--   <li>belonging to one of the intervals between 2 and the maximum size -
--   1. The number of intervals are determined by the <tt>step</tt>
--   parameter.</li>
--   </ul>
classifySize :: (Ord n, Show n, Integral n) => String -> a -> (a -> n) -> n -> n -> Property

-- | Given a lower bound <tt>low</tt>, an upper bound <tt>high</tt> and a
--   step size <tt>step</tt> (both of which must be positive), divide the
--   interval <tt>[0, ub]</tt> into sub-intervals of <tt>step</tt> size.
--   
--   If any of these values is negative the empty list will be returned.
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 0 0 0 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 0 10 2 :: [(Int, Int)]
--   [(0,2),(2,4),(4,6),(6,8),(8,10)]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 1 10 2 :: [(Int, Int)]
--   [(1,3),(3,5),(5,7),(7,9),(9,10)]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 3 10 3 :: [(Int, Int)]
--   [(3,6),(6,9),(9,10)]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 5 2 3 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals (-1) 10 3 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 1 (-10) 3 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 1 1000 (-100) :: [(Int, Int)]
--   []
--   </pre>
mkIntervals :: Integral n => n -> n -> n -> [(n, n)]


-- | Manual generators.
--   
--   This module provides functions to convert hedgehog <a>Gen</a>s to and
--   from a <a>Manual</a> generators, and functions to manipulate these
--   manual generators.
module Hedgehog.Extra.Manual
newtype Manual a
Manual :: (Size -> Seed -> a) -> Manual a
unManual :: Manual a -> Size -> Seed -> a
toManual :: Gen a -> Manual (TreeT (MaybeT Identity) a)
fromManual :: Manual (TreeT (MaybeT Identity) a) -> Gen a
dontShrink :: Gen a -> Manual (Maybe a)
sized :: (Size -> Manual a) -> Manual a

-- | A version of <a>replicateM</a> specific to <a>Manual</a>.
replicate :: forall a. Int -> Manual a -> Manual [a]
interleave :: [TreeT (MaybeT Identity) a] -> TreeT (MaybeT Identity) [a]
wrapTreeT :: Maybe (NodeT (MaybeT Identity) a) -> TreeT (MaybeT Identity) a
unwrapTreeT :: TreeT (MaybeT Identity) a -> Maybe (NodeT (MaybeT Identity) a)
instance GHC.Base.Functor Hedgehog.Extra.Manual.Manual
instance GHC.Base.Applicative Hedgehog.Extra.Manual.Manual
instance GHC.Base.Monad Hedgehog.Extra.Manual.Manual


-- | 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
module Control.State.Transition.Generator
class STS s => HasTrace s
type SignalGenerator s = Environment s -> State s -> Gen (Signal s)
type family BaseEnv s :: Type

-- | 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.
interpretSTS :: forall a. HasTrace s => BaseEnv s -> BaseM s a -> a

-- | Generate an initial environment that is based on the given trace
--   length.
envGen :: HasTrace s => Word64 -> Gen (Environment s)

-- | Generate a (valid) signal given an environment and a pre-state.
sigGen :: HasTrace s => SignalGenerator s
traceSigGen :: forall s. HasTrace s => BaseEnv s -> TraceLength -> SignalGenerator s -> Gen (Trace s)

-- | Return a (valid) trace generator given an initial state, environment,
--   and signal generator.
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)

-- | Generate a trace that contains at least one non-trivial signal. See
--   <a>HasSizeInfo</a>.
nonTrivialTrace :: forall s. (HasTrace s, HasSizeInfo (Signal s)) => BaseEnv s -> Word64 -> Gen (Trace s)
class HasSizeInfo sig
isTrivial :: HasSizeInfo sig => sig -> Bool

-- | Sample the maximum trace size, given the generator size and number of
--   samples.
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
Maximum :: Word64 -> TraceLength
Desired :: Word64 -> TraceLength
data TraceProfile s
TraceProfile :: !Int -> ![(Int, SignalGenerator s)] -> TraceProfile s

-- | Proportion of valid signals to generate.
[proportionOfValidSignals] :: TraceProfile s -> !Int

-- | List of failure conditions to try generate when generating an invalid
--   signal, and the proportion of each failure.
[failures] :: TraceProfile s -> ![(Int, SignalGenerator s)]
proportionOfInvalidSignals :: TraceProfile s -> Int

-- | Generate an invalid trace
invalidTrace :: forall s. HasTrace s => BaseEnv s -> Word64 -> [(Int, SignalGenerator s)] -> Gen (Trace s)

-- | Classify the trace length as either:
--   
--   <ul>
--   <li>being empty</li>
--   <li>being a singleton</li>
--   <li>having the given maximum size</li>
--   <li>belonging to one of the intervals between 2 and the maximum size -
--   1. The number of intervals are determined by the <tt>step</tt>
--   parameter.</li>
--   </ul>
classifyTraceLength :: Trace s -> Word64 -> Word64 -> PropertyT IO ()

-- | Classify the value size as either:
--   
--   <ul>
--   <li>being empty</li>
--   <li>being a singleton</li>
--   <li>having the given maximum size</li>
--   <li>belonging to one of the intervals between 2 and the maximum size -
--   1. The number of intervals are determined by the <tt>step</tt>
--   parameter.</li>
--   </ul>
classifySize :: (Ord n, Show n, Integral n) => String -> a -> (a -> n) -> n -> n -> PropertyT IO ()

-- | Given a lower bound <tt>low</tt>, an upper bound <tt>high</tt> and a
--   step size <tt>step</tt> (both of which must be positive), divide the
--   interval <tt>[0, ub]</tt> into sub-intervals of <tt>step</tt> size.
--   
--   If any of these values is negative the empty list will be returned.
--   
--   Examples:
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 0 0 0 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 0 10 2 :: [(Int, Int)]
--   [(0,2),(2,4),(4,6),(6,8),(8,10)]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 1 10 2 :: [(Int, Int)]
--   [(1,3),(3,5),(5,7),(7,9),(9,10)]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 3 10 3 :: [(Int, Int)]
--   [(3,6),(6,9),(9,10)]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 5 2 3 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals (-1) 10 3 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 1 (-10) 3 :: [(Int, Int)]
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; mkIntervals 1 1000 (-100) :: [(Int, Int)]
--   []
--   </pre>
mkIntervals :: Integral n => n -> n -> n -> [(n, n)]

-- | Given a function that computes an integral value from a trace, return
--   that value as a ratio of the trace length.
ratio :: Integral a => (Trace s -> a) -> Trace s -> Double

-- | Property that simply classifies the lengths of the generated traces.
traceLengthsAreClassified :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s)) => BaseEnv s -> Word64 -> Word64 -> Property

-- | Check that the signal generator of <tt>s</tt> only generate valid
--   signals.
onlyValidSignalsAreGenerated :: forall s. (HasTrace s, Show (Environment s), Show (State s), Show (Signal s), HasCallStack) => BaseEnv s -> Word64 -> Property

-- | Check that the signal generator of <tt>s</tt> 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
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 ()
instance Control.State.Transition.Generator.HasSizeInfo [a]
