Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
PropEr: a QuickCheck-inspired property-based testing tool for Erlang
Erlang Other
branch: fsm

This branch is 4 commits ahead, 207 commits behind master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
doc
ebin
examples
include
src
test
.gitignore
COPYING
Makefile
README
clean_doc.sh
clean_temp.sh
rebar
rebar.config

README

--------------------------------------------------------------------------------
Contact information and license
--------------------------------------------------------------------------------

PropEr (PROPerty-based testing tool for ERlang) is a QuickCheck-inspired
open-source property-based testing tool for Erlang, developed by Manolis
Papadakis <manopapad@gmail.com>, Eirini Arvaniti <eirinibob@gmail.com> and
Kostis Sagonas <kostis@cs.ntua.gr>. The base PropEr system was written mainly by
Manolis Papadakis, and the stateful code testing subsystem by Eirini Arvaniti.

You can reach the developers in the following ways:
* by email: at proper@softlab.ntua.gr
* on the web: at github.com/manopapad/proper (project page on github)
We welcome user contributions and feedback (comments, suggestions, feature
requests, bug reports, patches etc.).

Copyright 2010-2011 by Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas.

This program is distributed under the GPL, version 3 or later. Please see the
COPYING file for details.


--------------------------------------------------------------------------------
Quickstart guide
--------------------------------------------------------------------------------

* Compile PropEr: run 'make' (or 'make all', if you also want to build the
  documentation).
* Add PropEr's base directory to your Erlang code path by choosing one of the
  following ways:
  1. ERL_LIBS environment variable - Add the following line to your shell
     startup file (~/.bashrc in the case of the Bash shell):
       export ERL_LIBS=/full/path/to/proper
  2. Erlang resource file - Add the following line to your ~/.erlang file:
       code:load_abs("/full/path/to/proper").
* Add the following include line to all source files containing properties you
  wish to test:
     -include_lib("proper/include/proper.hrl").
  By including this header, all the macros, types and functions described in
  this file are automatically imported, so you can use them without a module
  identifier. You can disable this behaviour by compiling your module with
  -DPROPER_NO_IMPORTS. Also, all functions of arity 0 whose name starts with
  "prop_" are automatically exported from the module. If you wish to disable the
  automatic exporting of properties, compile your module with -DPROPER_NO_TRANS.
* Compile your source files.
* For each property, run:
     proper:quickcheck(your_module:some_property()).
       or
     proper:quickcheck(your_module:some_property(), <option/options>).


--------------------------------------------------------------------------------
Common Problems
--------------------------------------------------------------------------------

Using PropEr in conjunction with EUnit:
    Both systems define a ?LET macro, which can cause a clash. Simply include
    PropEr's header file before EUnit's header file. That way, any instance of
    ?LET will count as a PropEr ?LET.
Using PropEr under Erlang/OTP R13B03 or older:
    PropEr makes heavy use of recursive types, which are unsupported on versions
    of the Erlang/OTP distribution prior to R13B04. To compile PropEr under such
    a system, add {d,NO_TYPES} to erl_opts inside rebar.config. This enables the
    spec+type-stripping parse transform included in PropEr, which fixes the
    problem by stripping all type information from PropEr's source files while
    compiling.


--------------------------------------------------------------------------------
Introduction
--------------------------------------------------------------------------------

Traditional testing methodologies essentially involve software testers writing a
series of test inputs for their programs, along with their corresponding
expected outputs, then running the program with these inputs and observing
whether it behaves as expected. This method of testing, while simple and easy to
automate, suffers from a few problems, such as:
* Writing test cases by hand is tedious and time consuming.
* It is hard to know whether the test suite covers all aspects of the software
  under test.

Property-based testing is a novel approach to software testing, where the tester
needs only specify the generic structure of valid inputs for the program under
test, plus certain properties (regarding the program's behaviour and the input-
output relation) which are expected to hold for every valid input. A property-
based testing tool, when supplied with this information, should randomly
produce progressively more complex valid inputs, then apply those inputs to the
program while monitoring its execution, to ensure that it behaves according to
its specification, as outlined in the supplied properties.

Here are a few examples of simple properties a user may wish to test, expressed
in natural language:
* The program should accept any character string and convert all lowercase
  letters inside the string to uppercase.
* The program should accept any list of integers. If the input list is at least
  4 elements long, the program should return the 4th largest integer in the
  list, else it should throw an exception.

PropEr is such a property-based testing tool, designed to test programs written
in the Erlang programming language. Its focus is on testing the behaviour of
pure functions. The input domain of functions is specified through the use of
a type system, modeled closely after the type system of the language itself
(see the following sections for details). Properties are written using Erlang
expressions, with the help of a few predefined macros. Work is currently under
way to provide tighter integration with Erlang's built-in type system.


--------------------------------------------------------------------------------
How to write properties (test case generators)
--------------------------------------------------------------------------------

The simplest properties that PropEr can test consist of a single boolean
expression (or a statement block that returns a boolean), which is expected to
evaluate to 'true'. Thus, the test 'true' always succeeds, while the test
'false' always fails. More complex (and useful) properties can be written by
wrapping such a boolean expression with one or more of the following wrappers:

