### Install PropEr with Homebrew

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

For users on systems with Homebrew, this command provides a simple way to install the PropEr tool directly through the package manager, streamlining the setup process.

```Shell
brew install proper
```

--------------------------------

### Erlang FSM Start Function API

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_finite_state_machines.md

This section describes the API for starting the finite state machine. It defines a `day` type and the `start/1` function, which initializes the `gen_fsm` behavior with a specified starting day and an empty storage record. The `init/1` callback handles the FSM's initial state.

```Erlang
-type day() :: 'cheese_day' | 'lettuce_day' | 'grapes_day'.

-spec start(day()) -> {'ok', pid()} | {'error', {'already_started', pid()}}.
start(Day) ->
    gen_fsm:start({local, creature}, ?MODULE, [Day], []).

init([Day]) ->
    {ok, Day, #storage{}}.
```

--------------------------------

### Erlang Model State Initialization

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Initializes the model's state, defining the starting structure with empty lists for users and rented items. This callback function sets up the foundational state for the system.

```erlang
initial_state() ->
    #state{users  = [],
           rented = []}.
```

--------------------------------

### Run PropEr Quickcheck with EUnit Output Visibility

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

Provides a workaround for EUnit capturing standard output by passing the `{to_file, user}` option to `proper:quickcheck/2`, ensuring PropEr's test results are visible when invoked from EUnit.

```erlang
?assertEqual(true, proper:quickcheck(your_mod:some_prop(), [{to_file, user}])).
```

--------------------------------

### Compile and Test PropEr

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

These commands demonstrate how to compile the PropEr tool, run its unit tests, perform static analysis with Dialyzer, and build the project's documentation. Users can choose specific `make` targets based on their development needs.

```Shell
make
make test
make dialyzer
make all
```

--------------------------------

### PropEr ?SETUP Macro for Property Setup and Teardown

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper.html

This macro allows defining a setup function that runs before the first test and returns a finalize function that runs after the last test. Multiple ?SETUP macros can be used.

```APIDOC
?SETUP(<Setup_fun>, <Prop>)
  <Setup_fun>: A function that will be called before the first test. It must return a finalize function of arity 0, which should return the atom 'ok'.
  <Prop>: The property to be tested.
```

--------------------------------

### Erlang Ping-Pong Master: Start and Initialize

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_process_interaction.md

Initializes the ping-pong master as an Erlang gen_server. The `start_link` function registers the server locally, and `init` sets up its internal state as an empty dictionary to store player scores.

```Erlang
start_link() ->
    gen_server:start_link({local, ?MASTER}, ?MASTER, [], []).

init([]) ->
    {ok, dict:new()}.
```

--------------------------------

### PropEr Counterexample for Server Crash

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

This Erlang snippet shows a counterexample generated by PropEr that led to a server crash. It's a sequence of commands, starting with `create_account`, which exposed a bug in the `handle_call` logic when `ets:lookup_element` was called with a non-existent key, highlighting the importance of robust error handling.

```erlang
[{set,{var,1},{call,movie_server,create_account,[john]}},
```

--------------------------------

### Clone PropEr Git Repository

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

This command clones the PropEr source code repository from GitHub, allowing users to obtain the latest version or a specific tagged release of the tool.

```Shell
git clone git://github.com/proper-testing/proper.git
```

--------------------------------

### Set ERL_LIBS Environment Variable for PropEr

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

Configures the ERL_LIBS environment variable to point to the PropEr installation directory, allowing the Erlang runtime to locate PropEr modules. This should be added to a shell startup file like ~/.bashrc.

```shell
export ERL_LIBS=/full/path/to/proper
```

--------------------------------

### Run PropEr Quickcheck for a Single Property

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

Demonstrates how to execute a quickcheck test for a specific property defined within an Erlang module using PropEr's `proper:quickcheck/1` function.

```erlang
proper:quickcheck(your_module:some_property()).
```

--------------------------------

### Define Preconditions for PropEr State Machine Commands

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

This Erlang code defines `precondition/2` callbacks for a state machine, ensuring that commands like `return_dvd`, `rent_dvd`, and `delete_account` are only executed when the system state (S) meets specific criteria (e.g., user exists, DVD is rented). This helps guide the shrinking process in property-based testing by discarding invalid command sequences.

```erlang
precondition(S, {call,_,return_dvd,[Password,Movie]}) ->
    lists:member({Password,Movie}, S#state.rented);
precondition(S, {call,_,rent_dvd,[Password,_Movie]}) ->
    lists:member(Password, S#state.users);
precondition(S, {call,_,delete_account,[Password]}) ->
    lists:member(Password, S#state.users);
precondition(_, _) ->
    true.
```

--------------------------------

### Property-based test for ping-pong system behavior

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_process_interaction.md

