PropEr

https://proper-testing.github.io/
Admin
PropEr is an automated, semi-random, property-based testing tool for Erlang programs. It supports...
Tokens:71,512
Snippets:458
Trust Score:8.3
Update:1 year ago
Show doc for...
Tokens:
Raw
### Install PropEr using Homebrew

Source: https://proper-testing.github.io/userguide

How to install the PropEr testing tool on macOS or Linux using the Homebrew package manager.

```Shell
brew install proper
```

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

### Clone PropEr Source Code from GitHub

Source: https://proper-testing.github.io/userguide

Instructions to obtain PropEr's source code by cloning its Git repository from GitHub.

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

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

### Run PropEr Quickcheck with Output Visible in EUnit

Source: https://proper-testing.github.io/userguide

Execute a PropEr quickcheck property within an EUnit test, ensuring that PropEr's output is visible by redirecting it to the user's console using the {to_file, user} option.

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

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

### Erlang proper_statem Callback: initial_state/0

Source: https://proper-testing.github.io/code/ping_pong/master_statem

Implements the 'initial_state' callback for 'proper_statem', returning the starting state of the system.

```Erlang
initial_state() ->
    #state{}.
```

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

### Erlang Targeted Property-Based Testing Example

Source: https://proper-testing.github.io/apidocs/proper_target

Illustrates the typical structure of a targeted property in PropEr, demonstrating the use of `?EXISTS` to find inputs, `SUT:run` to execute the system under test, and `?MAXIMIZE` to guide the search based on a utility value (`UV`) against a `Threshold`.

```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)).
```

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

### Erlang FSM Start Function and Initialization

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Provides the Erlang `start/1` function to initiate the `gen_fsm` process for the creature, allowing specification of the initial day type. It also includes the `init/1` callback, which sets the FSM's initial state, including the current day and an empty storage record.

```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{}}.
```

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

### Add PropEr to Erlang Library Path via .erlang File

Source: https://proper-testing.github.io/userguide

Configure the Erlang library path by adding a code:load_abs call to the user's .erlang resource file, pointing to PropEr's base directory.

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

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

### Run PropEr Quickcheck for an Erlang Property

Source: https://proper-testing.github.io/userguide

Execute a property-based test using PropEr's quickcheck function for a specific module and property defined within an Erlang application.

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

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

### Add PropEr to Erlang Library Path via ERL_LIBS

Source: https://proper-testing.github.io/userguide

Configure the Erlang library path by setting the ERL_LIBS environment variable in a shell startup file (e.g., .bashrc) to include PropEr's base directory.

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

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

### PropEr ?SETUP Property Wrapper

Source: https://proper-testing.github.io/apidocs/proper

The `?SETUP` wrapper adds a setup function `<Setup_fun>` to the property. This function is called before the first test and must return a finalize function (arity 0, which should return the atom `ok`) which is called after the last test. It is possible to use multiple `?SETUP` macros on the same property.

```APIDOC
?SETUP(<Setup_fun>, <Prop>)
  <Setup_fun>: A function called before the first test. It must return a finalize function (arity 0, returns 'ok') called after the last test.
  <Prop>: The property to be tested.
```

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

### Erlang FSM Initial State and Data Callbacks

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

These Erlang callback functions define the initial state (`initial_state`) and initial state data (`initial_state_data`) for the finite state machine model. This setup ensures the model starts in a consistent and expected state for testing purposes.

```Erlang
initial_state() -> cheese_day.

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

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

### Erlang Proper Quickcheck Failure Example 2

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

Another example of `proper:quickcheck` output showing a test failure after modifying the state machine callbacks. It highlights a scenario where a user attempts to rent a DVD after their account has been deleted, leading to a `badarg` exception due to an invalid password.

```Erlang Shell
12> proper:quickcheck(movie_statem:prop_server_works_fine()).
............................................................................
.........!
Failed: After 86 test(s).
<...testcase of 34 commands...>
History: <...long history of command execution...>
State: {state,[1],[{1,peter_pan},{1,despicable_me},{1,finding_nemo}]}
Result: {postcondition,false}

Shrinking .........(9 time(s))
[{set,{var,1},{call,movie_server,create_account,[alice]}},
 {set,{var,15},{call,movie_server,delete_account,[{var,1}]}},
 {set,{var,16},{call,movie_server,rent_dvd,[{var,1},peter_pan]}}]
History: [{{state,[],[]},1},{{state,[1],[]},account_deleted},
          {{state,[],[]},not_a_client}]
