### Configuration Options for PropCheck

Source: https://context7.com/alfert/propcheck/llms.txt

Configure PropCheck behavior through mix.exs, application environment, and property options. Examples show counter example storage and property-level options.

```elixir
# mix.exs - Configure counter example storage
def project do
  [
    # ... other options
    propcheck: [counter_examples: "_build/propcheck.ctx"]
  ]
end

# config/test.exs - Application environment configuration
config :propcheck, counter_examples: "test/counter_examples.ctx"

# Property-level options
property "with custom options", [
  :verbose,                    # Print progress
  {:numtests, 500},            # Run 500 tests
  {:max_size, 100},            # Maximum size parameter
  {:max_shrinks, 1000},        # Maximum shrinking attempts
  {:start_size, 5},            # Initial size parameter
  {:constraint_tries, 100},    # Attempts for such_that constraints
  :noshrink                    # Disable shrinking
] do
  forall n <- nat() do
    n >= 0
  end
end

# Module-level default options
defmodule MyTests do
  use ExUnit.Case
  use PropCheck, default_opts: [:quiet, {:numtests, 200}]

  # All properties in this module use these defaults
  property "uses module defaults" do
    forall n <- nat(), do: n >= 0
  end
end

# Environment variables
# PROPCHECK_VERBOSE=1 mix test          # Enable verbose output
# PROPCHECK_DETECT_EXCEPTIONS=1 mix test # Enable exception detection
```

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

### Targeted Property-Based Testing with PropCheck

Source: https://context7.com/alfert/propcheck/llms.txt

Use guided search to find specific edge cases by maximizing or minimizing a fitness function. Requires importing PropCheck.

```elixir
use PropCheck

property "find path through maze using targeted search", [{:search_steps, 1000}] do
  exists path <- list(oneof([:up, :down, :left, :right])) do
    position = Maze.follow_path(@maze, @start, path)
    distance = Maze.distance(position, @exit)

    # Guide search toward the exit
    minimize(distance)

    position == @exit
  end
end

property "find large value in tree", [{:search_steps, 500}] do
  exists tree <- tree_generator() do
    max_value = Tree.max_value(tree)

    # Search for trees with large values
    maximize(max_value)

    max_value > 1000
  end
end

# forall_targeted - all instances should satisfy property
property "no path exceeds limit" do
  forall_targeted path <- path_generator() do
    length(path) < 100
  end
end

# not_exists - prove something doesn't exist
property "no shortcut exists" do
  not_exists path <- path_generator() do
    valid_shortcut?(path)
  end
end
```

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

### Configure counter-example file via application environment

Source: https://github.com/alfert/propcheck/blob/master/README.md

Set the counter-example filename using the application environment configuration.

```elixir
config :propcheck, counter_examples: "filename"
```

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

### Configure counter-example file in mix.exs

Source: https://github.com/alfert/propcheck/blob/master/README.md

Specify a custom filename for storing counter-examples within the project configuration.

```elixir
def project() do
  [ # many other options
    propcheck: [counter_examples: "filename"]
  ]
end
```

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

### Basic Property Test with ExUnit

Source: https://context7.com/alfert/propcheck/llms.txt

Demonstrates a basic property test using `use PropCheck` and the `property` macro with `forall` to test list reversal idempotency.

```elixir
defmodule MyPropertyTest do
  use ExUnit.Case
  use PropCheck

  property "list reversal is idempotent" do
    forall l <- list(integer()) do
      Enum.reverse(Enum.reverse(l)) == l
    end
  end
end
```

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

### Run properties directly with quickcheck

Source: https://context7.com/alfert/propcheck/llms.txt

Execute properties outside of ExUnit, useful for interactive IEx sessions.

```elixir
use PropCheck

# Basic quickcheck
quickcheck(
  forall n <- nat() do
    n >= 0
  end
)
# Returns: true

# With options
quickcheck(
  forall l <- list(integer()) do
    Enum.reverse(Enum.reverse(l)) == l
  end,
  [:verbose, {:numtests, 500}, {:max_size, 100}]
)

# Get counterexample on failure
result = quickcheck(
  forall n <- pos_integer() do
    n < 10  # Will fail for n >= 10
  end,
  [:long_result]
)
# Returns counterexample list on failure, e.g., [10]
```

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