This Erlang code snippet defines a property-based test, 'prop_ping_pong_works', using the `?FORALL` macro to generate and execute sequences of commands against the ping-pong system. It starts and stops the master process and captures the history, state, and result of the command execution for verification.

```erlang
prop_ping_pong_works() ->
    ?FORALL(Cmds, commands(?MODULE),
            ?TRAPEXIT(
                begin
                    ?MASTER:start_link(),
                    {History,State,Result} = run_commands(?MODULE, Cmds),
                    ?MASTER:stop(),
                    ?WHENFAIL(io:format("History: ~w~nState: ~w\nResult: ~w~n",
                                        [History, State, Result]),
```

--------------------------------

### Load PropEr Module in Erlang Resource File

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

Adds a line to the Erlang resource file (~/.erlang) to automatically load the PropEr module upon Erlang shell startup, making PropEr functions available globally.

```erlang
code:load_abs("/full/path/to/proper").
```

--------------------------------

### Examples of Combining PropEr and Native Erlang Types

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_typeserver.html

Demonstrates how PropEr and native Erlang types can be mixed as arguments for type constructors within `?FORALL` expressions, showing legal type declarations and their usage.

```Erlang
my_proper_type() -> ?LET(...).
-type my_native_type() :: ... .

% Legal expressions combining types:
vector(2, my_native_type())
function(0, my_native_type())
union([my_proper_type(), my_native_type()])
```

--------------------------------

### Define a Default PropEr Precondition

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Illustrates the basic `precondition/2` callback function in PropEr, which takes the current state and a symbolic call, returning a boolean. This example shows a permissive precondition that always returns true, allowing any command sequence to be considered valid for testing.

```Erlang
precondition(_, _) -> true.
```

--------------------------------

### Include PropEr Header in Erlang Source Files

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/userguide.md

Instructs Erlang source files containing properties to include PropEr's header file, providing necessary macro definitions and type specifications for property-based testing.

```erlang
-include_lib("proper/include/proper.hrl").
```

--------------------------------

### PropEr Symbolic Set Construction Example

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_symb.html

Compares the readable symbolic representation of a set construction using `call` syntax with a complex, internal representation. The symbolic form `{call,sets,from_list,[[1,2,3]]}` is preferred for its clarity and ease of understanding in failing test cases, contrasting with the verbose internal data structure.

```Erlang
{call,sets,from_list,[[1,2,3]]}
```

--------------------------------

### Execute PropEr Quickcheck Test

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_spells.md

Demonstrates how to run the `prop_spells` property test using the `proper:quickcheck` function. The example shows executing the test for 100,000 iterations and confirms that the property holds for all randomly generated inputs, indicating successful validation.

```Erlang
1> proper:quickcheck(magic:prop_spells(), 100000).
.... 100000 dots ...
OK: Passed 100000 test(s).
true
```

--------------------------------

### Adding Precondition for return_dvd Function

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

This Erlang code snippet illustrates how to add a precondition to a PropEr property. The `precondition` function ensures that the `return_dvd` command is only generated if the specified movie was actually rented by the given password, preventing unrealistic test cases and guiding PropEr towards more relevant scenarios.

```erlang
precondition(S, {call,_,return_dvd,[Password,Movie]}) ->
    lists:member({Password,Movie}, S#state.rented);
```

--------------------------------

### Erlang PropEr: Generic Property for Stateful Server Testing

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

This Erlang property, `prop_server_works_fine`, defines a generic test for stateful servers using PropEr. It encompasses two main phases: generating random symbolic command sequences via `commands(?MODULE)` and executing them with `run_commands(?MODULE, Cmds)`. The property ensures test isolation by including setup (`?SERVER:start_link()`) and cleanup (`?SERVER:stop()`) logic, asserting that the command execution result is `ok`.

```Erlang
prop_server_works_fine() ->
    ?FORALL(Cmds, commands(?MODULE),
            begin
                ?SERVER:start_link(),
                {_,_,Result} = run_commands(?MODULE, Cmds),
                ?SERVER:stop(),
                Result =:= ok
            end).
```

--------------------------------

### PropEr Quickcheck with Precondition and New Counterexample

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

This snippet presents the outcome of running PropEr's quickcheck after adding a precondition to the property. With the `return_dvd` precondition in place, PropEr discovers a different, more complex counterexample involving account creation, movie rentals, and then account deletion, showcasing how preconditions help uncover new types of bugs.

