small-steps-1.1.2.0: Small step semantics
Safe HaskellNone
LanguageHaskell2010

Test.Control.State.Transition.Trace.Generator.QuickCheck

Synopsis

Documentation

class STS sts ⇒ HasTrace sts traceGenEnv where Source #

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.

Minimal complete definition

envGen, sigGen, shrinkSignal

Associated Types

type BaseEnv sts Source #

type BaseEnv sts = ()

Methods

interpretSTS ∷ HasCallStack ⇒ BaseEnv sts → BaseM sts 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.

default interpretSTS ∷ BaseM sts ~ Identity ⇒ ∀ a. BaseEnv sts → BaseM sts a → a Source #

envGen ∷ traceGenEnv → Gen (Environment sts) Source #

sigGen ∷ traceGenEnv → Environment sts → State sts → Gen (Signal sts) Source #

shrinkSignal ∷ Signal sts → [Signal sts] Source #

traceFrom Source #

Arguments

∷ HasTrace sts traceGenEnv 
⇒ BaseEnv sts 
→ Word64

Maximum trace length.

→ traceGenEnv 
→ Environment sts 
→ State sts 
→ Gen (Trace sts) 

Generate a random trace starting in the given environment and initial state.

traceFromInitState Source #

Arguments

∷ (HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) 
⇒ BaseEnv sts 
→ Word64

Maximum trace length.

→ traceGenEnv 
→ Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))

Optional generator of STS initial state

→ Gen (Trace sts) 

Generate a random trace given a generator for initial state.

Takes an optional generator for initial state, or defaults to applySTS if no initial state is required by the STS.

trace Source #

Arguments

∷ (HasTrace sts traceGenEnv, Show (Environment sts)) 
⇒ BaseEnv sts 
→ Word64

Maximum trace length.

→ traceGenEnv 
→ Gen (Trace sts) 

Generate a random trace.

shrinkTrace ∷ HasTrace sts traceGenEnv ⇒ BaseEnv sts → Trace sts → [Trace sts] Source #

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.

Trace generator properties

forAllTrace Source #

Arguments

∷ (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts)) 
⇒ BaseEnv sts 
→ Word64

Maximum trace length.

→ traceGenEnv 
→ (Trace sts → prop) 
→ Property 

Check a property on the sts traces.

forAllTraceFromInitState Source #

Arguments

∷ (HasTrace sts traceGenEnv, Testable prop, Show (Environment sts)) 
⇒ BaseEnv sts 
→ Word64

Maximum trace length.

→ traceGenEnv 
→ Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))

Optional generator of STS initial state

→ (Trace sts → prop) 
→ Property 

Check a property on the sts traces.

Takes an optional generator for initial state of the STS.

onlyValidSignalsAreGenerated Source #

Arguments

∷ (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts)) 
⇒ BaseEnv sts 
→ Word64

Maximum trace length.

→ traceGenEnv 
→ Property 

Property that asserts that only valid signals are generated.

onlyValidSignalsAreGeneratedFromInitState Source #

Arguments

∷ (HasTrace sts traceGenEnv, Show (Environment sts), Show (Signal sts)) 
⇒ BaseEnv sts 
→ Word64

Maximum trace length.

→ traceGenEnv 
→ Maybe (IRC sts → Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))

Optional generator of STS initial state

→ Property 

Property that asserts that only valid signals are generated.

Takes an optional generator for initial state of the STS.

Trace classification

traceLengthsAreClassified Source #

Arguments

∷ (HasTrace sts traceGenEnv, Show (Environment sts)) 
⇒ BaseEnv sts 
→ Word64

Maximum trace length that the signal generator of s can generate.

→ Word64

Lengths of the intervals in which the lengths range should be split.

→ traceGenEnv

Trace generation environment

→ Property 

Property that simply classifies the lengths of the generated traces.

classifyTraceLength Source #

Arguments

∷ Word64

Maximum size of the traces

→ Word64

Steps used to divide the interval

→ Trace s 
→ Property 

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.

classifySize Source #

Arguments

∷ (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

→ Property 

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.

Internal

mkIntervals Source #

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