State: {state,[],[{1,peter_pan}]}
Result: {postcondition,{exception,error,badarg,
                     [{lists,member,[peter_pan,not_a_client]},
                      {movie_statem,postcondition,3},
                      <...6 more lines of stacktrace...>]}}
false
```

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

### Erlang Property-Based Test Definition

Source: https://proper-testing.github.io/code/ping_pong/master_statem

Defines the main property 'prop_master()' which uses 'proper' to generate and run sequences of commands against the 'ping_pong' state machine. It includes setup, execution, cleanup, and failure aggregation logic.

```Erlang
prop_master() ->
    ?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",
			   [pretty_history(History), pretty_state(State), Result]),
		 aggregate(command_names(Cmds), Result =:= ok))
	  end)).
```

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

### Run PropEr Quickcheck with Precondition and New Failure

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

This snippet shows the result of running PropEr quickcheck after adding the `precondition`. The previous failure mode is now avoided, but a new counterexample is discovered, indicating a different bug related to deleting an account after renting DVDs. This demonstrates how preconditions can guide testing towards new problem areas.

```Erlang
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}]}}]
```

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

### Erlang Property Test Shrinking Output Example 2

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_process_interaction

Another example of a shrunk test case output, demonstrating a different minimal sequence of operations that results in a postcondition failure. This specific case involves adding a player, playing ping-pong, and then getting the score, revealing issues with asynchronous operations.

```Erlang
[{set,{var,6},{call,ping_pong,add_player,[mary]}},
 {set,{var,7},{call,ping_pong,play_ping_pong,[mary]}},
 {set,{var,8},{call,ping_pong,get_score,[mary]}}]
History: [{{state,[],[]},ok},{{state,[mary],[{mary,0}]},ok},
          {{state,[mary],[{mary,1}]},0}]
State: {state,[mary],[{mary,1}]}
Result: {postcondition,false}
```

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

### Define Erlang Type for Setup Options Map

Source: https://proper-testing.github.io/apidocs/proper

Defines a map type for configuration options used during PropEr setup, including test counts, search parameters, and output functions.

```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()}
```

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

### Initialize Model State with initial_state/0 (Erlang)

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

Defines the initial state of the model, typically an empty record containing lists for users and rented items. This function is called once at the beginning to set up the model's starting point.

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

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

### Erlang Proper Property for Server State Machine

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

Defines a property-based test using Erlang's Proper library to verify the `movie_server` state machine. It starts the server, runs a sequence of generated commands, stops the server, and asserts that the overall command execution result is `ok`, indicating all postconditions were met.

```Erlang
prop_server_works_fine() ->
    ?FORALL(Cmds, commands(?MODULE),
            ?TRAPEXIT(
                begin
                    ?SERVER:start_link(),
                    {History,State,Result} = run_commands(?MODULE, Cmds),
                    ?SERVER:stop(),
                    ?WHENFAIL(io:format("History: ~w~nState: ~w\nResult: ~w~n",
                                        [History,State,Result]),
                              Result =:= ok)
                end)).
```

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

### Start Erlang Ping-Pong Master gen_server

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_process_interaction

This code defines the `start_link` function to initialize the ping-pong master as a local gen_server and its `init` callback. The server's internal state is initialized as an empty dictionary to store player scores, preparing it for interactions with ping-pong players.

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

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

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

### Erlang Proper Quickcheck Failure Example 1

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

Demonstrates the console output of a `proper:quickcheck` run that resulted in a failure. It shows the failing command sequence, the execution history, the final state of the abstract machine, and the `Result` indicating a postcondition violation, specifically when trying to delete an account while owing movies.

```Erlang Shell
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
```

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

### Erlang Property Test Shrinking Output Example 1

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_process_interaction

An example of the output from a property-based test shrinking process, showing the sequence of operations, historical states, and the final state that led to a failed postcondition. This snippet highlights the minimal failing test case identified by the shrinking algorithm.

```Erlang
{set,{var,11},{call,ping_pong,add_player,[alice]}},
 {set,{var,12},{call,ping_pong,add_player,[bob]}},
 {set,{var,13},{call,ping_pong,play_tennis,[john]}}]
History: [{{state,[],[]},ok},{{state,[alice],[{alice,0}]},ok},
          {{state,[alice],[{alice,1}]},maybe_later},
          {{state,[alice],[{alice,1}]},maybe_later},
          {{state,[alice],[{alice,1}]},{removed,alice}},
          {{state,[],[]},ok},{{state,[mary],[{mary,0}]},ok},
          {{state,[mary],[{mary,1}]},0}]