```erl
6> proper:quickcheck(movie_statem:prop_server_works_fine()).
..............!
Failed: After 15 test(s).
[{set,{var,1},{call,movie_server,create_account,[mary]}},
 {set,{var,2},{call,movie_server,ask_for_popcorn,[]}},
 {set,{var,3},{call,movie_server,rent_dvd,[{var,1},despicable_me]}},
 {set,{var,4},{call,movie_server,rent_dvd,[{var,1},the_lion_king]}},
 {set,{var,5},{call,movie_server,rent_dvd,[{var,1},peter_pan]}},
 {set,{var,6},{call,movie_server,rent_dvd,[{var,1},titanic]}},
 {set,{var,7},{call,movie_server,ask_for_popcorn,[]}},
 {set,{var,8},{call,movie_server,delete_account,[{var,1}]}}]

Shrinking ....(4 time(s))
[{set,{var,1},{call,movie_server,create_account,[mary]}},
 {set,{var,5},{call,movie_server,rent_dvd,[{var,1},peter_pan]}},
 {set,{var,8},{call,movie_server,delete_account,[{var,1}]}}]
```

--------------------------------

### Define Initial State for PropEr FSM Model

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_finite_state_machines.md

These Erlang functions, `initial_state` and `initial_state_data`, are callbacks used by PropEr to define the starting point of the finite state machine model. `initial_state()` specifies the initial state name (`cheese_day`), and `initial_state_data()` initializes the state data, in this case, an empty `#storage{}` record, aligning with the system under test's initial conditions.

```erlang
initial_state() -> cheese_day.

initial_state_data() -> #storage{}.
```

--------------------------------

### Define preconditions for valid API call execution

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_process_interaction.md

This Erlang code specifies the 'precondition' function, which ensures that certain API calls are only executed when the system is in a valid state. For example, removing a player or getting a score requires the player to already be a member of the state's player list.

```erlang
precondition(S, {call,_,remove_player,[Name]}) ->
    lists:member(Name, S#state.players);
precondition(S, {call,_,get_score,[Name]}) ->
    lists:member(Name, S#state.players);
precondition(S, {call,_,play_ping_pong,[Name]}) ->
    lists:member(Name, S#state.players);
precondition(S, {call,_,play_tennis,[Name]}) ->
    lists:member(Name, S#state.players);
precondition(_, _) ->
    true.
```

--------------------------------

### PropEr Quickcheck with TRAPEXIT and Counterexample Analysis

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

This snippet shows the output of running the revised PropEr property that incorporates `?TRAPEXIT`. PropEr successfully identifies a counterexample (returning an unrented movie) and provides a shrunk sequence of commands that leads to the server crash, demonstrating improved debugging capabilities.

```erl
4> proper:quickcheck(movie_statem:prop_server_works_fine()).
....................!
Failed: After 21 test(s).
A linked process died with reason
{badarg,[{ets,lookup_element,[491536,inception,2]},
         <...3 more lines of stacktrace...]}.

<...ERROR REPORT produced...>

[{set,{var,1},{call,movie_server,create_account,[john]}},
 {set,{var,2},{call,movie_server,create_account,[mary]}},
 {set,{var,3},{call,movie_server,create_account,[alice]}},
 {set,{var,4},{call,movie_server,ask_for_popcorn,[]}},
 {set,{var,5},{call,movie_server,rent_dvd,[{var,1},despicable_me]}},
 {set,{var,6},{call,movie_server,return_dvd,[{var,3},finding_nemo]}},
 {set,{var,7},{call,movie_server,rent_dvd,[{var,2},despicable_me]}},
 {set,{var,8},{call,movie_server,return_dvd,[{var,1},inception]}},
 {set,{var,9},{call,movie_server,ask_for_popcorn,[]}},
 {set,{var,10},{call,movie_server,create_account,[ben]}}]

Shrinking .....
<...ERROR REPORTS produced...>
(5 time(s))
[{set,{var,1},{call,movie_server,create_account,[john]}},
 {set,{var,8},{call,movie_server,return_dvd,[{var,1},inception]}}]
false
```

--------------------------------

### API: Create New Account

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Describes the API for creating a new user account on the movie server. Users provide a name and receive a password for future interactions.

```APIDOC
create_account(name()) -> password().
Purpose: Creates a new user account.
Parameters:
  name(): The name of the user (e.g., 'Bond', 'James Bond').
Returns:
  password(): A unique password for the new account.
```

```Erlang
-spec create_account(name()) -> password().
create_account(Name) ->
    gen_server:call(?MODULE, {new_account, Name}).
```

--------------------------------

### Executing Targeted PBT with Simulated Annealing

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_with_search_strategies.md

This Erlang snippet shows how to invoke PropEr's `quickcheck` function for targeted property-based testing. It specifies the use of `simulated_annealing` as the search strategy and sets the number of `search_steps` to 1000, guiding the input generation process to find inputs that maximize or minimize a utility value.

```erl
proper:quickcheck(prop_Target(), [{search_strategy, simulated_annealing}, {search_steps, 1000}]).
```

--------------------------------

### Erlang PropEr Simulated Annealing Generator Definition

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_spells.md