### Sample a list of values from a generator

Source: https://context7.com/alfert/propcheck/llms.txt

Use `produce/1` with a list generator to sample a list of values. This helps in understanding the distribution of generated lists.

```elixir
{:ok, list_value} = produce(list(integer()))
# e.g., {:ok, [-3, 12, 0, 5]}
```

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

### Sample multiple values to understand distribution

Source: https://context7.com/alfert/propcheck/llms.txt

Use a loop with `produce/1` to sample multiple values from a generator, allowing observation of frequency and distribution.

```elixir
# Sample multiple values to understand distribution
for _ <- 1..10 do
  {:ok, v} = produce(frequency([{3, :common}, {1, :rare}]))
  v
end
# e.g., [:common, :common, :rare, :common, :common, ...]
```

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

### Define PingPong State Machine for Callback Style Testing

Source: https://context7.com/alfert/propcheck/llms.txt

Defines a state machine for a ping-pong game using explicit callbacks. It includes initial state, command generation based on state, state transitions, preconditions, and postconditions.

```elixir
defmodule PingPongTest do
  use PropCheck.StateM
  use ExUnit.Case

  defstruct players: [], scores: %{}

  def initial_state, do: %__MODULE__{}

  # Command generator based on current state
  def command(%__MODULE__{players: []}),
    do: {:call, Server, :add_player, [name()]}

  def command(state) do
    oneof([
      {:call, Server, :add_player, [name()]},
      {:call, Server, :remove_player, [name(state)]},
      {:call, Server, :play, [name(state)]}
    ])
  end

  def name, do: elements([:alice, :bob, :charlie])
  def name(%{players: p}), do: elements(p)

  # State transitions
  def next_state(s, _v, {:call, Server, :add_player, [name]}) do
    if name in s.players do
      s
    else
      %{s | players: [name | s.players], scores: Map.put(s.scores, name, 0)}
    end
  end

  def next_state(s, _v, {:call, Server, :remove_player, [name]}) do
    %{s | players: List.delete(s.players, name), scores: Map.delete(s.scores, name)}
  end

  def next_state(s, _v, {:call, Server, :play, [name]}) do
    %{s | scores: Map.update!(s.scores, name, &(&1 + 1))}
  end

  # Preconditions
  def precondition(s, {:call, Server, :remove_player, [name]}), do: name in s.players
  def precondition(s, {:call, Server, :play, [name]}), do: name in s.players
  def precondition(_s, _call), do: true

  # Postconditions
  def postcondition(_s, {:call, Server, :add_player, [_]}, :ok), do: true
  def postcondition(_s, {:call, Server, :remove_player, [n]}, {:removed, n}), do: true
  def postcondition(_s, {:call, Server, :play, [_]}, :ok), do: true
  def postcondition(_s, _call, _result), do: false

  property "server operations work correctly" do
    forall cmds <- commands(__MODULE__) do
      Server.start_link()
      {history, state, result} = run_commands(__MODULE__, cmds)
      Server.stop()
      result == :ok
    end
  end
end
```

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

### Explore shrinking behavior

Source: https://context7.com/alfert/propcheck/llms.txt

Use `sample_shrink/2` to observe the shrinking sequence of a generated value, which is crucial for understanding how PropCheck reduces failing test cases.

```elixir
# Explore shrinking behavior
sample_shrink(list(integer()), 10)
# Prints the shrinking sequence
```

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

### Sample values with a custom size

Source: https://context7.com/alfert/propcheck/llms.txt

Use `produce/2` to sample values from a generator with a specified maximum size, particularly useful for collection types like lists.

```elixir
# With custom size
{:ok, large_list} = produce(list(integer()), 50)
```

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

### Universal Property Testing with forall/2

Source: https://context7.com/alfert/propcheck/llms.txt

The `forall` macro binds generated values to variables for evaluating boolean expressions. It supports single or multiple generator bindings.

```elixir
use PropCheck

# Single generator binding
property "natural numbers are non-negative" do
  forall n <- nat() do
    n >= 0
  end
end
```

```elixir
# Multiple generator bindings with list syntax
property "sum of products is non-negative" do
  forall [n <- nat(), l <- list(nat())] do
    n * Enum.sum(l) >= 0
  end
end
```