State: {state,[mary],[{mary,1}]}
Result: {postcondition,false}
```

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

### Quickcheck All PropEr Properties in a Module (Shell)

Source: https://proper-testing.github.io/tutorials/PropEr_introduction_to_Property-Based_Testing

This shell example demonstrates how to run all properties defined within an Erlang module (`my_sort`) using `proper:module/1`. It provides a comprehensive overview of the testing process for each property, including success messages and, in case of failure, the counterexample found and the shrinking process. The return value is a list of MFAs for properties that failed.

```Shell
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 Property for Stateful Server Testing

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

This Erlang code defines a generic PropEr property, `prop_server_works_fine/0`, for testing stateful servers. It uses `commands/1` to generate symbolic command sequences and `run_commands/2` to execute them, ensuring proper setup (`start_link`) and cleanup (`stop`) for each test run to maintain test independence.

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

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

### Run PropEr Quickcheck with Testcase Distribution Output

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Executes the instrumented `prop_doesnt_run_out_of_supplies` property. The output now includes a distribution of the transitions tested, revealing that certain transitions (like `hungry/0`) are not frequently covered.

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

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

### PropEr Symbolic Command Example

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

This code snippet illustrates a symbolic command in PropEr, binding the result of a `create_account` API call to a symbolic variable `{var,1}`. This command is not executed immediately but represents a future operation within the test sequence.

```Erlang
{set, {var,1}, {call,?SERVER,create_account,[james_bond]}}
```

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

### Erlang proper_statem Callback: precondition/2

Source: https://proper-testing.github.io/code/ping_pong/master_statem

Implements the 'precondition' callback, defining conditions that must be met for a command to be valid in the current state. For example, a player must exist to be removed or pinged.

```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,_,ping,[Name]}) ->
    lists:member(Name, S#state.players);
precondition(_, _) ->
    true.
```

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

### Erlang Proper Statem Initial State

Source: https://proper-testing.github.io/code/movies/movie_statem

This function, `initial_state/0`, defines the starting point for the state machine model. It returns a `#state{}` record with empty lists for `users` and `rented` movies, representing a fresh, uninitialized movie rental system.

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

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

### Implement Erlang gen_server Initialization Callback

Source: https://proper-testing.github.io/code/movies/movie_server

The `init/1` callback is invoked when the `gen_server` starts. It initializes the server's state by creating two ETS tables: one for users and one for movies, populating the movie table with initial data defined by `?MOVIES`.

```Erlang
init([]) ->
    Tid = ets:new(movies, []),
    ets:insert(Tid, ?MOVIES),
    {ok, #state{users     = ets:new(users, []),
		movies    = Tid,
		next_pass = 1}}.
```

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

### Erlang Property-Based Test for Ping-Pong System

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_process_interaction

This Erlang code defines `prop_ping_pong_works/0`, a property-based test using the `proper` library. It generates sequences of commands, executes them against the `?MASTER` process, and asserts that the overall result of the command execution is `ok`. The test includes setup (`start_link`), teardown (`stop`), and detailed failure reporting with history, state, and result information.

```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]),
                              aggregate(command_names(Cmds), Result =:= ok))
                end)).
```

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

### Run Initial PropEr Quickcheck Test

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Executes the first property-based test using PropEr's `quickcheck` function on the `food_fsm` module's `prop_doesnt_run_out_of_supplies` property. This initial run is expected to fail, demonstrating a common issue with FSM transitions.

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

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

### Instrument PropEr Property for Testcase Distribution

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Shows how to instrument an Erlang PropEr property (`prop_doesnt_run_out_of_supplies`) using `?FORALL`, `proper_fsm:commands`, `proper_fsm:run_commands`, and `aggregate`. This instrumentation collects statistics about the distribution of tested transitions, providing insights into test coverage.

```Erlang
prop_doesnt_run_out_of_supplies() ->
    ?FORALL(Cmds, proper_fsm:commands(?MODULE),
            begin
                start(cheese_day), %% could also be grapes_day or lettuce_day,
                                   %% but the same kind of day should be used
                                   %% to initialize the model state
                {History, State, Result} = proper_fsm:run_commands(?MODULE, Cmds),
                stop(),
                ?WHENFAIL(io:format("History: ~w~nState: ~w\nResult: ~w~n",
                                    [History, State, Result]),
                          aggregate(zip(proper_fsm:state_names(History),
                                        command_names(Cmds)),
                          Result =:= ok))
            end).
```

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