This Erlang function `list_of_spells_sa()` defines the structure required by PropEr's simulated annealing strategy for generating inputs. It specifies the initial element generator (`first`) using `list_of_spells()` and the neighborhood function (`next`) using `list_of_spells_next()`. This setup guides how the search strategy explores the input space.

```Erlang
list_of_spells_sa() ->
  #{first => list_of_spells(),
    next => list_of_spells_next()}.
```

--------------------------------

### Erlang Stateful Targeted Property Testing Function

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_fsm.html

This Erlang function, `prop_targeted_testing`, demonstrates how to implement stateful targeted property-based testing. It uses `?FORALL_TARGETED` to generate command sequences, runs them against a finite state machine, and employs a utility value (`UV`) to guide the search towards specific failure modes or interesting states, maximizing the chances of finding difficult-to-reproduce bugs.

```Erlang
prop_targeted_testing() ->
    ?FORALL_TARGETED(Cmds, proper_fsm:commands(?MODULE),
                     begin
                         {History, State, Result} = proper_fsm:run_commands(?MODULE, Cmds),
                         UV = uv(History, State, Result),
                         ?MAXIMIZE(UV),
                         cleanup(),
                         Result =:= ok
                     end).
```

--------------------------------

### Simulate New Day and FSM State Transitions

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_finite_state_machines.md

This Erlang code defines the `new_day` function, which sends an event to the creature FSM to signal the start of a new day with a specified food type. It also includes clauses for `cheese_day`, `lettuce_day`, and `grapes_day` functions, demonstrating how the FSM transitions between states (e.g., from `cheese_day` to `lettuce_day`) based on the food provided for the new day.

```erlang
-spec new_day(food()) -> 'ok'.
new_day(Food) ->
    gen_fsm:send_event(creature, {new_day, Food}).

cheese_day({new_day, lettuce}, S) ->
    {next_state, lettuce_day, S};
cheese_day({new_day, grapes}, S) ->
    {next_state, grapes_day, S}.

lettuce_day({new_day, cheese}, S) ->
    {next_state, cheese_day, S};
lettuce_day({new_day, grapes}, S) ->
    {next_state, grapes_day, S}.

grapes_day({new_day, cheese}, S) ->
    {next_state, cheese_day, S};
grapes_day({new_day, lettuce}, S) ->
    {next_state, lettuce_day, S}.
```

--------------------------------

### Generate List of Example Erlang Spells

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_spells.md

Provides an example Erlang function `spells/0` that returns a predefined list of `spell` records. Each record in the list represents a unique spell with specific attribute modifications (positive or negative) that can be applied to a character.

```Erlang
-spec spells() -> list(spell()).
spells() ->
  [#attr{strength = 5, constitution = -2, dexterity = -3},
   #attr{defense = 4, willpower = -4},
   #attr{intelligence = -3, charisma = 1,
         wisdom = 1,  perception = 1},
   #attr{strength = 1,  constitution = 2,
         defense = 2, willpower = -3},
   #attr{intelligence = 1,  charisma = 1,
         wisdom = 1,  willpower = -3},
   #attr{strength = 1, intelligence = -3,
         charisma = 0, luck = 2},
   #attr{intelligence = 1,  charisma = 1,  wisdom = 1,
         willpower = -4, perception = 1},
   #attr{charisma = 2, perception = 1,  luck = -3},
   #attr{strength = 2,  constitution = -2},
   #attr{constitution = 2,  defense = -2},
   #attr{defense = 2,  dexterity = -2},
   #attr{dexterity = 2,  intelligence = -2},
   #attr{strength = -1, constitution = -1, defense = -1,
         dexterity = -1, intelligence = -1, charisma = -1,
         wisdom = -1, willpower = 10, perception = -1, luck = -1},
   #attr{intelligence = 2,  charisma = -2},
   #attr{charisma = 2,  wisdom = -2},
   #attr{wisdom = 2,  willpower = -2},
   #attr{willpower = 2,  perception = -2},
   #attr{perception = 2,  luck = -2},
   #attr{strength = -2, luck = 2},
   #attr{strength = 5, luck = -8}].
```

--------------------------------

### Test Distribution Analysis with `proper:quickcheck`

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Command line output from `proper:quickcheck` showing the statistical distribution of commands executed during a test run. This analysis reveals that the `return_dvd/2` operation is rarely tested, highlighting an imbalance in test coverage.

```erl
41> proper:quickcheck(movie_statem:prop_server_works_fine(), 3000).
...........3000 dots.............
OK: Passed 3000 test(s).

31.20% {movie_server,ask_for_popcorn,0}
30.84% {movie_server,create_account,1}
18.92% {movie_server,delete_account,1}
17.72% {movie_server,rent_dvd,2}
 1.32% {movie_server,return_dvd,2}
true
```

--------------------------------

### Example of Rejected Erlang Spec for Auto-ADT

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_symb.html

