counter_test.exs

defmodule CounterTest do
  use ExUnit.Case
  use PropCheck.StateM
  use PropCheck
  require Logger

  test "Start" do
    {:ok, pid} = Counter.start_link(0)

    assert Process.alive?(pid)
    Counter.stop()
    assert(!Process.alive?(pid))
  end

  @moduletag timeout: :infinity
  property "Server count is correct" do
    forall cmds in non_empty(commands(__MODULE__)) do
      trap_exit do
        {:ok, pid} = Counter.start_link(0)

        assert Process.alive?(pid)

        r = run_commands(__MODULE__, cmds)

        {history, state, result} = r

        Counter.stop()

        (result == :ok)
        |> when_fail(
          IO.puts("""
          History: #{inspect(history, pretty: true)}
          State: #{inspect(state, pretty: true)}
          Result: #{inspect(result, pretty: true)}
          """)
        )
        |> aggregate(command_names(cmds))
      end
    end
  end

  def initial_state() do
    %{count: 0, watches: []}
  end

  def command(_state) do
    oneof([
      {:call, Counter, :increment, []},
      {:call, Counter, :decrement, []},
      {:call, Counter, :watch, [integer(-5, 5)]}
    ])
  end

  def next_state(state = %{count: val}, _value, {:call, Counter, :increment, []}) do
    %{state | count: val + 1}
  end

  def next_state(state = %{count: val}, _value, {:call, Counter, :decrement, []}) do
    %{state | count: val - 1}
  end

  def next_state(
        state = %{watches: watches},
        _value,
        {:call, Counter, :watch, [value]}
      ) do
    %{state | watches: [value | watches]}
  end

  def precondition(_state, _call) do
    true
  end

  def postcondition(%{count: count, watches: watches}, {:call, Counter, :increment, []}, :ok) do
    watch(count + 1, watches)
    Counter.value() == count + 1
  end

  def postcondition(%{count: count, watches: watches}, {:call, Counter, :decrement, []}, :ok) do
    watch(count - 1, watches)
    Counter.value() == count - 1
  end

  def postcondition(_state, {:call, Counter, :watch, [_value]}, :ok) do
    true
  end

  #################################################################################

  def watch(_count, []) do
    :ok
  end

  def watch(count, [count | rest]) do
    receive do
      {:alarm, count} -> watch(count, rest)
    after
      50 -> raise("no_alarm")
    end
  end

  def watch(count, [_other | rest]) do
    watch(count, rest)
  end
end