### Re-run PropEr Quickcheck After Precondition Fix

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Executes the `prop_doesnt_run_out_of_supplies` property again after implementing the `precondition` callback. This run demonstrates a new error, `cant_generate`, indicating issues with generator constraints.

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

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

### Erlang FSM History Transitions

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Defines helper functions for transitions that do not change the current state of the FSM, using `history` as the target state. `store_transition` is for buying food, and `eat_transition` is for when the creature is hungry.

```Erlang
store_transition() ->
    [{history, {call,?MODULE,buy,[food(), quantity()]}}].

eat_transition() ->
    [{history, {call,?MODULE,hungry,[]}}].
```

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

### Initial PropEr Quickcheck Test Distribution

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

Runs a PropEr quickcheck for 3000 tests on the `prop_server_works_fine` property. The output displays the initial distribution of executed commands, revealing that the `return_dvd/2` operation is rarely tested due to its preconditions.

```Erlang Shell
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
```

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

### Run PropEr Quickcheck with ?TRAPEXIT and Analyze Failure

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

After applying `?TRAPEXIT`, this snippet shows the execution of the refined PropEr property. PropEr now correctly reports a failure and provides a detailed counterexample, including the sequence of commands that led to the server crash, and demonstrates the shrinking process to find a minimal failing sequence.

```Erlang
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
```

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

### Run PropEr Quickcheck and Observe Crash

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

This snippet demonstrates an initial attempt to run a PropEr quickcheck on a state machine property. It shows the unexpected termination of the `movie_server` and, critically, PropEr itself, highlighting the need for robust error handling during property-based testing.

```Erlang
2> proper:quickcheck(movie_statem:prop_server_works_fine()).
....
=ERROR REPORT==== 29-May-2011::22:28:16 ===
** Generic server movie_server terminating
** Last message in was {return,1,inception}
** When Server state == {state,53265,49168,2}
** Reason for termination ==
** {badarg,[{ets,lookup_element,[49168,inception,2]},
            {movie_server,handle_call,3},
            {gen_server,handle_msg,5},
            {proc_lib,init_p_do_apply,3}]}
** exception exit: badarg
     in function  ets:lookup_element/3
        called as ets:lookup_element(49168,inception,2)
     in call from movie_server:handle_call/3
     in call from gen_server:handle_msg/5
     in call from proc_lib:init_p_do_apply/3
```

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

### Include PropEr Header File in Erlang Source

Source: https://proper-testing.github.io/userguide

Directive to include PropEr's header file in Erlang source files that contain properties, providing access to PropEr's macros and functions.

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

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

### Run Proper Quickcheck Test with Weighted Transitions

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Demonstrates running a `proper:quickcheck` test on a `food_fsm` module with weighted transitions. The output shows a failed test case, including the sequence of calls and the FSM's state history, indicating a problem where food supplies run out and quantities become negative.