This Erlang `-spec` declaration illustrates a type signature that introduces an implicit binding among ADT parameters, which is explicitly rejected by PropEr's Auto-ADT subsystem. It serves as an example of a limitation where the same type variable cannot be used twice in the parameters of an ADT in a way that implies such a binding.

```Erlang
-spec foo(mydict(T,S),mydict(S,T)) -> mydict(T,S).
```

--------------------------------

### Erlang Targeted Property-Based Testing Example

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_target.html

Illustrates the typical structure for a targeted property using the `?EXISTS`, `?MAXIMIZE`, and `?NOT_EXISTS` macros within a PropEr test specification. This example shows how to define a property that seeks to maximize a utility value (UV) derived from the System Under Test (SUT) while ensuring a condition (UV < Threshold) is met.

```Erlang
prop_target() ->                 % Try to check that
  ?EXISTS(Input, Params,         % some input exists
          begin                  % that fullfills the property.
            UV = SUT:run(Input), % Do so by running SUT with Input
            ?MAXIMIZE(UV),       % and maximize its Utility Value
            UV < Threshold       % up to some Threshold.
          end)).
```

--------------------------------

### atom/0

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_types.html

Represents all Erlang atoms. Atoms starting with '$' are reserved by PropEr and will not be generated. Instances shrink towards the empty atom, `''`.

```APIDOC
atom() -> [proper_types:type()]
```

--------------------------------

### API: Rent DVD

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Describes the API for renting a DVD. The server checks movie availability and user registration, returning a list of currently rented movies or an error.

```APIDOC
rent_dvd(password(), movie()) -> [movie()] | 'not_a_client'.
Purpose: Rents a DVD for a user.
Parameters:
  password(): The user's account password.
  movie(): The movie to rent.
Returns:
  [movie()]: A list of all movies currently rented by the user, if successful.
  'not_a_client': If the provided password is invalid.
```

```Erlang
-spec rent_dvd(password(), movie()) -> [movie()] | 'not_a_client'.
rent_dvd(Password, Movie) ->
    gen_server:call(?MODULE, {rent, Password, Movie}).
```

--------------------------------

### parallel_commands/2 API Reference

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_statem.html

Documents the `parallel_commands/2` function, which generates command sequences starting from a specified initial state. It is similar to `parallel_commands/1` but provides state initialization.

```APIDOC
parallel_commands/2:
  Signature: parallel_commands(Mod :: mod_name(), InitialState :: symbolic_state()) -> proper_types:type()
  Description: Similar to parallel_commands/1, but generated command sequences always start at a given state.
  Parameters:
    Mod: mod_name() - The module defining the state machine.
    InitialState: symbolic_state() - The initial state from which command sequences should start.
  Returns:
    proper_types:type() - The generated command sequence or related type.
```

--------------------------------

### Build PropEr API Documentation Locally

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/api.md

Instructions on how to generate the PropEr API documentation from source files.

```Shell
make doc
```

--------------------------------

### gen_and_print_samples/3 Function Definition

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper.html

This function generates and prints samples for a given raw type, starting from a specified size and ending at another specified size.

```APIDOC
gen_and_print_samples(RawType :: [proper_types:raw_type()],
                      StartSize :: [proper_gen:size()],
                      EndSize :: [proper_gen:size()]) ->
                         ok
```

--------------------------------

### Run EUnit Tests from Erlang Shell

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_introduction_to_Property-Based_Testing.md

Illustrates how to recompile an Erlang module and execute all defined EUnit tests using the `eunit:test/1` function from the Erlang shell. This command provides a quick way to run all unit tests and see their results.

```erl
5> c(my_sort).
{ok,my_sort}
6> eunit:test(my_sort).
  All 4 tests passed.
ok
```

--------------------------------

### Define strategy_fun() Type

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper.html

A function type that, given a number of tests and workers, splits the testing load into a list of tuples indicating start test and number of tests.

```APIDOC
strategy_fun() =
    fun((NumTests :: pos_integer(), NumWorkers :: pos_integer()) ->
            [{non_neg_integer(), non_neg_integer()}])
```

--------------------------------

### API: Ask for Popcorn

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Describes a simple API call to request popcorn from the DVD club, available to anyone without authentication.

```APIDOC
ask_for_popcorn() -> 'bon_appetit'.
Purpose: Allows anyone to buy popcorn.
Parameters: None.
Returns:
  'bon_appetit': A confirmation that popcorn is available.
```

```Erlang
-spec ask_for_popcorn() -> 'bon_appetit'.
ask_for_popcorn() ->
    gen_server:call(?MODULE, popcorn).
```

--------------------------------

### Analyze Initial Proper Quickcheck Failure Output

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

