small-steps-1.1.0.1: Small step semantics
Safe HaskellSafe-Inferred
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 ∷ Type Source #

type BaseEnv s = ()

Methods

interpretSTS ∷ ∀ a. HasCallStackBaseEnv 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 interpretSTSBaseM sts ~ Identity ⇒ ∀ a. BaseEnv sts → BaseM sts a → a Source #

envGenHasCallStack ⇒ traceGenEnv → Gen (Environment sts) Source #

sigGenHasCallStack ⇒ traceGenEnv → Environment sts → State sts → Gen (Signal sts) Source #

shrinkSignalHasCallStackSignal sts → [Signal sts] Source #

traceFrom Source #

Arguments

∷ ∀ sts traceGenEnv. 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

∷ ∀ sts traceGenEnv. (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

∷ ∀ sts traceGenEnv. (HasTrace sts traceGenEnv, Show (Environment sts)) 
BaseEnv sts 
Word64

Maximum trace length.

→ traceGenEnv 
Gen (Trace sts) 

Generate a random trace.

shrinkTrace ∷ ∀ sts traceGenEnv. 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

∷ ∀ sts traceGenEnv prop. (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

∷ ∀ sts traceGenEnv prop. (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

∷ ∀ sts traceGenEnv. (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

∷ ∀ sts traceGenEnv. (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

∷ ∀ sts traceGenEnv. (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)]
[]