```Erlang
15> proper:quickcheck(food_fsm:prop_doesnt_run_out_of_supplies()).
..........................!
Failed: After 27 test(s).
[{set,{var,1},{call,food_fsm,hungry,[]}},
 {set,{var,2},{call,food_fsm,new_day,[grapes]}},
 {set,{var,3},{call,food_fsm,hungry,[]}},
 {set,{var,4},{call,food_fsm,hungry,[]}},
 {set,{var,5},{call,food_fsm,hungry,[]}},
 {set,{var,6},{call,food_fsm,buy,[lettuce,3]}},
 {set,{var,7},{call,food_fsm,hungry,[]}},
 {set,{var,8},{call,food_fsm,hungry,[]}},
 {set,{var,9},{call,food_fsm,hungry,[]}},
 {set,{var,10},{call,food_fsm,buy,[cheese,3]}},
 {set,{var,11},{call,food_fsm,hungry,[]}},
 {set,{var,12},{call,food_fsm,hungry,[]}},
 {set,{var,13},{call,food_fsm,hungry,[]}}]
History: [{{cheese_day,{storage,5,5,5}},{cheese_left,5}},
          {{cheese_day,{storage,4,5,5}},ok},
          {{grapes_day,{storage,4,5,5}},{grapes_left,5}},
          {{grapes_day,{storage,4,5,4}},{grapes_left,4}},
          {{grapes_day,{storage,4,5,3}},{grapes_left,3}},
          {{grapes_day,{storage,4,5,2}},ok},
          {{grapes_day,{storage,4,8,2}},{grapes_left,2}},
          {{grapes_day,{storage,4,8,1}},{grapes_left,1}},
          {{grapes_day,{storage,4,8,0}},{grapes_left,0}}]
State: {grapes_day,{storage,4,8,-1}}
Result: {postcondition,false}

Shrinking .....(5 time(s))
[{set,{var,4},{call,food_fsm,hungry,[]}},
 {set,{var,8},{call,food_fsm,hungry,[]}},
 {set,{var,9},{call,food_fsm,hungry,[]}},
 {set,{var,11},{call,food_fsm,hungry,[]}},
 {set,{var,12},{call,food_fsm,hungry,[]}},
 {set,{var,13},{call,food_fsm,hungry,[]}}]
History: [{{cheese_day,{storage,5,5,5}},{cheese_left,5}},
          {{cheese_day,{storage,4,5,5}},{cheese_left,4}},
          {{cheese_day,{storage,3,5,5}},{cheese_left,3}},
          {{cheese_day,{storage,2,5,5}},{cheese_left,2}},
          {{cheese_day,{storage,1,5,5}},{cheese_left,1}},
          {{cheese_day,{storage,0,5,5}},{cheese_left,0}}]
State: {cheese_day,{storage,-1,5,5}}
Result: {postcondition,false}
false
```

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

### Erlang PropEr: Failed Quickcheck Output with Counterexample

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

This output from `proper:quickcheck` shows a failed test run, indicating a bug in the `movie_statem` server. It provides the sequence of commands that led to the failure, the system's history, and the state at the point of failure. The 'Shrinking' section demonstrates PropEr's ability to simplify the failing command sequence to a minimal counterexample, highlighting the core issue.

```Erlang
15> proper:quickcheck(movie_statem:prop_server_works_fine()).
...................!
Failed: After 20 test(s).
[{set,{var,1},{call,movie_server,ask_for_popcorn,[]}},
 {set,{var,2},{call,movie_server,create_account,[mary]}},
 {set,{var,3},{call,movie_server,rent_dvd,[{var,2},peter_pan]}},
 {set,{var,4},{call,movie_server,rent_dvd,[{var,2},peter_pan]}},
 {set,{var,5},{call,movie_server,create_account,[mary]}},
 {set,{var,6},{call,movie_server,return_dvd,[{var,2},peter_pan]}},
 {set,{var,7},{call,movie_server,create_account,[alice]}},
 {set,{var,8},{call,movie_server,rent_dvd,[{var,7},inception]}},
 {set,{var,9},{call,movie_server,rent_dvd,[{var,7},titanic]}},
 {set,{var,10},{call,movie_server,delete_account,[{var,2}]}}]
History: [{{state,[],[]},bon_appetit},{{state,[],[]},1},
          {{state,[1],[]},[peter_pan]},
          {{state,[1],[{1,peter_pan}]},[peter_pan]}]
State: {state,[1],[{1,peter_pan}]}
Result: {postcondition,false}

Shrinking ...(3 time(s))
[{set,{var,2},{call,movie_server,create_account,[mary]}},
 {set,{var,3},{call,movie_server,rent_dvd,[{var,2},peter_pan]}},
 {set,{var,4},{call,movie_server,rent_dvd,[{var,2},peter_pan]}}]
History: [{{state,[],[]},1},{{state,[1],[]},[peter_pan]},
          {{state,[1],[{1,peter_pan}]},[peter_pan]}]
State: {state,[1],[{1,peter_pan}]}
Result: {postcondition,false}
false
```

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

### Create New Account on Erlang Movie Server

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

This function allows a client to create a new account on the movie server. It takes the client's desired `name()` as input. Upon successful creation, the server returns a unique `password()` that must be used for all subsequent interactions with the account.

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

```APIDOC
create_account(Name: name()) -> password()
  Description: Creates a new user account on the movie server.
  Parameters:
    Name: The name of the user for whom the account is being created.
  Returns:
    password(): A unique password for the newly created account.
```

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

### Erlang PropEr: Initial Preconditions for State Machine

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_generic_servers

These Erlang `precondition/2` clauses are used in PropEr to define valid states for command execution during property-based testing. They ensure that operations like `return_dvd`, `rent_dvd`, and `delete_account` are only attempted when the system state (S) meets specific criteria, such as the user being a member or the movie being rented. This helps in guiding the shrinking process to valid counterexamples.