This snippet displays the output from `proper:quickcheck` after the initial run of `prop_server_works_fine()`. It shows a test failure after 30 iterations, detailing the sequence of commands that led to the failure, the execution history, the final state of the abstract state machine, and the `Result: {postcondition,false}` indicating a failed postcondition. The output also includes the 'shrinking' process, which simplifies the failing test case.

```erl
8> proper:quickcheck(movie_statem:prop_server_works_fine()).
.............................!
Failed: After 30 test(s).
[{set,{var,1},{call,movie_server,create_account,[bob]}},
 {set,{var,2},{call,movie_server,delete_account,[{var,1}]}},
 {set,{var,3},{call,movie_server,create_account,[bob]}},
 {set,{var,4},{call,movie_server,delete_account,[{var,3}]}},
 {set,{var,5},{call,movie_server,ask_for_popcorn,[]}},
 {set,{var,6},{call,movie_server,create_account,[mary]}},
 {set,{var,7},{call,movie_server,rent_dvd,[{var,6},the_lion_king]}},
 {set,{var,8},{call,movie_server,create_account,[mary]}},
 {set,{var,9},{call,movie_server,delete_account,[{var,6}]}}]
 History: [{{state,[],[]},1},{{state,[1],[]},account_deleted},
           {{state,[],[]},2},{{state,[2],[]},account_deleted},
           {{state,[],[]},bon_appetit},{{state,[],[]},3},
           {{state,[3],[]},[the_lion_king]},
           {{state,[3],[{3,the_lion_king}]},4},
           {{state,[4,3],[{3,the_lion_king}]},return_movies_first}]
 State: {state,[4],[{3,the_lion_king}]}
 Result: {postcondition,false}

Shrinking ..(2 time(s))
[{set,{var,6},{call,movie_server,create_account,[mary]}},
 {set,{var,7},{call,movie_server,rent_dvd,[{var,6},the_lion_king]}},
 {set,{var,9},{call,movie_server,delete_account,[{var,6}]}}]
History: [{{state,[],[]},1},{{state,[1],[]},[the_lion_king]},
          {{state,[1],[{1,the_lion_king}]},return_movies_first}]
State: {state,[],[{1,the_lion_king}]}
Result: {postcondition,false}
false
```

--------------------------------

### API: Return DVD

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Describes the API for returning a DVD. The movie is removed from the user's account, and an updated list of rented movies is returned.

```APIDOC
return_dvd(password(), movie()) -> [movie()] | 'not_a_client'.
Purpose: Returns a rented DVD.
Parameters:
  password(): The user's account password.
  movie(): The movie to return.
Returns:
  [movie()]: A list of movies still rented by the user, if successful.
  'not_a_client': If the provided password is invalid.
```

```Erlang
-spec return_dvd(password(), movie()) -> [movie()] | 'not_a_client'.
return_dvd(Password, Movie) ->
    gen_server:call(?MODULE, {return, Password, Movie}).
```

--------------------------------

### proper_gen:sample/1 Function

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_gen.html

Generates and prints a single random instance of a given type. This function is a convenience wrapper, equivalent to calling `sample/3` with a start size of 10 and an end size of 20.

```APIDOC
sample(Type :: proper_types:raw_type()) -> ok
```

--------------------------------

### Run PropEr Quickcheck and Analyze Testcase Distribution

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_finite_state_machines.md

Executes the `prop_doesnt_run_out_of_supplies` property again, demonstrating the output that includes testcase distribution statistics. This helps understand which FSM transitions and commands were tested and their frequency, providing crucial insights into test coverage and potential biases.

```erl
proper:quickcheck(food_fsm:prop_doesnt_run_out_of_supplies()).
```

--------------------------------

### PropEr FSM commands/2 Function API Documentation

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_fsm.html

Detailed API documentation for the `commands/2` function. This function is similar to `commands/1` but allows the user to specify an `InitialState` from which the generated command sequences will always begin. The first command in such sequences will be `{init, InitialState}`, ensuring correct state initialization during execution, shrinking, and counterexample checking.

```APIDOC
commands(Mod :: mod_name(), InitialState :: fsm_state()) -> proper_types:type()

Similar to `commands/1`, but generated command sequences always start at a given state. In this case, the first command is always
`{init, InitialState = {Name,Data}}` 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).
```

--------------------------------

### Implementing Precondition Callback for FSM in Erlang

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_finite_state_machines.md

This Erlang function defines the precondition for FSM transitions. In this initial setup, it's set to always return `true`, meaning no specific preconditions are enforced before any transition can occur.

```erlang
precondition(_From, _Target, _StateData, {call,_,_,_}) ->
    true.
```

--------------------------------

### Improved Test Distribution After Generator Modification

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Command line output from `proper:quickcheck` demonstrating the more balanced distribution of command execution after modifying the `command/1` generator. The `return_dvd/2` operation now has significantly higher test coverage.