```elixir
# Alternative tuple syntax for multiple generators
property "tuple binding example" do
  forall {a, b} <- {integer(), integer()} do
    a + b == b + a
  end
end
```

```elixir
# Using verbose mode to see test progress
quickcheck(
  forall n <- nat() do
    n >= 0
  end,
  [:verbose, {:numtests, 200}]
)
```

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

### Define Cache Model for State Machine Testing

Source: https://context7.com/alfert/propcheck/llms.txt

Defines a model for a cache with a maximum size, including initial state, command generation, and specific command implementations for testing.

```elixir
defmodule CacheTest do
  use ExUnit.Case
  use PropCheck
  use PropCheck.StateM.ModelDSL

  # Model state
  defstruct entries: [], max: 10

  # Initial model state
  def initial_state, do: %__MODULE__{}

  # Generate commands with frequency weights
  def command_gen(_state) do
    frequency([
      {3, {:find, [key()]}},
      {1, {:cache, [key(), val()]}},
      {1, {:flush, []}}
    ])
  end

  def key, do: oneof([integer(1, 10), integer()])
  def val, do: integer()

  # Define command: find
  defcommand :find do
    def impl(key), do: Cache.find(key)

    def post(%__MODULE__{entries: entries}, [key], result) do
      case List.keyfind(entries, key, 0, false) do
        false -> result == {:error, :not_found}
        {^key, val} -> result == {:ok, val}
      end
    end
  end

  # Define command: cache
  defcommand :cache do
    def impl(key, val), do: Cache.cache(key, val)

    def next(state = %__MODULE__{entries: l, max: m}, [k, v], _res) do
      new_entries = case List.keyfind(l, k, 0, false) do
        false when length(l) >= m -> tl(l) ++ [{k, v}]
        false -> l ++ [{k, v}]
        {^k, _} -> List.keyreplace(l, k, 0, {k, v})
      end
      %{state | entries: new_entries}
    end
  end

  # Define command: flush
  defcommand :flush do
    def impl, do: Cache.flush()
    def next(state, _args, _res), do: %{state | entries: []}
    def pre(%__MODULE__{entries: e}, _args), do: e != []  # Don't flush empty cache
  end

  # The property
  property "cache operations are correct" do
    forall cmds <- commands(__MODULE__) do
      Cache.start_link(10)
      {history, state, result} = run_commands(__MODULE__, cmds)
      Cache.stop()

      (result == :ok)
      |> when_fail(print_report({history, state, result}, cmds))
    end
  end
end
```

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

### Sample a single value from a generator

Source: https://context7.com/alfert/propcheck/llms.txt

Use `produce/1` to sample a single value from a generator. This is useful for debugging and understanding generator behavior.

```elixir
use PropCheck

# Sample a single value
{:ok, value} = produce(nat())
# e.g., {:ok, 7}
```

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

### Re-check a specific counterexample

Source: https://context7.com/alfert/propcheck/llms.txt

Use the `check` function with a generator and a list of specific values to re-verify a known counterexample.

```elixir
check(
  forall n <- pos_integer() do
    n < 100
  end,
  [10]  # The counterexample to verify
)
```

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

### Create choice generators with union and frequency

Source: https://context7.com/alfert/propcheck/llms.txt

Use union, frequency, oneof, and elements to generate data from multiple alternatives.

```elixir
use PropCheck

# Simple union - equal probability for each type
mixed_type = union([integer(), atom(), binary()])

property "mixed types are one of the expected types" do
  forall x <- mixed_type do
    is_integer(x) or is_atom(x) or is_binary(x)
  end
end

# Weighted union - control probability of each type
weighted_type = frequency([
  {3, integer()},      # 3x more likely
  {1, atom()},         # baseline probability
  {1, binary()}        # baseline probability
])

# oneof is an alias for union
value = oneof([:ok, :error, :pending])

# elements picks from a list of concrete values
status = elements([:active, :inactive, :pending])

property "status is valid" do
  forall s <- status do
    s in [:active, :inactive, :pending]
  end
end
```

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

### Control generation size

Source: https://context7.com/alfert/propcheck/llms.txt

Use sized and resize to manipulate the complexity parameter of generated data.