?FORALL(<Xs>, <Xs_type>, <Prop>)
    The <Xs> field can either be a single variable, a tuple of variables or a
    list of variables. The <Xs_type> field must then be a single type, a tuple
    of types of the same length as the tuple of variables or a list of types of
    the same length as the list of variables, respectively. Tuples and lists can
    be combined in any way, as long as <Xs> and <Xs_type> are compatible. Both
    PropEr-provided types (as listed in the 'Basic types' and 'How to construct
    types' sections) and types declared in Erlang's built-in typesystem (we
    refer to such types in this README as 'native types') may be used in the
    <Xs_type> field. The use of native types in ?FORALLs is subject to some
    limitations, as described in the 'Native types support' section. All the
    variables inside <Xs> can (and should) be present as free variables inside
    the wrapped property <Prop>. When a ?FORALL wrapper is encountered, a random
    instance of <Xs_type> is produced and each variable in <Xs> is replaced
    inside <Prop> by its corresponding instance.
conjunction([{Tag1,Prop1},...,{TagN,PropN}])
    This property is true only if all of the sub-properties Prop1,...,PropN are
    true. The tags Tag1,...,TagN must be distinct atoms. These are used when
    reporting the failure of a property (each failing sub-property is reported
    using its tag) and inside counterexamples (see the 'Counterexamples' section
    for details).
?IMPLIES(<Precondition>, <Prop>)
    This wrapper only makes sense when in the scope of at least one ?FORALL. The
    <Precondition> field must be a boolean expression or a statement block that
    returns a boolean. If the precondition evaluates to 'false' for the variable
    instances produced in the enclosing ?FORALL wrappers, the test case is
    rejected (it doesn't count as a failing test case), and PropEr starts over
    with a new random test case. Also, in verbose mode, an 'x' is printed on
    screen.
collect(<Category>, <Prop>)
    The <Category> field can be an expression or statement block that evaluates
    to any term - the test case produced will be categorized under this term.
    All produced categories are printed at the end of testing (in case no test
    fails) along with the percentage of test cases belonging to each category.
    Multiple 'collect' wrappers are allowed in a single property, in which case
    the percentages for each 'collect' wrapper are printed separately.
collect(<Stats_printer>, <Category>, <Prop>)
    Same as collect/2, but takes an extra first argument, which should be a fun
    with the following signature:
    (SortedSample :: [term()]) -> 'ok'
    This fun will be called at the end of testing (in case no test fails) with
    a sorted list of collected terms. It is expected to print some statistics
    over the collected terms. with_title/1 is a predefined function that accepts
    an atom or string and returns a stats printing function which is equivalent
    to the default one, but prints the given title above the statistics.
aggregate(<Categories>, <Prop>)
    Same as collect/2, but accepts a list of categories under which to classify
    the produced test case.
aggregate(<Stats_printer>, <Categories>, <Prop>)
    Same as collect/3, but accepts a list of categories under which to classify
    the produced test case.
classify(<Counts>, <Category/Categories>, <Prop>)
    Same as collect/2, but accepts both a single category and a list of
    categories. Also, if the boolean flag <Counts> is 'false', the produced test
    case is not counted.
measure(<Title>, <Number> | <List_of_numbers>, <Prop>)
    The number (or numbers) provided are collected and some numeric statistics
    over the collected sample are printed at the end of testing (in case no test
    fails), prepended with <Title>, which should be an atom or string.
?WHENFAIL(<Action>, <Prop>)
    The <Action> field should contain an expression or statement block that
    produces some side-effect (e.g. prints something to the screen). In case
    this test fails, <Action> will be executed. Note that the output of such
    actions is not affected by the verbosity setting of the main application.
?TRAPEXIT(<Prop>)
    If the code inside <Prop> spawns and links to a process that dies
    abnormally, PropEr will catch the exit signal and treat it as a test
    failure, instead of crashing. ?TRAPEXIT cannot contain any more wrappers.
?TIMEOUT(<Time_limit>, <Prop>)
    Signifies that <Prop> should be considered failing if it takes more than
    <Time_limit> milliseconds to return. The purpose of this wrapper is to test
    code that may hang if something goes wrong. ?TIMEOUT cannot contain any more
    wrappers.

The following predefined properties may be used in place of a simple boolean
expression as the innermost property:

equals(<A>, <B>)
    Returns true if <A> =:= <B>, else returns false and prints "<A> =/= <B>" on
    screen.

Additionally, a property may be wrapped with one or more of the following
outer-level wrappers, which control the behaviour of the testing subsystem. If
the same wrapper appears more than once in a property, the innermost takes
precedence.

numtests(<Positive_number>, <Prop>)
    Specifies the number of tests to run. Default is 100.
fails(<Prop>)
    Specifies that we expect the property to fail for some input. The property
    will be considered failing if it passes all the tests.
on_output(<Output_function>, <Prop>)
    Specifies an output function to be used by PropEr for all output printing.
    This wrapper is equivalent to the 'on_output' option (see the 'Options'
    section for details).

Note that failure of a property may also be signified by throwing an exception,
error or exit.

For some actual usage examples, see the code in the examples directory. The
testing modules in the tests directory may also be of interest.


--------------------------------------------------------------------------------
Program behaviour
--------------------------------------------------------------------------------

When running in verbose mode (this is the default), each sucessful test prints
a '.' on screen. If a test fails, a '!' is printed, along with the failing
test case (the instances of the types in every ?FORALL) and the cause of the
failure, if it was not simply the falsification of the property. Then, unless
the test was expected to fail, PropEr attempts to produce a minimal test case
that fails the property in the same way. This process is called
'shrinking'. During shrinking, a '.' is printed for each successful
simplification of the failing test case. When PropEr reaches its shrinking limit
or realizes that the instance cannot be shrunk further while still failing the
test, it prints the minimal failing test case and failure reason and exits.

The return value of PropEr can be one of the following:

* 'true': The property held for all valid produced inputs.
* 'false': The property failed for some input.
* {'error', <Type_of_error>}: An error occured - see the 'Errors' section for a
  description of possible errors.

You can also run PropEr in pure mode by using proper:pure_check/1,2 instead of
proper:quickcheck/1,2. Under this mode, PropEr will perform no I/O and will not
access the caller's process dictionary in any way. Please note that PropEr will
not actually run as a pure function under this mode.

To test all properties exported from a module (a property is a 0-arity function
whose name begins with "prop_"), you can run:
   proper:module(<Module>).
     or
   proper:module(<Module>, <option/options>).
This returns a list of all failing properties, represented by mfas. Testing
progress is also printed on screen (unless 'quiet' mode is active). The
provided options are passed on to each property, except for 'long_result', which
controls the return value format of proper:module itself (see the
'Counterexamples' section).


--------------------------------------------------------------------------------
Counterexamples
--------------------------------------------------------------------------------

A counterexample for a property is represented as a list of terms; each such
term corresponds to the type in a ?FORALL. The instances are provided in the
same order as the ?FORALL wrappers in the property, i.e. the instance at the
head of the list corresponds to the outermost ?FORALL etc. Instances generated
inside a failing sub-property of a conjunction are marked with the
sub-property's tag.

The last (simplest) counterexample produced by PropEr during a (failing) run can
be retrieved after testing has finished, by running proper:counterexample().
When testing a whole module, run proper:counterexamples() to get a
counterexample for each failing property, as a list of {mfa(),counterexample()}
tuples. To enable this functionality, some information has to remain in the
process dictionary even after PropEr has returned. To completely clean up the
process dictionary of PropEr-produced entries, run proper:clean_garbage().

Counterexamples can also be retrieved by running PropEr in long-result mode,
where counterexamples are returned as part of the return value. Specifically,
when testing a single property under long-result mode (activated by supplying
the option 'long_result', or by calling proper:counterexample/1,2 instead of
proper:quickcheck/1,2), PropEr will return a counterexample in case of failure
(instead of simply returning 'false'). When testing a whole module under
long-result mode (activated by supplying the option 'long_result' to
proper:module/2), PropEr will return a list of {mfa(),counterexample()} tuples,
one for each failing property.

You can re-check a specific counterexample <CExm> against the property <Prop>
that it previously falsified by running:
   proper:check(<Prop>, <CExm>)
     or
   proper:check(<Prop>, <CExm>, <option/options>)
This will return one of the following (both in short- and long-result mode):
  * 'true': The property now holds for this test case.
  * 'false': The test case still fails (although not necessarily for the same
    reason as before).
  * {'error', <Type_of_error>}: An error occured - see the 'Errors' section for
    a description of possible errors.
Proper will not attempt to shrink the input in case it fails the property.
Unless silent mode is active, PropEr will also print a message on screen,
describing the result of the re-checking. Note that PropEr can do very little
to verify that <CExm> actually corresponds to <Prop>.


--------------------------------------------------------------------------------
Options
--------------------------------------------------------------------------------

Options can be provided as an extra argument to testing functions exported from
the main proper module (such as proper:quickcheck). A single option can be
written stand-alone, or multiple options can be provided in a list. When two
settings conflict, the one that comes first in the list takes precedence.
Settings given inside external wrappers to a property (see the 'How to write
properties' section) override any conflicting settings provided as options.

The available options are:

'quiet'
    Enables quiet mode - no output is printed on screen while PropEr is running.
'verbose'
    Enables verbose mode - this is the default mode of operation.
{'to_file', <IO_device>}
    Redirects all of PropEr's output to <IO_device>, which should be an IO
    device associated with a file opened for writing.
{'on_output', <output_function>}
    PropEr will use the supplied function for all output printing. This function
    should accept two arguments in the style of io:format/2.
    CAUTION: The above output control options are incompatible with each other.
'long_result'
    Enables long-result mode (see the 'Counterexamples' section for details).
{'numtests', <Positive_number>} or simply <Positive_number>
    This is equivalent to the 'numtests' property wrapper. Any 'numtests'
    wrappers in the actual property will overwrite this setting.
{'start_size', <Size>}
    Specifies the initial value of the 'size' parameter (default is 1), see the
    'How to construct types' section for details.
{'max_size', <Size>}
    Specifies the maximum value of the 'size' parameter (default is 42), see the
    'How to construct types' section for details.
{'max_shrinks', <Non_negative_number>}
    Specifies the maximum number of times a failing test case should be shrunk
    before returning. Note that the shrinking may stop before so many shrinks
    are achieved if the shrinking subsystem deduces that it cannot shrink the
    failing test case further. Default is 500.
'noshrink'
    Instructs PropEr to not attempt to shrink any failing test cases.
{'constraint_tries', <Positive_number>}
    Specifies the maximum number of tries before the generator subsystem gives
    up on producing an instance that satisfies a ?SUCHTHAT constraint. Default
    is 50.
'fails'
    This is equivalent to the 'fails' property wrapper.
{'spec_timeout', 'infinity' | <Non_negative_number>}
    When testing a spec, PropEr will consider an input to be failing if the
    function under test takes more that the specified amount of milliseconds to
    return for that input.
'any_to_integer'
    All generated instances of the type 'any()' will be integers. This is
    provided as a means to speed up the testing of specs, where 'any()' is a
    commonly used type (see the 'Spec testing' section for details).


--------------------------------------------------------------------------------
Basic types
--------------------------------------------------------------------------------

The following basic types are provided:

* integer() : all integers,
    also written as largeint() for compatibility with QuickCheck,
    the shrinking subsystem will attempt to shrink instances of this type to
    values as close as possible to 0
* integer(Low,High) : integers between 'Low' and 'High', bounds included,
    also written as choose(Low,High) and range(Low,High),
    Low and High must be Erlang expressions that evaluate to integers, with
    Low =< High,
    instances shrink towards the bound with the smallest absolute value
* non_neg_integer() : all non-negative integers,
    instances shrink towards 0
* pos_integer() : all positive integers,
    instances shrink towards 1
* neg_integer() : all negative integers,
    instances shrink towards -1
* float() : all floating point numbers,
    also written as real() for compatibility with QuickCheck,
    instances shrink towards 0.0
* float(Low,High) : all floats between 'Low' and 'High', bounds included,
    Low and High must be Erlang expressions that evaluate to floats, with
    Low =< High,
    instances shrink towards the bound with the smallest absolute value
* number() : all numbers (integers and floats),
    instances shrink towards zero (0 or 0.0)
* byte() : all integers between 0 and 255,
    instances shrink towards 0
* char() : all integers between 0 and 16#10ffff,
    instances shrink towards the NUL character, \000
* binary() : all binaries,
    instances shrink towards the empty binary, <<>>
* bitstring() : all bitstrings,
    instances shrink towards the empty bitstring, <<>>
* atom() : all atoms, except those starting with '$'
    you should not use any atoms starting with a '$', as these may clash
    with atoms used internally by PropEr,
    instances shrink towards the empty atom, ''
* boolean() : the atoms 'true' or 'false',
    also written as bool() for compatibility with QuickCheck,
    instances shrink towards 'false'
* list(ElemType) : all lists containing elements of type ElemType,
    instances shrink towards the empty list, []
* list() : equivalent to list(any())
* string() : all lists of characters,
    instances shrink towards the empty string, ""
* function(ArgTypes, RetType) : all pure functions that map instances of
    ArgTypes (ArgTypes must be provided in a list) to instances of RetType,
    the syntax function(Arity, RetType) is also acceptable
* any() : all Erlang terms (that PropEr can produce)
    also written as term()
    currently, functions are never produced as instances of any()
    CAUTION: Instances of 'any()' are expensive to produce, shrink and instance-
    check, both in terms of processing time and consumed memory. Only use this
    type if you are certain that you need it.

All the above have analogues in the built-in types of the Erlang language.

In addition, the following types are provided:

* int() : small integers (bound by the current value of the 'size' parameter -
    see the next section for details),
    instances shrink towards 0
* nat() : small non-negative integers (bound by the current value of the 'size'
    parameter - see the next section for details),
    instances shrink towards 0
* non_neg_float() : all non-negative floats,
    instances shrink towards 0.0
* binary(Len) : all binaries with a byte size of 'Len',
    Len must be an Erlang expression that evaluates to a non-negative integer,
    instances shrink towards binaries of zeroes
* bitstring(Len) : all bitstrings with a bit size of 'Len',
    Len must be an Erlang expression that evaluates to a non-negative integer,
    instances shrink towards bitstrings of zeroes
* tuple(ListOfTypes) : all tuples whose i-th element is an instance of the type
    at index i of ListOfTypes,
    also written simply as a tuple of types
* loose_tuple(ElemType) : all tuples whose elements are all of type ElemType
    instances shrink towards {}
* tuple() : equivalent to loose_tuple(any())
* vector(Len,ElemType) : all lists of length Len containing elements of type
    ElemType,
    Len must be an Erlang expression that evaluates to a non-negative integer
* fixed_list(ListOfTypes) : all lists whose i-th element is an instance of the
    type at index i of ListOfTypes,
    also written simply as ListOfTypes
* orderedlist(ElemType) : all sorted lists containing elements of type ElemType,
    instances shrink towards the empty list, []
* exactly(X) : singleton type consisting only of X,
    X must be an evaluated term,
    also written as return(X) or simply as X
* union(ListOfTypes) : the union of all types in ListOfTypes,
    ListOfTypes can't be empty,
    the random instance generator is equally likely to choose any one of the
    types in ListOfTypes,
    the shrinking subsystem will always try to shrink an instance of a type
    union to an instance of the first type in ListOfTypes, thus you should write
    the simplest case first,
    also written as oneof(ListOfTypes) and elements(ListOfTypes)
* weighted_union(ListOfTypes) : a specialization of union(ListOfTypes), where
    each type in ListOfTypes is assigned a frequency like so: {frequency,type},
    frequencies must be Erlang expressions that evaluate to positive integers,
    types with larger frequencies are more likely to be chosen by the random
    instance generator,
    the shrinking subsystem will ignore the frequencies and try to shrink
    towards the first type in ListOfTypes,
    also written as wunion(ListOfTypes) and frequency(ListOfTypes)
* default(Default, Type) : adds a default value, Default, to Type,
    the default serves as a primary shrinking target for instances, while it is
    also chosen by the random instance generation subsystem half the time
* weighted_default(Default, Type) : a specialization of default(Default, Type),
    where Default and Type are assigned weights like so: {frequency,type},
    to be considered by the random instance generator,
    the shrinking subsystem will ignore the weights and try to shrink
    using the default value
* function[0-4](RetType) : equivalent to function([0-4], RetType), provided for
    compatibility with QuickCheck
* timeout() : equivalent to union([non_neg_integer() | 'infinity']),
    instances shrink towards 0
* arity() : equivalent to range(0,255),
    instances shrink towards 0

As you can see from the above descriptions, types can be combined in tuples or
lists to produce other types, while exact values (such as exact numbers, atoms
or strings) can be combined with types inside such structures, like in this
example of the type of a tagged tuple: {'result', integer()}.


--------------------------------------------------------------------------------
How to construct types
--------------------------------------------------------------------------------

The following macros and functions can be applied to types in order to produce
new ones:

?LET(<Xs>, <Xs_type>, <In>)
    To produce an instance of this type, all appearances of the variables in
    <Xs> inside <In> are replaced by their corresponding values in a randomly
    generated instance of <Xs_type>. It's OK for the <In> part to evaluate to a
    type - in that case, an instance of the inner type is generated recursively.
?SUCHTHAT(<X>, <Type>, <Condition>)
    This produces a specialization of <Type>, which only includes those members
    of <Type> that satisfy the constraint <Condition> - that is, those members
    for which the function 'fun(<X>) -> <Condition> end' returns 'true'. If the
    constraint is very strict - that is, only a small percentage of instances
    of <Type> pass the test - it will take a lot of tries for the instance
    generation subsystem to randomly produce a valid instance of the specialized
    type. This will result in slower testing - testing may even be stopped
    short, in case the 'constraint_tries' limit is reached (see the 'Options'
    section). If this is the case, it would be more appropriate to generate
    valid instances of the specialized type using the ?LET macro. Also make sure
    that even small instances can satisfy the constraint, since PropEr will only
    try small instances at the start of testing. If this is not possible, you
    can instruct PropEr to start at a larger size ('start_size' option - see the
    'Options' section for details).
?SUCHTHATMAYBE(<X>, <Type>, <Condition>)
    Equivalent to the ?SUCHTHAT macro, but the constraint <Condition> is
    considered non-strict: if the 'constraint_tries' limit is reached, the
    generator will just return an instance of <Type> instead of failing,
    even if that instance doesn't satisfy the constraint.
non_empty(<List_or_binary_type>)
    This is a predefined constraint that can be applied to random-length list
    and binary types (e.g. list(), string(), binary()) to ensure that the
    produced values are not empty.
noshrink(<Type>)
    Creates a new type which is equivalent to <Type>, but whose instances are
    never shrunk by the shrinking subsystem.
?SHRINK(<Generator>, <List_of_alternative_generators>)
    This creates a type whose instances are generated by evaluating the
    statement block <Generator> (this may evaluate to a type, which is generated
    recursively). If an instance of such a type is to be shrunk, the generators
    in <List_of_alternative_generators> are first run to produce hopefully
    simpler instances of the type. Thus, the generators in the second argument
    should be simpler than the default. The simplest ones should be at the front
    of the list, since those are the generators preferred by the shrinking
    subsystem. Like the main <Generator>, the alternatives may also evaluate to
    a type, which is generated recursively.
?LETSHRINK(<List_of_variables>, <List_of_types>, <Generator>)
    This is created by combining a ?LET and a ?SHRINK macro. Instances are
    generated by applying a randomly generated list of values inside <Generator>
    (just like a ?LET, with the added constraint that the variables and types
    must be provided in a list - alternatively, <List_of_types> may be a list or
    vector type). When shrinking instances of such a type, the sub-instances
    that were combined to produce it are first tried in place of the failing
    instance.
?LAZY(<Generator>)
    This construct returns a type whose only purpose is to delay the evaluation
    of <Generator> (<Generator> can return a type, which will be generated
    recursively). Using this, you can simulate the lazy generation of instances:
      stream() -> ?LAZY(frequency([ {1,[]}, {3,[0|stream()]} ])).
    The above type produces lists of zeroes with an average length of 3. Note
    that, had we not enclosed the generator with a ?LAZY macro, the evaluation
    would continue indefinitely, due to the eager evaluation of the Erlang
    language.
with_parameter(<Parameter_name>, <Value>, <Type>)
    <Parameter_name> will be associated with <Value> while generating <Type>.
    This can be useful when generating commands for stateful systems (as
    described in 'Testing stateful systems' section).
with_parameters(<Proplist_of_parameters>, <Type>)
    Similar to with_parameter/3, but accepts a list of
    {<Parameter_name>,<Value>} pairs.
parameter(<Parameter_name>, <Default>)
    Returns the <Value> associated with <Parameter_name>, or <Default> in case
    <Parameter_name> is not associated with any value.
parameter(<Parameter_name>)
    Equivalent to parameter(<Parameter_name>, undefined).

The following functions and macros are related to the 'size' parameter, which
controls the maximum size of produced instances. The actual size of a produced
instance is chosen randomly, but can never exceed the value of the 'size'
parameter at the moment of generation. A more accurate definition is the
following: the maximum instance of 'size' S can never be smaller than the
maximum instance of 'size' S-1. The actual size of an instance is measured
differently for each type: the actual size of a list is its length, while the
actual size of a tree may be the number of its internal nodes. Some types, e.g.
unions, have no notion of size, thus their generation is not influenced by the
value of 'size'. The 'size' parameter starts at 0 and grows automatically during
testing.

?SIZED(<S>, <Generator>)
    Creates a new type, whose instances are produced by replacing all
    appearances of the <S> parameter inside the statement block <Generator> with
    the value of the 'size' parameter. It's OK for the <Generator> to return a
    type - in that case, an instance of the inner type is generated recursively.
resize(<New_size>, <Type>)
    Overrides the 'size' parameter used when generating instances of <Type> with
    <New_size>. Has no effect on size-less types, such as unions. Also, this
    will not affect the generation of any internal types contained in <Type>,
    such as the elements of a list - those will still be generated using the
    test-wide value of 'size'. One use of this function is to modify types to
    grow faster or slower, like so:
      ?SIZED(Size, resize(Size * 2, list(integer()))
    The above specifies a list type that grows twice as fast as normal lists.


--------------------------------------------------------------------------------
Native types support
--------------------------------------------------------------------------------

PropEr can parse types expressed in Erlang's native type format and convert them
to its own type format. Such expressions can be used instead of regular type
constructors in the second argument of ?FORALLs. No extra notation is required -
PropEr will detect which calls correspond to native types by applying a parse
transform during compilation. This parse transform is automatically applied to
any module that includes the proper.hrl header file. You can disable this
feature by compiling your modules with -DPROPER_NO_TRANS. Note that this will
currently also disable the automatic exporting of properties.

The use of native types in properties is subject to the following usage rules:

* Native types cannot be used outside of ?FORALLs.
* Inside ?FORALLs, native types can be combined with other native types, and
  even with PropEr types, inside tuples and lists (the constructs '[...]',
  '{...}' and '++' are all allowed).
* All other constructs of Erlang's built-in type system (e.g. '|' for union, '_'
  as an alias of 'any()', '<<_:_>>' binary type syntax or 'fun((...) -> ...)'
  function type syntax) are not allowed in ?FORALLs, since they are rejected by
  the Erlang parser.
* Anything other than a tuple constructor, list constructor, '++' application,
  local or remote call will automatically be considered a PropEr type
  constructor and not be processed further by the parse transform.
* Parametric native types are fully supported - of course, they can only appear
  instantiated in a ?FORALL. The arguments of parametric native types are always
  interpreted as native types.
* Parametric PropEr types, on the other hand, can take any kind of argument. You
  can even mix native and PropEr types in the arguments of a PropEr type. For
  example, assuming that the following declarations are present:
     my_proper_type() -> ?LET(...).
     -type my_native_type() :: ... .
  Then the following expressions are all legal:
     vector(2, my_native_type())
     function(0, my_native_type())
     union([my_proper_type(), my_native_type()])
* Some type constructors can take native types as arguments (but only inside
  ?FORALLs):
  - ?SUCHTHAT, ?SUCHTHATMAYBE, non_empty, noshrink: these work with native
    types too
  - ?LAZY, ?SHRINK, resize, ?SIZED: these don't work with native types
  - ?LET, ?LETSHRINK: only the top-level base type can be a native type
* Native type declarations in the ?FORALLs of a module can reference any custom
  type declared in a -type or -opaque attribute of the same module, as long as
  no module identifier is used.
* Typed records cannot be referenced inside ?FORALLs using the '#rec_name{}'
  syntax. To use a typed record in a ?FORALL, enclose the record in a custom
  type like so:
     -type rec_name() :: #rec_name{}.
  and use the custom type instead.
* ?FORALLs may contain references to self-recursive or mutually recursive native
  types, so long as each type in the hierarchy has a clear base case. Currently,
  PropEr requires that the toplevel of any recursive type declaration is either
  a (maybe empty) list or a union containing at least one choice that doesn't
  reference the type (it may, however, reference any of the types that are
  mutually recursive with it). This means, for example, that some valid
  recursive type declarations, such as this one:
     ?FORALL(..., a(), ...) where:
     -type a() :: {'a','none' | a()}.
  are not accepted by PropEr. However, such types can be rewritten in a way that
  allows PropEr to parse them:
     ?FORALL(..., a(), ...) where:
     -type a() :: {'a','none'} | {'a',a()}.
  This also means that recursive record declarations are not allowed:
    ?FORALL(..., rec(), ...) where:
     -type rec() :: #rec{}.
     -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).
  A little rewritting can usually remedy this problem as well:
     ?FORALL(..., rec(), ...) where:
     -type rec() :: #rec{b :: 'nil'} | #rec{b :: rec()}.
     -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).
* Remote types may be referenced in a ?FORALL, as long as they are exported from
  the remote module. Currently, PropEr requires that any remote modules whose
  types are directly referenced from within properties are present in the code
  path at compile time, either compiled with debug_info enabled or in source
  form. If PropEr cannot find a remote module at all, finds only a compiled
  object file with no debug information or fails to compile the source file, all
  calls to that module will automatically be considered calls to PropEr type
  constructors.
* For native types to be translated correctly, both the module that contains the
  ?FORALL declaration as well as any module that contains the declaration of a
  type referenced (directly or indirectly) from inside a ?FORALL must be present
  in the code path at runtime, either compiled with debug_info enabled or in
  source form.
* Local types with the same name as an auto-imported BIF are not accepted by
  PropEr, unless the BIF in question has been declared in a no_auto_import
  option.
* When an expression can be interpreted both as a PropEr type and as a native
  type, the former takes precedence. This means that a function foo() will
  shadow a type foo() if they are both present in the module. The same rule
  applies to remote functions and types as well.
* The above may cause some confusion when list syntax is used:
  - The expression '[integer()]' can be interpreted both ways, so the PropEr way
    applies. Therefore, instances of this type will always be lists of length 1,
    not arbitrary integer lists, as would be expected when interpreting the
    expression as a native type.
  - Assuming that a custom type foo/1 has been declared, the expression
    foo([integer()]) can only be interpreted as a native type declaration,
    which means that the generic type of integer lists will be passed to foo/1.
* Currently, PropEr does not detect the following mistakes:
  - inline record-field specializations that reference non-existent fields
  - type parameters that are not present in the RHS of a '-type' declaration
  - using '_' as a type variable in the LHS of a '-type' declaration
  - using the same variable in more than one position in the LHS of a '-type'
    declaration


--------------------------------------------------------------------------------
Spec testing
--------------------------------------------------------------------------------

You can test the accuracy of an exported function's spec by running:
     proper:check_spec(mfa()).
       or
     proper:check_spec(mfa(), <option/options>).
Under this mode of operation, PropEr will call the provided function with
increasingly complex valid inputs (according to its spec) and test that no
unexpected value is returned. If an input is found that violates the spec, it
will be saved as a counterexample and PropEr will attempt to shrink it.

You can test all exported functions of a module against their spec by running:
     proper:check_specs(<Module>).
       or
     proper:check_specs(<Module>, <option/options/).
The behaviour of proper:check_specs is similar to that of proper:module.

The use of check_spec is subject to the following usage rules:

* Currently, PropEr can't test functions whose range contains a type that
  exhibits a certain kind of self-reference: it is (directly or indirectly)
  self-recursive and at least one recursion path contains only unions and type
  references. E.g. these types are acceptable:
     -type a(T) :: T | {'bar',a(T)}.
     -type b() :: 42 | [c()].
     -type c() :: {'baz',b()}.
  while these are not:
     -type a() :: 'foo' | b().
     -type b() :: c() | [integer()].
     -type c() :: 'bar' | a().
     -type d(T) :: T | d({'baz',T}).
* Throwing any exception or raising an 'error:badarg' is considered normal
  behaviour. Currently, users cannot fine-tune this setting.
* Only the first clause of the function's spec is considered.
* The only spec constraints we accept are 'is_subtype' constraints whose first
  argument is a simple, non-'_' variable. It is not checked whether or not these
  variables actually appear in the spec. The second argument of an 'is_subtype'
  constraint cannot contain any non-'_' variables. Multiple constraints for the
  same variable are not supported.

PropEr comes with an extra header file, "proper/include/proper_param_adts.hrl",
which contains definitions of parametric wrappers for some STDLIB ADTs, namely
array/1, dict/2, gb_set/1, gb_tree/2, queue/1, set/1, orddict/2 and ordset/1. By
including this header file, you can use the above parametric types to better
document your code and facilitate spec testing (PropEr automatically recognizes
these types and produces valid instances). Please note that Dialyzer currenty
treats these the same way as the non-parametric versions.


--------------------------------------------------------------------------------
Symbolic datatypes
--------------------------------------------------------------------------------

When writing properties that involve abstract data types, such as dicts or sets,
it is usually best to avoid dealing with the ADTs' internal representations
directly. Working, instead, with a symbolic representation of an ADT's
construction process (series of API calls) has several benefits:

* Failing testcases are easier to read and understand. Compare:
     {call,sets,from_list,[[1,2,3]]}
  with:
     {set,3,16,16,8,80,48,
	  {[],[],[],[],[],[],[],[],[],[],[],[],[],[],[],[]},
	  {{[],[3],[],[],[],[],[2],[],[],[],[],[1],[],[],[],[]}}}
* Failing testcases are easier to shrink.
* It is especially useful when testing the datatype itself: Certain
  implementation errors may depend on some particular selection and ordering of
  API calls, thus it is important to cover the entire ADT construction API.

PropEr supports the symbolic representation of datatypes, using the following
syntax:

* {call,<Module>,<Function>,<Arguments>}: This represents a call to the API
  function <Module>:<Function> with arguments <Arguments>. Each of the arguments
  may be a symbolic call itself or contain other symbolic calls in lists or
  tuples of arbitrary depth.
* {'$call',<Module>,<Function>,<Arguments>}: Identical to the above, but gets
  evaluated automatically before being applied to a property.
* {var,<Atom>}: This contruct serves as a placeholder for values that are not
  known at type construction time. It will be replaced by the actual value of
  the variable during evaluation.

The following functions, automatically imported from the proper_symb module
(unless PROPER_NO_IMPORTS is defined), can be used when working with symbolic
instances:

* eval(<Symbolic_instance>): Intended for use inside the property-testing code,
  this function evaluates a symbolic instance.
* eval(<VarValues>, <Symbolic_instance>): Same as above, but accepts a proplist
  of variable names and values, to be replaced anywhere inside the symbolic
  instance before proceeding with the evaluation.
* defined(<Symbolic_instance>): Returns true if the symbolic instance can be
  successfully evaluated (its evaluation doesn't raise an error or exception).
* well_defined(<Symbolic_instance>): An attribute which can be applied to
  symbolic generators that may produce invalid sequences of operations when
  called. The resulting type is guaranteed to only produce well-defined symbolic
  instances.
* pretty_print/1,2: Similar in calling convention to eval/1,2, but returns a
  string representation of the call sequence instead of evaluating it.


--------------------------------------------------------------------------------
Auto-ADT
--------------------------------------------------------------------------------

To simplify the symbolic testing of ADTs, PropEr comes with the Auto-ADT
subsystem: An opaque native type, if exported from its module, is assumed to be
an abstract data type, causing PropEr to ignore its internal representation and
instead construct symbolic instances of the type. The API functions used in
these symbolic instances are extracted from the ADT's definition module, which
is expected to contain one or more '-spec'ed exported functions that can be used
to construct instances of the ADT. Specifically, PropEr will use all functions
that return at least one instance of the ADT. As with recursive native types,
the base case is automatically detected (in the case of ADTs, calls to functions
like new/0 and from_list/1 would be considered the base case). The produced
symbolic calls will be '$call' tuples, which are automatically evaluated, thus
no call to eval/1 is required inside the property. Produced instances are
guaranteed to evaluate successfully. Parametric ADTs are fully supported, as
long as they appear instantiated inside ?FORALLs. ADTs hard-coded in the Erlang
type system (array, dict, digraph, gb_set, gb_tree, queue, and set) are
automatically detected and handled as such. PropEr also accepts parametric
versions of the above ADTs in ?FORALLs (array/1, dict/2, gb_set/1, gb_tree/2,
queue/1, set/1, also orddict/2 and ordset/1).

The use of Auto-ADT is currently subject to the following limitations:

* In the ADT's '-opaque' declaration, as in all types' declarations, only
  type variables should be used as parameters in the LHS. None of these
  variables can be the special '_' variable and no variable should appear more
  than once in the parameters.
* ADTs inside specs can only have simple variables as parameters. These
  variables cannot be bound by any is_subtype constraint. Also, the special '_'
  variable is not allowed in ADT parameters. If this would result in singleton
  variables, as in the specs of functions like new/0, use variable names that
  begin with an underscore.
* Specs that introduce an implicit binding among the parameters of an ADT are
  rejected, e.g.:
     -spec foo(mydict(T,S),mydict(S,T)) -> mydict(T,S).
  This includes using the same type variable twice in the parameters of an ADT.
* While parsing the return type of specs in search of ADT references, PropEr
  only recurses into tuples, unions and lists - all other constructs are
  ignored. This prohibits, among others, indirect references to the ADT through
  other custom types and records.
* When encountering a union in the return type, PropEr will pick the first
  choice that can return an ADT. This choice must be distinguishable from the
  others either by having a unique term structure or by having a unique tag (if
  it's a tagged tuple).
* When parsing multi-clause specs, only the first clause is considered.
* The only spec constraints we accept are 'is_subtype' constraints whose first
  argument is a simple, non-'_' variable. It is not checked whether or not these
  variables actually appear in the spec. The second argument of an 'is_subtype'
  constraint cannot contain any non-'_' variables. Multiple constraints for the
  same variable are not supported.
* Unexported opaques and opaques with no suitable specs to serve as API calls
  are silently discarded. Those will be treated like ordinary types.
* Unexported or unspecced functions are silently rejected.
* Functions with unsuitable return values are silently rejected.
* Specs that make bad use of variables are silently rejected.

For an example on how to write Auto-ADT-compatible parametric specs, see the
tests/stack module, which contains a simple implementation of a stack, or the
proper/proper_dict module, which wraps the STDLIB dict ADT.


--------------------------------------------------------------------------------
Testing stateful code
--------------------------------------------------------------------------------

PropEr provides the module proper_statem to facilitate testing of stateful
systems whose side-effects are specified via an abstract state machine. Given a
callback module implementing the state machine, PropEr can generate random
symbolic command sequences subject to the constraints (preconditions) of the
specification.

The symbolic representation of a command has the following syntax:

* {set,{var,<Integer>},{call,<Module>,<Function>,<Arguments>}}: Binds a
symbolic variable to the result of a symbolic call.

During command generation we use symbolic variables to bind the results of
symbolic calls. Therefore, the state of the abstract state machine might (and
usually does) contain symbolic variables and/or symbolic calls, which are
necessary to operate on symbolic variables. Thus, we refer to it as symbolic
state.

As a next step, symbolic command sequences are evaluated in order to check that
command execution behaves according to the state machine specifications
(postconditions). During this phase, symbolic calls are evaluated and symbolic
variables are replaced by their corresponding real values. Now we refer to the
state as dynamic state.


More specifically, the following functions must be exported from the callback
module implementing the abstract state machine:

* initial_state(): Specifies the (symbolic) initial state of the state machine.
This state will be evaluated at command execution time to produce the actual
initial state. The function is not only called at command generation time, but
also in order to initialize the state every time the command sequence is run
(i.e. during normal execution, while shrinking and when checking a
counterexample). For this reason, it should be deterministic.
* command(<Symbolic_state>): Generates a symbolic call to be included in the
command sequence, given the current <Symbolic_state> of the state machine.
However, before the call is actually included, a precondition is checked.
* precondition(<Symbolic_state>, <Symbolic_call>): Specifies the precondition
that should hold so that <Symbolic_call> can be included in the command
sequence, given the current <Symbolic_state> of the state machine. In case
precondition doesn't hold, a new call is chosen using the command/1
generator. If preconditions are very strict, it will take a lot of tries for
PropEr to randomly choose a valid command. Testing will be stopped in case the
'constraint_tries' limit is reached (see the 'Options'section).
* postcondition(<Dynamic_state>, <Symbolic_call>, <Result>): Specifies the
postcondition that should hold about the <Result> of the evaluation of
<Symbolic_call>, given the current <Dynamic_state> of the state machine.
This function is called during command execution time, this is why the state
is dynamic.
* next_state(<Symbolic_state> | <Dynamic_state>, <Result>, <Symbolic_call>):
Specifies the next state of the state machine, given the current state, the
<Symbolic_call> chosen and its <Result>. This function is called both at
command generation and command execution time in order to determine the next
state, therefore the <Result> can be either symbolic (i.e. containing symbolic
variables and/or symbolic calls) or dynamic (i.e. containing real values).


The following functions, automatically imported from the proper_statem module
(unless PROPER_NO_IMPORTS is defined), can be used when working with stateful
code:

* commands(<Module>): A special PropEr type which generates random command
sequences, as specified by the absract state machine in <Module>. The initial
state is specified by <Module>:initial_state().
* commands(<Module>, <Symbolic_state>): Similar to commands/1, but generated
command sequences always start at <Symbolic_state>. In this case, the first
command is always {init,<Symbolic_state>} and is used to correctly initialize
the state every time the command sequence is run (i.e. during normal execution,
while shrinking and when checking a counterexample).
In this case, <Module>:initial_state/0 is never called.
* more_commands(<N>, <Generator>): Increases the maximum length of command
sequences generated within Generator by a factor <N>.

* run_commands(<Module>, <Cmds>): This function runs a given command sequence
<Cmds> according to the state machine specified in <Module>. The result is a
tuple of the form: {<History>,<Dynamic_state>,<Statem_result>}.
  - <History> contains the execution history of all commands that were executed
  without raising an exception. It contains tuples of the form {<Dynamic_state>,
  <Result>}, specifying the <Dynamic_state> prior to command execution and the
  actual <Result> of the command.
  - <Dynamic_state> contains the state of the abstract state machine at the
  moment when execution stopped.
  -  <Statem_result> specifies the overall result of command execution. It
  can be one of the following:
    -- 'ok': all commands were successfully run and all postconditions were
    true
    -- 'initialization_error': there was an error while evaluating the initial
    state
    -- {'postcondition', <Boolean> | <Exception>}: a postcondition was false
    or raised an exception
    -- {'precondition', <Boolean> | <Exception>}: a precondition was false or
    raised an exception
    -- <Exception>: an exception was raised while running a command
* run_commands(<Module>, <Cmds>, <Environment>): Similar to run_commands/2,
but also accepts a list of {<Key>,<Value>} pairs. Keys may be used in symbolic
variables (i.e. {var,<Key>}) whithin the command sequence <Cmds>. These
symbolic variables will be replaced by their corresponding <Value> during
command execution.

* command_names(<Cmds>): Extracts the names of the commands in a given command
sequence in the form of MFAs. It is useful in combination with functions such
as aggregate/2,3  in order to collect statistics about command execution.
* state_after(<Module>, <Cmds>): Returns the symbolic state after running
the command sequence <Cmds> according to the state machine found in <Module>.
The commands are not actually executed.
* zip(<listA>, <listB>): Behaves like lists:zip/2, but listA, listB do no not
necessarily have equal length. Zipping stops when the shortest list stops. This
is useful for zipping a command sequence with its (failing) execution history.

Examples of sample properties to check can be found at examples/pdict_statem
and examples/ets_statem. These modules contain an abstract state machine
specification for testing operations on the process dictionary and ets tables
respectively.


--------------------------------------------------------------------------------
Parallel testing
--------------------------------------------------------------------------------

After ensuring that a system's behaviour can be described via an abstract state
machine when commands are executed sequentially, it is possible to move to
parallel testing. The same state machine can be used to generate command
sequences that will be executed concurrently to test for race conditions.
A parallel testcase consists of a command list, which is run sequentially to put
the system in a random state, and a list of concurrent tasks. These tasks are
also command lists, but they are executed concurrently in separate processes.
After running a parallel testcase, PropEr uses the state machine specification
to check if the results observed could have been produced by a possible
serialization of the concurrent tasks. If no such serialization is possible,
then an atomicity violation is detected.

The following functions, automatically imported from the proper_statem module
(unless PROPER_NO_IMPORTS is defined), can be used for parallel testing:

* parallel_commands(<Module>): A special PropEr type which generates parallel
testcases from the absract state machine specified in <Module>. The initial
state is specified by <Module>:initial_state().
* parallel_commands(<Module>, <Symbolic_state): Similar to parallel_commands/1,
but generated command sequences always start at <Symbolic_state>.
* run_parallel_commands(<Module>, <TestCase>): This function runs a parallel
<TestCase> according to the specifications in <Module>. The result is a tuple
of the form: {<Sequential_history>,<Parallel_history>,<Statem_result>}.
  - <Sequential_history> contains the execution history of the sequential
  prefix
  - <Parallel_history> contains the execution history of each of the
  concurrent tasks.
  - <Statem_result> specifies the outcome of the attemp to serialize command
  execution, based on the results observed. It can be one of the following:
    -- 'ok'
    -- 'no_possible_interleaving'
* run_parallel_commands(<Module>, <TestCase>, <Environment>): Similar to
run_parallel_commands/2, but also accepts an <Environment> used for symbolic
variable evaluation, exactly as described in run_commands/3.

Note: in its current implementation PropEr might not be able to generate
suitable concurrent tasks for each test. In this case, an 'f' is printed on
screen to inform the user.

An example of a sample property for parallel testing can be found at
examples/ets_statem, where we test concurrent operations on a public ets table.


--------------------------------------------------------------------------------
PropEr fsm
--------------------------------------------------------------------------------

PropEr provides another useful module for testing stateful systems, in
particular those that can be better described as a finite state machine.
For PropEr, an FSM is a triple {S0, D, S}, where S0 is the initial state,
D a set of possible updates (transitions) and S a finite set of states.

* State representation
Following the convention used in gen_fsm behaviour, a state is fully described
by a StateName and some StateData. StateName is used to denote a state of
the state machine and StateData is used to denote the internal state of the
Erlang process which implements the state machine. States are fully represented
as tuples {StateName, StateData}.

StateName is usually an atom (i.e. the name of the state), but can also be a
tuple. In the latter case, the first element of the tuple must be an atom
specifying the name of the state, whereas the rest of the elements can be
arbitrary terms specifying state attributes.
For example, when implementing the fsm of an elevator which can reach N
different floors, the StateName for each floor could be {floor,K}, 1 <= K <= N.
StateData can be an arbitrary term, but is usually a record.

* Transition represantation
Transitions are represented as tuples {TargetState, {call,M,F,ArgsGen}}. This
means that performing the specified symbolic call at the current state of the
fsm will lead to TargetState. The atom <history> can be used as TargetState to
denote that a transition does not change the current state of the fsm.


The following functions must be exported from the callback module implementing
the finite state machine:

* initial_state(): Specifies the initial state_name of the fsm. As in
proper_statem:initial_state/0, its result should be deterministic.
* initial_state_data() : Specifies the (symbolic) initial state_data. As in
proper_statem:initial_state/0, its result should be deterministic.
* StateName(<StateData>): There should be one instance of this function for
each possible state name StateName. In case StateName is a tuple the function
takes a different form, described just below. The function returns a list
of possible transitions from the current state {StateName,StateData}.
At command generation time, the instance of this function with the same name
as the current state name StateName is called to return the list of possible
transitions. Then, PropEr will randomly choose a transition and, according to
that, generate the next symbolic call to be included in the command sequence.
However, before the call is actually included, a precondition that might
impose constraints on <StateData> is checked.
Note also that PropEr detects transitions that would raise an exception of class
<error> at generation time (not earlier) and does not choose them. This feature
can be used to include conditional transitions that depend on the <StateData>.
* StateName(<Attr1>, ..., <AttrN>, <StateData>): There should be one instance
of this function for each possible state name {StateName,<Attr1>,...,<AttrN>}.
The function has similar beaviour to StateName/1, described above.
* weight(<FromState>, <TargetState>, <Call>): This is an optional callback.
When it is not defined (or not exported), transitions are chosen with equal
probability. When it is defined, it assigns an integer weight to transitions
from <FromState> to <TargetState> triggered by symbolic call <Call>. In this
case, each transition is chosen with probability proportional to the weight
assigned.
* precondition(<FromState>, <TargetState>, <StateData>, <Call>):
Similar to proper_statem:precondition/2. Specifies the precondition that should
hold about <StateData> so that <Call> can be included in the command sequence.
In case precondition doesn't hold, a new transition is chosen using the
appropriate StateName/1 generator (more specifically FromState/1).
It is possible for more than one transitions to be triggered by the same
symbolic call and lead to different target states. In this case, at most one of
the target states may have a true precondition. Otherwise, PropEr will not be
able to detect which transition was chosen and an exception will be raised.
Preconditions are also very important for the shrinking procedure. When
attempting to shrink fsm command sequences, we try to eliminate commands that
do not contribute to failure, ensuring that all preconditions still hold.
* postcondition(<FromState>, <TargetState>, <StateData>, <Call>, <Result>):
Similar to proper_statem:postcondition/3. Specifies the postcondition that
should hold about the <Result> of the evaluation of <Call>.
* next_state_data(<FromState>, <TargetState>, <StateData>, <Result>, <Call>):
Similar to proper_statem:next_state/3. Specifies how the transition from
<FromState> to <TargetState> triggered by <Call> affects the <StateData>.
<Result> refers to the result of <Call> and can be either symbolic or dynamic.


The following functions can be used when working with finite state machines.
Due to name conflicts with functions automatically imported from proper_statem,
a fully qualified call is needed, i.e. proper_fsm:Fun(Args).

* proper_fsm:commands(<Module>): A special PropEr type which generates random
command sequences, as specified by the finite state machine in <Module>. The
initial state is {<Module>:initial_state(), <Module>:initial_state_data()}.
* proper_fsm:commands(<Module>, <Symbolic_state>): Similar to commands/1, but
generated command sequences always start at <Symbolic_state>, which should be
a tuple {<StateName>, <StateData>}. In this case, the first command is always
{init,<Symbolic_state>} and is used to correctly initialize the state every time
the command sequence is run (i.e. during normal execution, while shrinking and
when checking a counterexample).

* proper_fsm:run_commands(<Module>, <Cmds>): This function runs a given command
sequence <Cmds> according to the finite state machine specified in <Module>. The
result is a tuple of the form: {<History>,<Dynamic_state>,<Fsm_result>}.
See proper_statem:run_commands/2 for more details. <Fsm_result> has the same
form and meaning as <Statem_result>.
* proper_fsm:run_commands(<Module>, <Cmds>, <Environment>): Similar to
run_commands/2, but also accepts an <Environment> used for symbolic variable
evaluation, exactly as described in proper_statem:run_commands/3.

* proper_fsm:state_names(<History>): Extracts the names of the states from a
given command execution history. It is useful in combination with functions such
as aggregate/2,3 in order to collect statistics about state transitions during
command execution.

Examples of sample properties to check can be found at examples/elevator_fsm,
containing a finite state machine specification for an elevator.


--------------------------------------------------------------------------------
Errors
--------------------------------------------------------------------------------

The following errors may be encountered during testing. The term provided for
each error is the error type returned by proper:quickcheck in case such an error
occurs. Normaly, a message is also printed on screen describing the error.

* 'arity_limit': The random instance generation subsystem has failed to produce
  a function of the desired arity. Please recompile PropEr with a suitable value
  for ?MAX_ARITY (defined in proper_internal.hrl). This error should only be
  encountered during normal operation.
* 'cant_generate': The random instance generation subsystem has failed to
  produce an instance that satisfies some ?SUCHTHAT constraint. You should
  either increase the 'constraint_tries' limit, loosen the failing constraint,
  or make it non-strict. This error should only be encountered during normal
  operation.
* 'cant_satisfy': All the tests were rejected because no produced test case
  would pass all ?IMPLIES checks. You should loosen the failing ?IMPLIES
  constraint(s). This error should only be encountered during normal operation.
* 'non_boolean_result': The property code returned a non-boolean result. Please
  fix your property.
* 'rejected': Only encountered during re-checking, the counterexample does not
  match the property, since the counterexample doesn't pass an ?IMPLIES check.
* 'too_many_instances': Only encountered during re-checking, the counterexample
  does not match the property, since the counterexample contains more instances
  than there are ?FORALLs in the property.
* 'type_mismatch': The variables' and types' structures inside a ?FORALL don't
  match. Please check your properties.
* {'typeserver', <SubError>}: The typeserver encountered an error. The
  <SubError> field contains specific information regarding the error.
* {'unexpected', <Result>}: A test returned an unexpected result during normal
  operation. If you ever get this error, it means that you have found a bug in
  PropEr - please send an error report to the maintainers and remember to
  include both the failing test case and the output of the program, if possible.
* {'unrecognized_option', <Option>}: <Option> is not an option that PropEr
  understands.


--------------------------------------------------------------------------------
Demo functions
--------------------------------------------------------------------------------

You can use the following functions to try out the random instance generation,
shrinking and type translation subsystems:

* proper_gen:pick(<Type>):
    equivalent to proper_gen:pick(<Type>, 10)
* proper_gen:pick(<Type>, <Size>):
    Generates a random instance of <Type>, of size <Size>.
* proper_gen:sample(<Type>):
    equivalent to proper_gen:sample(<Type>, 10, 20)
* proper_gen:sample(<Type>, <Start_Size>, <End_Size>):
    Generates and prints one random instance of <Type> for each size from
    <Start_Size> up to <End_Size>.
* proper_gen:sampleshrink(<Type>):
    equivalent to proper_gen:sampleshrink(<Type>, 10)
* proper_gen:sampleshrink(<Type>, <Size>):
    Generates a random instance of <Type>, of size <Size>, then shrinks it as
    far as it goes. The value produced on each step of the shrinking process is
    printed on the screen.
* proper_typeserver:demo_translate_type(<Module>, <Type_Expr>):
    Translates the native type expression <Type_Expr> (which should be provided
    inside a string) into a PropEr type, which can then be passed to any one
    of the above demo functions. PropEr acts as if it found this type expression
    inside the code for <Module>.
* proper_typeserver:demo_is_instance(<Term>, <Module>, <Type_Expr>):
    Checks if <Term> is a valid instance of native type <Type_Expr> (which
    should be provided inside a string). PropEr acts as if it found this type
    expression inside the code for <Module>.

CAUTION: These functions should never be used inside properties. They are meant
for demonstration purposes only.


--------------------------------------------------------------------------------
Incompatibilities with QuviQ's QuickCheck
--------------------------------------------------------------------------------

We have generaly tried to keep PropEr's notation and output as compatible as
possible with QuviQ's QuickCheck, to allow for the reuse of existing testing
code written for QuickCheck. However, incompatibilities are to be expected,
since the two programs probably bear little resemblance under the hood. Here
we provide a nonexhaustive list of known incompatibilities:

* ?SUCHTHATMAYBE behaves differently in PropEr.
* proper_gen:pick differs from eqc_gen:pick in return value format.
* PropEr handles 'size' differently from QuickCheck.
* proper:module/2 accepts options in the second argument instead of the first.
Something went wrong with that request. Please try again.