```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.
```

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

### Erlang Shell Manual Unit Tests

Source: https://proper-testing.github.io/tutorials/PropEr_introduction_to_Property-Based_Testing

Demonstrates compiling and running manual unit tests for the `my_sort` module directly in the Erlang shell to verify basic functionality of the sort function with specific inputs.

```Erlang Shell
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]
```

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

### Erlang Proper Quickcheck Test Execution and Results

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

This snippet shows the execution of a property-based test using Erlang's `proper:quickcheck` function. It demonstrates calling a property function `food_fsm:prop_doesnt_run_out_of_supplies()` with 1000 tests, followed by the successful test output and the distribution of states encountered during the testing process.

```Erlang
17> proper:quickcheck(food_fsm:prop_doesnt_run_out_of_supplies(), 1000).
...........1000 dots.............
OK: Passed 1000 test(s).

19% {cheese_day,{food_fsm,hungry,0}}
13% {cheese_day,{food_fsm,buy,2}}
13% {cheese_day,{food_fsm,new_day,1}}
11% {lettuce_day,{food_fsm,hungry,0}}
11% {grapes_day,{food_fsm,hungry,0}}
 8% {lettuce_day,{food_fsm,new_day,1}}
 8% {grapes_day,{food_fsm,buy,2}}
 7% {lettuce_day,{food_fsm,buy,2}}
 7% {grapes_day,{food_fsm,buy,2}}
true
```

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

### Erlang Shell EUnit Test Run

Source: https://proper-testing.github.io/tutorials/PropEr_introduction_to_Property-Based_Testing

Shows how to recompile the module and execute all defined EUnit tests from the Erlang shell, confirming test pass/fail status.

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

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

### Define FSM Transitions with Multiple Targets

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Illustrates an Erlang FSM state `cheese_day` that can transition to multiple target states (`grapes_day`, `lettuce_day`) via the same symbolic call `new_day/1`. This setup leads to the `too_many_targets` error in PropEr if not disambiguated by preconditions.

```Erlang
cheese_day(_S) ->
    [{grapes_day,  {call,?MODULE,new_day,[grapes]}},
     {lettuce_day, {call,?MODULE,new_day,[lettuce]}}].
```

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

### Erlang FSM Buy Event and Food Replenishment

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Defines the `buy/2` function for sending a `store` event to the FSM, simulating the creature buying food. It includes the `gen_fsm` event handlers for `store` across different day states, updating the food quantities in the storage record based on the type of food purchased.

```Erlang
-spec buy(food(), quantity()) -> 'ok'.
buy(Food, Quantity) ->
    gen_fsm:send_event(creature, {store, Food, Quantity}).
cheese_day({store, Food, Quantity}, S) ->
    case Food of
        cheese ->
            {next_state, cheese_day,
             S#storage{cheese = S#storage.cheese + Quantity}};
        lettuce ->
            {next_state, cheese_day,
             S#storage{lettuce = S#storage.lettuce + Quantity}};
        grapes ->
            {next_state, cheese_day,
             S#storage{grapes = S#storage.grapes + Quantity}}
    end;
lettuce_day({store, Food, Quantity}, S) ->
    case Food of
        cheese ->
            {next_state, lettuce_day,
             S#storage{cheese = S#storage.cheese + Quantity}};
        lettuce ->
            {next_state, lettuce_day,
             S#storage{lettuce = S#storage.lettuce + Quantity}};
        grapes ->
            {next_state, lettuce_day,
             S#storage{grapes = S#storage.grapes + Quantity}}
    end;
grapes_day({store, Food, Quantity}, S) ->
    case Food of
        cheese ->
            {next_state, grapes_day,
             S#storage{cheese = S#storage.cheese + Quantity}};
        lettuce ->
            {next_state, grapes_day,
             S#storage{lettuce = S#storage.lettuce + Quantity}};
        grapes ->
            {next_state, grapes_day,
             S#storage{grapes = S#storage.grapes + Quantity}}
    end;
```

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

### Erlang FSM New Day Event Handling

Source: https://proper-testing.github.io/tutorials/PropEr_testing_of_finite_state_machines

Introduces the `new_day/1` function, which sends a `new_day` event to the FSM to simulate the start of a new day with a specified food type. It includes the `gen_fsm` event handler for `new_day` when the creature is on a `cheese_day` and transitions to a `lettuce_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};
```
Tokens:
Raw