```elixir
use PropCheck

# Access current size parameter
property "size-aware generation" do
  forall l <- sized(size, resize(size * 2, list(integer()))) do
    # Lists grow twice as fast as normal
    length(l) <= 84  # max_size defaults to 42, so 42*2 = 84
  end
end

# Custom tree generator using sized
tree_gen = fn
  (0, _, _) -> :leaf
  (s, g, tree) ->
    frequency([
      {1, tree.(0, g, tree)},
      {9, let_shrink([
        l <- tree.(div(s, 2), g, tree),
        r <- tree.(div(s, 2), g, tree)
      ]) do
        {:node, g, l, r}
      end}
    ])
end

tree = fn(g) -> sized(s, tree_gen.(s, g, tree_gen)) end

property "trees are valid" do
  forall t <- tree.(int()) do
    t == :leaf or is_tuple(t)
  end
end
```

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

### Dependent Generator Binding with let/2

Source: https://context7.com/alfert/propcheck/llms.txt

The `let` macro creates derived generators by transforming generated values. It allows building complex generators from simpler ones and supports pinning variables.

```elixir
use PropCheck

# Create an even number generator
even = let n <- nat() do
  n * 2
end

property "even numbers are divisible by 2" do
  forall n <- even do
    rem(n, 2) == 0
  end
end
```

```elixir
# Multiple bindings for complex generators
even_factor = let [n <- nat(), m <- nat()] do
  n * m * 2
end
```

```elixir
# Pinning variables to reference earlier bindings in the same let
non_decreasing = let [m <- integer(^l, :inf), l <- integer(), h <- integer(^m, :inf)] do
  {l, m, h}
end

property "non-decreasing tuples are ordered" do
  forall {l, m, h} <- non_decreasing do
    l <= m and m <= h
  end
end
```

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

### Force-push updated branch

Source: https://github.com/alfert/propcheck/blob/master/README.md

Use this command to push changes after a rebase, ensuring a safer update than a standard force push.

```bash
git push --force-with-lease
```

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

### Add PropCheck dependency to mix.exs

Source: https://github.com/alfert/propcheck/blob/master/README.md

Include PropCheck in the project dependencies for test and development environments.

```elixir
defp deps do
  [
    {:propcheck, "~> 1.5", only: [:test, :dev]}
  ]
end
```

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

### Rebase feature branch on master

Source: https://github.com/alfert/propcheck/blob/master/README.md

Use these commands to synchronize a feature branch with the latest master branch before submitting a pull request.

```bash
git checkout master
git pull --rebase
git checkout my_feature
git rebase master
```

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

### Collect test statistics

Source: https://context7.com/alfert/propcheck/llms.txt

Use collect, aggregate, classify, and measure to gather data about test distribution. Requires :verbose mode.

```elixir
use PropCheck

property "collecting statistics about list lengths", [:verbose] do
  forall l <- list(integer()) do
    true
    |> collect(length(l))  # Collects length of each generated list
  end
end

property "aggregate multiple categories", [:verbose] do
  forall l <- list(integer()) do
    categories = [
      if(length(l) < 5, do: :short, else: :long),
      if(Enum.sum(l) >= 0, do: :positive_sum, else: :negative_sum)
    ]

    true
    |> aggregate(categories)
  end
end

property "classify test cases", [:verbose] do
  forall n <- integer() do
    true
    |> classify(n > 0, :positive)
    |> classify(n < 0, :negative)
    |> classify(n == 0, :zero)
  end
end

property "measure numeric statistics", [:verbose] do
  forall l <- list(integer()) do
    true
    |> measure("list length", length(l))
  end
end
```

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

### Debug failed properties with when_fail

Source: https://context7.com/alfert/propcheck/llms.txt

Execute side effects like logging when a property fails.

```elixir
use PropCheck

property "list operations with debug output" do
  forall l <- list(integer()) do
    result = Enum.sum(l) >= 0

    when_fail(result,
      IO.puts("Failed with list: #{inspect(l)}, sum: #{Enum.sum(l)}")
    )
  end
end

# Combining with aggregate for statistics
property "comprehensive testing with failure info" do
  forall l <- list(integer()) do
    result = length(l) < 100

    result
    |> when_fail(IO.puts("List too long: #{length(l)}"))
    |> aggregate(length(l))
  end
end
```

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