```erl
42> proper:quickcheck(movie_statem:prop_server_works_fine(), 3000).
...........3000 dots.............
OK: Passed 3000 test(s).

36.69% {movie_server,rent_dvd,2}
18.84% {movie_server,return_dvd,2}
18.53% {movie_server,ask_for_popcorn,0}
18.03% {movie_server,create_account,1}
 7.91% {movie_server,delete_account,1}
true
```

--------------------------------

### Define setup_opts() Type

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper.html

Defines the options available for setting up a PropEr test run, including parameters for the number of tests, search strategy, and output function.

```APIDOC
setup_opts() =
    #{numtests := pos_integer(),
      search_steps := pos_integer(),
      search_strategy := proper_target:strategy(),
      start_size := proper_gen:size(),
      max_size := proper_gen:size(),
      output_fun := output_fun()}
```

--------------------------------

### Run Initial Equivalence Property Test (Erlang)

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_introduction_to_Property-Based_Testing.md

Demonstrates how to execute a property test for `prop_equiv_usort` using the `proper:quickcheck` function in the Erlang shell.

```erl
proper:quickcheck(my_sort:prop_equiv_usort()).
....................................................................................................
OK: Passed 100 test(s).
true
```

--------------------------------

### Generate Parallel Testcases from Initial State (parallel_commands/2)

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_statem.html

Similar to `parallel_commands/1`, but generates parallel testcases that always start at a given `InitialState`. This allows for controlled initialization of parallel test scenarios, ensuring consistency across test runs.

```APIDOC
parallel_commands(Mod :: [mod_name()], InitialState :: [symbolic_state()]) -> [proper_types:type()]
```

--------------------------------

### PropEr Postcondition for Account Creation

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Defines a `postcondition/3` callback for the `create_account` command. It ensures that the newly returned password (Result) is not already present in the system's user list (S#state.users), verifying that a new account always returns a unique password.

```Erlang
postcondition(S, {call,_,create_account,[_Name]}, Result) ->
    not lists:member(Result, S#state.users);
```

--------------------------------

### PropEr Postcondition for Buying Popcorn

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Defines a `postcondition/3` callback for the `ask_for_popcorn` command. It asserts that the server's response to buying popcorn is `bon_appetit`, verifying the expected system behavior for this specific interaction.

```Erlang
postcondition(_S, {call,_,ask_for_popcorn,[]}, Result) ->
    Result =:= bon_appetit.
```

--------------------------------

### PropEr Postcondition for Renting a DVD

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

Defines a `postcondition/3` callback for the `rent_dvd` command. It checks if the movie was available before the rental. If available, it asserts that the movie is added to the user's list (Result); otherwise, it asserts that the movie is not added, reflecting conditional behavior.

```Erlang
postcondition(S, {call,_,rent_dvd,[_Password,Movie]}, Result) ->
    case is_available(Movie, S) of
        true ->
            lists:member(Movie, Result);
        false ->
            not lists:member(Movie, Result)
    end;
```

--------------------------------

### Erlang Ping-Pong Master: Get Player Score

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_process_interaction.md

Retrieves the current score for a given player. `get_score` calls the server, and `handle_call` fetches the player's score from the master's state dictionary and replies with it.

```Erlang
get_score(Name) ->
    gen_server:call(?MASTER, {get_score, Name}).

handle_call({get_score, Name}, _From, Dict) ->
    Score = dict:fetch(Name, Dict),
        {reply, Score, Dict}.
```

--------------------------------

### Generate Command Sequences from Initial State (commands_gen/2)

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_statem.html

Generates command sequences starting from a specified initial state, similar to `commands/2`. This function is a variant of the command generation mechanism within PropEr, allowing for controlled initialization of the test sequence.

```APIDOC
commands_gen(Mod :: [mod_name()], InitialState :: [symbolic_state()]) -> [proper_types:type()]
```

--------------------------------

### PropEr Erlang Initial Command Generator for DVD Club

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_testing_of_generic_servers.md

An initial implementation of a PropEr command generator in Erlang for a DVD club system. This function defines a set of possible symbolic calls (e.g., create_account, delete_account, rent_dvd) that can be included in a test case, using simple random generation for names, passwords, and movie titles.

```Erlang
command(_S) ->
    oneof([{call,?MODULE,create_account,[name()]},
           {call,?MODULE,delete_account,[password()]},
           {call,?MODULE,rent_dvd,[password(), movie()]},
           {call,?MODULE,return_dvd,[password(), movie()]},
           {call,?MODULE,ask_for_popcorn,[]}]).
```

--------------------------------

### PropEr FSM Property for Testing

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_fsm.html

This code snippet provides an example of a PropEr property (`prop_fsm`) designed to test a finite state machine specification. It generates command sequences, runs them against the FSM, performs cleanup, and asserts that the final result is 'ok'.

```Erlang
prop_fsm() ->
    ?FORALL(Cmds, proper_fsm:commands(?MODULE),
            begin
                {_History, _State, Result} = proper_fsm:run_commands(?MODULE, Cmds),
                cleanup(),
                Result =:= ok
            end).
```

--------------------------------

### Include EUnit Library for Testing

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_introduction_to_Property-Based_Testing.md

Shows the necessary `include_lib` directive to integrate the EUnit testing framework into an Erlang module. This directive allows the module to use EUnit's macros and functions for defining structured unit tests.

```erlang
-include_lib("eunit/include/eunit.hrl").
```

--------------------------------

### Get Symbolic State After Commands (state_after/2)

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_statem.html

Returns the symbolic state of the state machine after running a given command sequence. The state is computed according to the state machine specification found in the module `Mod`, without actually executing the commands.

```APIDOC
state_after(Mod, Cmds)
```

--------------------------------

### Erlang Shell Unit Tests for my_sort

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_introduction_to_Property-Based_Testing.md

Demonstrates compiling and running basic unit tests for the `my_sort` module directly in the Erlang shell. This verifies the sorting functionality with a few manually selected inputs, providing initial confidence in the implementation.

```erl
1> c(my_sort).
{ok,my_sort}
2> my_sort:sort([17,42]).
[17,42]
3> my_sort:sort([42,17]).
[17,42]
4> my_sort:sort([3,1,4,2]).
[1,2,3,4]
```

--------------------------------

### Rewriting Recursive Native Erlang Types for PropEr Compatibility

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_typeserver.html

Provides examples and solutions for rewriting self-recursive or mutually recursive native Erlang types to ensure they are accepted by PropEr's parser when used in `?FORALL` expressions.

```Erlang
% Example of a recursive type not accepted by PropEr:
% ?FORALL(..., a(), ...)
% where:
% -type a() :: {'a','none' | a()}.

% Rewritten accepted version:
% ?FORALL(..., a(), ...)
% where:
-type a() :: {'a','none'} | {'a',a()}.

% Example of a recursive record not allowed:
% ?FORALL(..., rec(), ...)
% where:
% -type rec() :: #rec{}.
% -record(rec, {a = 0 :: integer(), b = 'nil' :: 'nil' | #rec{}}).

% Rewritten accepted version:
% ?FORALL(..., rec(), ...)
% where:
-type rec() :: #rec{b :: 'nil'} | #rec{b :: rec()}.
```

--------------------------------

### Include PropEr and EUnit Libraries

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_introduction_to_Property-Based_Testing.md

Specifies the correct order for including both PropEr and EUnit libraries in an Erlang module. PropEr's include must precede EUnit's due to potential macro conflicts, ensuring both testing frameworks can be used simultaneously.

```erlang
-include_lib("proper/include/proper.hrl").
-include_lib("eunit/include/eunit.hrl").
```

--------------------------------

### Erlang Shell: Running All Module Properties with PropEr

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/tutorials/PropEr_introduction_to_Property-Based_Testing.md

This shell interaction demonstrates how to run all properties defined within a module (`my_sort`) using `proper:module/1`. It iterates through each property, reporting its test results. The output shows successful tests for some properties and a counterexample for `prop_same_length/0`, along with the shrinking process to find a minimal failing input.

```erl
19> proper:module(my_sort).
Testing my_sort:prop_same_length_no_dupls/0
....................................................................................................
OK: Passed 100 test(s).

Testing my_sort:prop_same_length_conditional_check/0
.......x....x...xx.....x...x...x..x...x.xxx.....x..x....x.x.xx.xxxxx...x.xx.x.xxxxxxxx....xxxxxx.x.x
..xx..xx.xxxxx.x..x.xxxxx.x.xxxx..x.xx.x....x.x.x.x.x...x.xx.xx....xxx.x.xxxxxxx.x.xx.x.xxxxxx.xx..x
x..
OK: Passed 100 test(s).

Testing my_sort:prop_ordered/0
....................................................................................................
OK: Passed 100 test(s).

Testing my_sort:prop_same_length/0
.........................!
Failed: After 26 test(s).
[4,7,-5,-9,7,0,23]

Shrinking .......(7 time(s))
[0,0]

[{my_sort,prop_same_length,0}]
```

--------------------------------

### PropEr ?LAZY Macro for Delayed Generator Evaluation

Source: https://github.com/proper-testing/proper-testing.github.io/blob/master/apidocs/proper_types.html

The ?LAZY macro delays the evaluation of a generator, allowing for the simulation of lazy instance generation. This is particularly useful in Erlang to prevent infinite evaluation loops due to its eager evaluation strategy, as demonstrated by the 'stream' example.

```APIDOC
?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:
```

```Erlang
stream() -> ?LAZY(frequency([ {1,[]}, {3,[0|stream()]} ])).
```