### PropCheck Basic Type Generators

Source: https://context7.com/alfert/propcheck/llms.txt

PropCheck provides generators for various basic types including integers, floats, booleans, atoms, binaries, and strings.

```elixir
use PropCheck

# Integer generators
integer()                    # All integers
integer(1, 100)              # Integers between 1 and 100
pos_integer()                # Positive integers (>= 1)
non_neg_integer()            # Non-negative integers (>= 0)
neg_integer()                # Negative integers (<= -1)
nat()                        # Small non-negative integers (size-bounded)
int()                        # Small integers (size-bounded, both positive and negative)
```

```elixir
# Float generators
float()                      # All floats
float(-1.0, 1.0)             # Floats in range
non_neg_float()              # Non-negative floats
```

```elixir
# Other basic types
boolean()                    # true or false
atom()                       # Random atoms
binary()                     # Random binaries
binary(10)                   # Binary of exactly 10 bytes
utf8()                       # UTF-8 encoded strings
```

```elixir
# Collection generators
list(integer())              # List of integers
list()                       # List of any type
vector(5, integer())         # List of exactly 5 integers
map(atom(), integer())       # Map with atom keys and integer values
tuple([integer(), atom()])   # Tuple of specific types
loose_tuple(integer())       # Tuple of any size with integer elements
```

```elixir
# Example property using various generators
property "map operations preserve keys" do
  forall m <- map(atom(), integer()) do
    Map.keys(m) |> Enum.all?(&is_atom/1)
  end
end
```

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

### Code Instrumentation for Concurrency Testing

Source: https://context7.com/alfert/propcheck/llms.txt

Instrument code to add yield points for more thorough concurrency testing. Requires importing PropCheck.Instrument.

```elixir
defmodule ConcurrencyTest do
  use ExUnit.Case
  use PropCheck
  use PropCheck.StateM.ModelDSL

  alias PropCheck.Instrument

  setup_all do
    # Instrument the module under test to add yield points
    Instrument.instrument_module(MyCache, PropCheck.YieldInstrumenter)
    :ok
  end

  property "concurrent cache operations are linearizable" do
    forall cmds <- parallel_commands(__MODULE__) do
      MyCache.start_link()
      {seq_history, par_history, result} = run_parallel_commands(__MODULE__, cmds)
      MyCache.stop()

      (result == :ok)
      |> when_fail(IO.puts("Linearization failed"))
    end
  end
end

# Instrument an entire application
Instrument.instrument_app(:my_app, PropCheck.YieldInstrumenter)

# Check if a module is already instrumented
Instrument.is_instrumented?(MyModule)
```

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

### Define conditional properties with implies

Source: https://context7.com/alfert/propcheck/llms.txt

The implies macro skips test cases that do not satisfy a precondition.

```elixir
use PropCheck
require Integer

property "square root of positive numbers is positive" do
  forall n <- integer() do
    implies n > 0 do
      :math.sqrt(n) > 0
    end
  end
end

property "even numbers are divisible by 2" do
  forall n <- nat() do
    implies rem(n, 2) == 0, do: Integer.is_even(n)
  end
end
```

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

### Filtering Generated Values with such_that/2

Source: https://context7.com/alfert/propcheck/llms.txt

The `such_that` macro filters generated values to include only those satisfying a given condition. Use sparingly as strict constraints can slow down test generation.

```elixir
use PropCheck

# Generate only even natural numbers
even = such_that n <- nat(), when: rem(n, 2) == 0

property "filtered evens are even" do
  forall n <- even do
    rem(n, 2) == 0
  end
end
```

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

### Define constrained generators

Source: https://context7.com/alfert/propcheck/llms.txt

Use such_that to filter generated values based on specific conditions.

```elixir
non_empty_list = such_that l <- list(nat()), when: length(l) > 0

# Non-strict version - returns unfiltered value if constraint_tries exceeded
maybe_even = such_that_maybe n <- nat(), when: rem(n, 2) == 0

property "list has at least two elements" do
  twofer_list = such_that l <- list(nat()), when: length(l) > 1
  forall [_ | t] <- twofer_list do
    Enum.any?(t)
  end
end
```

=== COMPLETE CONTENT === This response contains all available snippets from this library. No additional content exists. Do not make further requests.