/**
/* Internal tests for the linearizability checker
*/

#include <linearizability_tester.h>
#include <sequential_data_structures.h>

using namespace lt;

static void test_lru_cache()
{
  LruCache<char> lru_cache{ 3 };
  assert(lru_cache.insert('\1'));
  assert(!lru_cache.insert('\1'));

  assert(lru_cache.insert('\2'));
  assert(lru_cache.insert('\3'));
  assert(lru_cache.insert('\1'));
  assert(!lru_cache.insert('\3'));
  assert(lru_cache.insert('\4'));
  assert(lru_cache.insert('\1'));
}

static void test_atomic_op()
{
  bool ok;
  state::Atomic atomic, new_atomic;

  OpPtr<state::Atomic> read_call_op_ptr;

  OpPtr<state::Atomic> read_0_ret_op_ptr, read_0_pending_op_ptr;
  OpPtr<state::Atomic> read_1_ret_op_ptr;
  OpPtr<state::Atomic> read_2_ret_op_ptr;

  OpPtr<state::Atomic> write_1_call_op_ptr, write_1_ret_op_ptr, write_1_pending_op_ptr;
  OpPtr<state::Atomic> cas_2_succeeded_call_op_ptr, cas_2_succeeded_ret_op_ptr, cas_2_pending_op_ptr;
  OpPtr<state::Atomic> cas_2_failed_call_op_ptr, cas_2_failed_ret_op_ptr;

  read_call_op_ptr = state::Atomic::make_read_call();

  read_0_ret_op_ptr = state::Atomic::make_read_ret('\0');
  read_0_pending_op_ptr = state::Atomic::make_read_pending();
  read_1_ret_op_ptr = state::Atomic::make_read_ret('\1');
  read_2_ret_op_ptr = state::Atomic::make_read_ret('\2');

  write_1_call_op_ptr = state::Atomic::make_write_call('\1');
  write_1_ret_op_ptr = state::Atomic::make_write_ret();
  write_1_pending_op_ptr = state::Atomic::make_write_pending();

  cas_2_succeeded_call_op_ptr = state::Atomic::make_cas_call('\1', '\2');
  cas_2_succeeded_ret_op_ptr = state::Atomic::make_cas_ret(true);
  cas_2_pending_op_ptr = state::Atomic::make_cas_pending();

  cas_2_failed_call_op_ptr = state::Atomic::make_cas_call('\2', '\1');
  cas_2_failed_ret_op_ptr = state::Atomic::make_cas_ret(false);

  Op<state::Atomic>& read_call_op = *read_call_op_ptr;

  Op<state::Atomic>& read_0_ret_op = *read_0_ret_op_ptr;
  Op<state::Atomic>& read_0_pending_op = *read_0_pending_op_ptr;
  Op<state::Atomic>& read_1_ret_op = *read_1_ret_op_ptr;
  Op<state::Atomic>& read_2_ret_op = *read_2_ret_op_ptr;

  Op<state::Atomic>& write_1_call_op = *write_1_call_op_ptr;
  Op<state::Atomic>& write_1_ret_op = *write_1_ret_op_ptr;
  Op<state::Atomic>& write_1_pending_op = *write_1_pending_op_ptr;

  Op<state::Atomic>& cas_2_succeeded_call_op = *cas_2_succeeded_call_op_ptr;
  Op<state::Atomic>& cas_2_succeeded_ret_op = *cas_2_succeeded_ret_op_ptr;
  Op<state::Atomic>& cas_2_pending_op = *cas_2_pending_op_ptr;

  Op<state::Atomic>& cas_2_failed_call_op = *cas_2_failed_call_op_ptr;
  Op<state::Atomic>& cas_2_failed_ret_op = *cas_2_failed_ret_op_ptr;

  assert(!read_call_op.is_partitionable());
  assert(!read_0_ret_op.is_partitionable());
  assert(!read_0_pending_op.is_partitionable());
  assert(!read_1_ret_op.is_partitionable());
  assert(!read_2_ret_op.is_partitionable());

  assert(!write_1_call_op.is_partitionable());
  assert(!write_1_ret_op.is_partitionable());
  assert(!write_1_pending_op.is_partitionable());

  assert(!cas_2_succeeded_call_op.is_partitionable());
  assert(!cas_2_succeeded_ret_op.is_partitionable());
  assert(!cas_2_pending_op.is_partitionable());
  assert(!cas_2_failed_call_op.is_partitionable());
  assert(!cas_2_failed_ret_op.is_partitionable());

  std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_0_ret_op);
  assert(atomic == new_atomic);
  assert(!ok);

  std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
  assert(atomic == new_atomic);
  assert(!ok);

  std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_0_pending_op);
  assert(atomic == new_atomic);
  assert(ok);

  std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
  assert(atomic == new_atomic);
  assert(!ok);

  std::tie(ok, new_atomic) = write_1_call_op.apply(atomic, write_1_pending_op);
  assert(atomic != new_atomic);
  assert(ok);

  std::tie(ok, new_atomic) = write_1_call_op.apply(atomic, write_1_ret_op);
  assert(atomic != new_atomic);
  assert(ok);

  atomic = new_atomic;

  std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
  assert(atomic == new_atomic);
  assert(ok);

  std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_2_ret_op);
  assert(atomic == new_atomic);
  assert(!ok);

  std::tie(ok, new_atomic) = cas_2_failed_call_op.apply(atomic, cas_2_failed_ret_op);
  assert(atomic == new_atomic);
  assert(ok);

  std::tie(ok, new_atomic) = cas_2_failed_call_op.apply(atomic, cas_2_succeeded_ret_op);
  assert(atomic == new_atomic);
  assert(!ok);

  std::tie(ok, new_atomic) = cas_2_succeeded_call_op.apply(atomic, cas_2_pending_op);
  assert(atomic != new_atomic);
  assert(ok);

  std::tie(ok, new_atomic) = cas_2_succeeded_call_op.apply(atomic, cas_2_succeeded_ret_op);
  assert(atomic != new_atomic);
  assert(ok);

  atomic = new_atomic;

  std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_2_ret_op);
  assert(atomic == new_atomic);
  assert(ok);
}

/// a few sanity checks
static void test_stack()
{
  Entry<state::Set> ret, call;
  call.set_op(state::Set::make_contains_call('\1'));
  ret.set_op(state::Set::make_ret(true));
  call.set_match(&ret);

  EntryPtr<state::Set> A{ &call }, B{ &call }, C{ &call };

  Stack<state::Set> stack{ 3 };

  assert(stack.is_empty());
  assert(!stack.is_full());
  assert(stack.size() == 0U);

  stack.push(A, state::Set());

  assert(std::get<0>(stack.top()) == A);
  assert(!stack.is_empty());
  assert(!stack.is_full());
  assert(stack.size() == 1U);

  stack.push(B, state::Set());

  assert(std::get<0>(stack.top()) == B);
  assert(!stack.is_empty());
  assert(!stack.is_full());
  assert(stack.size() == 2U);

  stack.push(C, state::Set());

  assert(std::get<0>(stack.top()) == C);
  assert(!stack.is_empty());
  assert(stack.is_full());
  assert(stack.size() == 3U);

  stack.pop();

  assert(std::get<0>(stack.top()) == B);
  assert(!stack.is_empty());
  assert(!stack.is_full());
  assert(stack.size() == 2U);

  stack.push(C, state::Set());

  assert(std::get<0>(stack.top()) == C);
  assert(!stack.is_empty());
  assert(stack.is_full());
  assert(stack.size() == 3U);

  // pop multiple entries at once
  stack.pop(2);

  assert(!stack.is_empty());
  assert(!stack.is_full());
  assert(stack.size() == 1U);

  stack.pop();

  assert(stack.is_empty());
  assert(!stack.is_full());
  assert(stack.size() == 0U);
}

static void test_bitset()
{
  constexpr unsigned bits_per_block = static_cast<unsigned>(sizeof(unsigned long) * CHAR_BIT);
  constexpr unsigned N = bits_per_block + 7;

  FlexibleBitset bitset;

  for (unsigned k{ 0U }; k < N; ++k)
    assert(!bitset.is_set(k));

  assert(bitset.is_empty());

  bitset.set(0);
  assert(bitset.is_set(0));
  assert(!bitset.is_empty());

  for (unsigned k{ 1U }; k < N; ++k)
    assert(!bitset.is_set(k));

  bitset.reset(0);
  assert(!bitset.is_set(0));
  assert(bitset.is_empty());

  bitset.set(1);
  assert(!bitset.is_set(0));
  assert(bitset.is_set(1));
  assert(!bitset.is_empty());

  for (unsigned k{ 2U }; k < N; ++k)
    assert(!bitset.is_set(k));

  bitset.set(N-1);
  assert(bitset.is_set(N-1));
  assert(!bitset.is_empty());

  for (unsigned k{ 2U }; k < N - 1U; ++k)
    assert(!bitset.is_set(k));

  FlexibleBitset another_bitset;
  another_bitset.set(1);
  another_bitset.set(N-1);
  
  FlexibleBitset yet_another_bitset(another_bitset);

  assert(bitset == another_bitset);
  assert(bitset == yet_another_bitset);

  assert(!bitset.is_set(bits_per_block - 1U));
  assert(bitset.set(bits_per_block - 1U));
  assert(bitset.is_set(bits_per_block - 1U));

  assert(!bitset.is_set(bits_per_block));
  assert(bitset.set(bits_per_block));
  assert(bitset.is_set(bits_per_block));

  assert(!bitset.is_set(bits_per_block + 1U));
  assert(bitset.set(bits_per_block + 1U));
  assert(bitset.is_set(bits_per_block + 1U));

  assert(!bitset.is_set(2U * bits_per_block - 1U));
  assert(bitset.set(2U * bits_per_block - 1U));
  assert(bitset.is_set(2U * bits_per_block - 1U));

  assert(!bitset.is_set(2U * bits_per_block));
  assert(bitset.set(2U * bits_per_block));
  assert(bitset.is_set(2U * bits_per_block));

  assert(!bitset.is_set(2U * bits_per_block + 1U));
  assert(bitset.set(2U * bits_per_block + 1U));
  assert(bitset.is_set(2U * bits_per_block + 1U));

  bitset = another_bitset;

  assert(bitset.set(2U * bits_per_block - 1U));
  assert(bitset.reset(2U * bits_per_block - 1U));
  assert(bitset == another_bitset);

  assert(bitset.set(2U * bits_per_block));
  assert(bitset.reset(2U * bits_per_block));
  // different number of blocks
  assert(bitset != another_bitset);

  assert(bitset.set(2U * bits_per_block + 1U));
  assert(bitset.reset(2U * bits_per_block + 1U));

  // different number of blocks
  assert(bitset != another_bitset);
}

static void test_state_set()
{
  bool ok;
  state::Set set;

  assert(!set.contains('\1'));

  std::tie(ok, set) = set.insert('\1');
  assert(ok);

  assert(set.contains('\1'));

  // item is already in the set
  std::tie(ok, set) = set.insert('\1');
  assert(!ok);
  assert(set.contains('\1'));

  std::tie(ok, set) = set.erase('\1');
  assert(ok);
  assert(!set.contains('\1'));

  // item has been already erased from the set
  std::tie(ok, set) = set.erase('\1');
  assert(!ok);
  assert(!set.contains('\1'));
}

static void test_state_set_op()
{
  bool ok;
  state::Set set, new_set;

  OpPtr<state::Set> empty_op_ptr;
  OpPtr<state::Set> contains_op_ptr;
  OpPtr<state::Set> insert_op_ptr;
  OpPtr<state::Set> erase_op_ptr;

  OpPtr<state::Set> true_ret_op_ptr{ state::Set::make_ret(true) };
  OpPtr<state::Set> false_ret_op_ptr{ state::Set::make_ret(false) };

  const Op<state::Set>& true_ret_op = *true_ret_op_ptr;
  const Op<state::Set>& false_ret_op = *false_ret_op_ptr;

  empty_op_ptr = state::Set::make_empty_call();
  contains_op_ptr = state::Set::make_contains_call('\1');
  insert_op_ptr = state::Set::make_insert_call('\1');
  erase_op_ptr = state::Set::make_erase_call('\1');

  Op<state::Set>& empty_op = *empty_op_ptr;
  Op<state::Set>& contains_op = *contains_op_ptr;
  Op<state::Set>& insert_op = *insert_op_ptr;
  Op<state::Set>& erase_op = *erase_op_ptr;

  std::tie(ok, new_set) = empty_op.apply(set, true_ret_op);
  assert(set == new_set);
  assert(ok);

  std::tie(ok, new_set) = contains_op.apply(set, false_ret_op);
  assert(set == new_set);
  assert(ok);

  std::tie(ok, new_set) = insert_op.apply(set, true_ret_op);
  assert(set != new_set);
  assert(ok);

  set = new_set;

  std::tie(ok, new_set) = empty_op.apply(set, false_ret_op);
  assert(set == new_set);
  assert(ok);

  std::tie(ok, new_set) = contains_op.apply(set, true_ret_op);
  assert(set == new_set);
  assert(ok);

  // item is already in the set, so insertion is unsuccessful
  std::tie(ok, new_set) = insert_op.apply(set, false_ret_op);
  assert(set == new_set);
  assert(ok);

  std::tie(ok, new_set) = contains_op.apply(set, true_ret_op);
  assert(set == new_set);
  assert(ok);

  std::tie(ok, new_set) = erase_op.apply(set, true_ret_op);
  assert(set != new_set);
  assert(ok);

  assert(std::get<0>(contains_op.apply(set, true_ret_op)));
  assert(!std::get<0>(contains_op.apply(set, false_ret_op)));

  assert(!std::get<0>(contains_op.apply(new_set, true_ret_op)));
  assert(std::get<0>(contains_op.apply(new_set, false_ret_op)));
}

static void test_state_stack()
{
  constexpr unsigned N = 2;

  state::Stack<N> stack;
  state::Stack<N> new_stack;
  state::Stack<N> stack_1, stack_2;

  assert(stack.is_empty());
  assert(!stack.is_full());

  new_stack = stack.push('\1');

  assert(stack != new_stack);
  stack = stack_1 = new_stack;

  assert(!stack.is_empty());
  assert(!stack.is_full());

  assert(stack.top() == '\1');

  new_stack = stack.push('\2');

  assert(stack != new_stack);
  stack = stack_2 = new_stack;

  assert(stack_1 != stack_2);

  assert(!stack.is_empty());
  assert(stack.is_full());

  assert(stack.top() == '\2');

  new_stack = stack.pop();
  assert(new_stack == stack_1);

  stack = new_stack;

  assert(!stack.is_empty());
  assert(!stack.is_full());

  assert(stack.top() == '\1');

  new_stack = stack.push('\2');

  assert(stack != new_stack);
  assert(new_stack == stack_2);

  stack = new_stack;

  assert(!stack.is_empty());
  assert(stack.is_full());

  assert(stack.top() == '\2');

  new_stack = stack.pop();
  assert(new_stack == stack_1);

  stack = new_stack;

  assert(!stack.is_empty());
  assert(!stack.is_full());

  assert(stack.top() == '\1');

  new_stack = stack.push('\3');

  assert(stack != new_stack);
  assert(new_stack != stack_1);
  assert(new_stack != stack_2);

  stack = new_stack;

  assert(!stack.is_empty());
  assert(stack.is_full());

  assert(stack.top() == '\3');
}

static void test_state_queue()
{
  constexpr unsigned N = 2;

  state::Queue<N> queue;

  state::Queue<N> new_queue;
  state::Queue<N> queue_1, queue_2;

  assert(queue.is_empty());
  assert(!queue.is_full());
  
  queue.enqueue('\1');
  new_queue = queue.enqueue('\1');

  assert(queue != new_queue);
  queue = queue_1 = new_queue;

  assert(!queue.is_empty());
  assert(!queue.is_full());

  assert(queue.get_value() == '\1');

  new_queue = queue.enqueue('\2');

  assert(queue != new_queue);
  queue = queue_2 = new_queue;

  assert(queue_1 != queue_2);

  assert(!queue.is_empty());
  assert(queue.is_full());

  assert(queue.get_value() == '\1');

  new_queue = queue.dequeue();
  assert(new_queue != queue_1);

  queue = new_queue;
  
  assert(!queue.is_empty());
  assert(!queue.is_full());

  assert(queue.get_value() == '\2');

  new_queue = queue.enqueue('\1');

  assert(queue != new_queue);
  assert(new_queue != queue_2);

  queue = new_queue;

  assert(!queue.is_empty());
  assert(queue.is_full());

  assert(queue.get_value() == '\2');

  new_queue = queue.dequeue();
  assert(new_queue != queue_1);
  queue = new_queue;

  assert(!queue.is_empty());
  assert(!queue.is_full());

  assert(queue.get_value() == '\1');

  new_queue = queue.enqueue('\3');

  assert(queue != new_queue);
  assert(new_queue != queue_1);
  assert(new_queue != queue_2);

  queue = new_queue;

  assert(!queue.is_empty());
  assert(queue.is_full());

  assert(queue.get_value() == '\1');
  
}

static void test_state_stack_op()
{
  constexpr unsigned N = 1;

  bool ok;
  state::Stack<N> stack, new_stack;

  OpPtr<state::Stack<N>> try_push_1_op_ptr, try_push_2_op_ptr;
  OpPtr<state::Stack<N>> try_pop_op_ptr;

  OpPtr<state::Stack<N>> true_try_push_ret_op_ptr{ state::Stack<N>::make_try_push_ret(true) };
  OpPtr<state::Stack<N>> false_try_push_ret_op_ptr{ state::Stack<N>::make_try_push_ret(false) };

  const Op<state::Stack<N>>& true_try_push_ret_op = *true_try_push_ret_op_ptr;
  const Op<state::Stack<N>>& false_try_push_ret_op = *false_try_push_ret_op_ptr;

  OpPtr<state::Stack<N>> true_1_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(true, '\1') };
  OpPtr<state::Stack<N>> true_2_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(true, '\2') };
  OpPtr<state::Stack<N>> false_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(false, '\0') };

  const Op<state::Stack<N>>& true_1_try_pop_ret_op = *true_1_try_pop_ret_op_ptr;
  const Op<state::Stack<N>>& true_2_try_pop_ret_op = *true_2_try_pop_ret_op_ptr;
  const Op<state::Stack<N>>& false_try_pop_ret_op = *false_try_pop_ret_op_ptr;

  try_pop_op_ptr = state::Stack<N>::make_try_pop_call();
  Op<state::Stack<N>>& try_pop_op = *try_pop_op_ptr;
  
  std::tie(ok, new_stack) = try_pop_op.apply(stack, false_try_pop_ret_op);
  assert(stack == new_stack);
  assert(ok);

  std::tie(ok, new_stack) = try_pop_op.apply(stack, true_1_try_pop_ret_op);
  assert(stack == new_stack);
  assert(!ok);

  std::tie(ok, new_stack) = try_pop_op.apply(stack, true_2_try_pop_ret_op);
  assert(stack == new_stack);
  assert(!ok);

  try_push_2_op_ptr = state::Stack<N>::make_try_push_call('\2');
  Op<state::Stack<N>>& try_push_2_op = *try_push_2_op_ptr;

  std::tie(ok, new_stack) = try_push_2_op.apply(stack, false_try_push_ret_op);
  assert(stack != new_stack);
  assert(!ok);
  
  std::tie(ok, new_stack) = try_push_2_op.apply(stack, true_try_push_ret_op);
  assert(stack != new_stack);
  assert(ok);

  stack = new_stack;

  try_push_1_op_ptr = state::Stack<N>::make_try_push_call('\1');
  Op<state::Stack<N>>& try_push_1_op = *try_push_1_op_ptr;

  // stack is full
  std::tie(ok, new_stack) = try_push_1_op.apply(stack, false_try_push_ret_op);
  assert(stack == new_stack);
  assert(ok);

  std::tie(ok, new_stack) = try_push_1_op.apply(stack, true_try_push_ret_op);
  assert(stack == new_stack);
  assert(!ok);

  std::tie(ok, new_stack) = try_pop_op.apply(stack, false_try_pop_ret_op);
  assert(stack != new_stack);
  assert(!ok);

  std::tie(ok, new_stack) = try_pop_op.apply(stack, true_1_try_pop_ret_op);
  assert(stack != new_stack);
  assert(!ok);

  std::tie(ok, new_stack) = try_pop_op.apply(stack, true_2_try_pop_ret_op);
  assert(stack != new_stack);
  assert(ok);
}

static void test_state_queue_op()
{
  constexpr unsigned N = 1;

  bool ok;
  state::Queue<N> queue, new_queue;

  OpPtr<state::Queue<N>> try_enqueue_1_op_ptr, try_enqueue_2_op_ptr;
  OpPtr<state::Queue<N>> try_dequeue_op_ptr;

  OpPtr<state::Queue<N>> true_try_enqueue_ret_op_ptr{ state::Queue<N>::make_try_enqueue_ret(true) };
  OpPtr<state::Queue<N>> false_try_enqueue_ret_op_ptr{ state::Queue<N>::make_try_enqueue_ret(false) };

  const Op<state::Queue<N>>& true_try_enqueue_ret_op = *true_try_enqueue_ret_op_ptr;
  const Op<state::Queue<N>>& false_try_enqueue_ret_op = *false_try_enqueue_ret_op_ptr;

  OpPtr<state::Queue<N>> true_1_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(true, '\1') };
  OpPtr<state::Queue<N>> true_2_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(true, '\2') };
  OpPtr<state::Queue<N>> false_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(false, '\0') };

  const Op<state::Queue<N>>& true_1_try_dequeue_ret_op = *true_1_try_dequeue_ret_op_ptr;
  const Op<state::Queue<N>>& true_2_try_dequeue_ret_op = *true_2_try_dequeue_ret_op_ptr;
  const Op<state::Queue<N>>& false_try_dequeue_ret_op = *false_try_dequeue_ret_op_ptr;

  try_dequeue_op_ptr = state::Queue<N>::make_try_dequeue_call();
  Op<state::Queue<N>>& try_dequeue_op = *try_dequeue_op_ptr;
  
  std::tie(ok, new_queue) = try_dequeue_op.apply(queue, false_try_dequeue_ret_op);
  assert(queue == new_queue);
  assert(ok);
  
  std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_1_try_dequeue_ret_op);
  assert(queue == new_queue);
  assert(!ok);

  std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_2_try_dequeue_ret_op);
  assert(queue == new_queue);
  assert(!ok);
  

  try_enqueue_2_op_ptr = state::Queue<N>::make_try_enqueue_call('\2');
  Op<state::Queue<N>>& try_enqueue_2_op = *try_enqueue_2_op_ptr;

  std::tie(ok, new_queue) = try_enqueue_2_op.apply(queue, false_try_enqueue_ret_op);
  assert(queue != new_queue);
  assert(!ok);
  
  std::tie(ok, new_queue) = try_enqueue_2_op.apply(queue, true_try_enqueue_ret_op);
  assert(queue != new_queue);
  assert(ok);

  queue = new_queue;

  try_enqueue_1_op_ptr = state::Queue<N>::make_try_enqueue_call('\1');
  Op<state::Queue<N>>& try_enqueue_1_op = *try_enqueue_1_op_ptr;

  // queue is full
  std::tie(ok, new_queue) = try_enqueue_1_op.apply(queue, false_try_enqueue_ret_op);
  assert(queue == new_queue);
  assert(ok);

  std::tie(ok, new_queue) = try_enqueue_1_op.apply(queue, true_try_enqueue_ret_op);
  assert(queue == new_queue);
  assert(!ok);

  std::tie(ok, new_queue) = try_dequeue_op.apply(queue, false_try_dequeue_ret_op);
  assert(queue != new_queue);
  assert(!ok);

  std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_1_try_dequeue_ret_op);
  assert(queue != new_queue);
  assert(!ok);

  std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_2_try_dequeue_ret_op);
  assert(queue != new_queue);
  assert(ok);
}
/// The empty log is trivially linearizable.
static void test_linearizability_empty_log()
{
  std::size_t number_of_entries{ 0U };
  LogInfo<state::Set> log_info;
  LinearizabilityTester<state::Set> t{ log_info };
  assert(log_info.is_empty());
  assert(t.check());
}

/// a few sanity checks on the raw entry data structure
static void test_raw_single_contains_is_linearizable()
{
  Entry<state::Set> contains_call, contains_ret;

  contains_ret.set_op(state::Set::make_ret(false));
  contains_ret.prev = &contains_call;

  contains_call.set_op(state::Set::make_contains_call('\1'));
  contains_call.next = &contains_ret;
  contains_call.set_match(&contains_ret);

  std::size_t number_of_entries{ 2U };
  LogInfo<state::Set> log_info{ &contains_call, number_of_entries };
  LinearizabilityTester<state::Set> t{ log_info };
  assert(t.check());
}

static void test_raw_single_contains_is_not_linearizable()
{
  Entry<state::Set> contains_call, contains_ret;

  contains_ret.set_op(state::Set::make_ret(true));
  contains_ret.prev = &contains_call;

  contains_call.set_op(state::Set::make_contains_call('\1'));
  contains_call.next = &contains_ret;
  contains_call.set_match(&contains_ret);

  std::size_t number_of_entries{ 2U };
  LogInfo<state::Set> log_info{ &contains_call, number_of_entries };
  LinearizabilityTester<state::Set> t{ log_info };
  assert(!t.check());
}

static void test_single_contains(bool ret)
{
  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;

  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call('\1'));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(ret));

  assert(log.log_head_ptr() == contains_call_entry_ptr);
  assert(log.number_of_entries() == 2U);

  assert(log.log_head_ptr() == contains_call_entry_ptr);
  assert(contains_call_entry_ptr->prev == nullptr);
  assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
  assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);

  assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
  assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
  assert(contains_ret_entry_ptr->next == nullptr);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == (!ret));

  if (ret)
  {
    // If log cannot be linearized, then all pointers
    // (except the first one) are still the same.
    assert(log.log_head_ptr() == contains_call_entry_ptr);
    assert(contains_call_entry_ptr->prev != nullptr);
    assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
    assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);

    assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
    assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
    assert(contains_ret_entry_ptr->next == nullptr);
  }
}

static void test_log_copy()
{
  constexpr bool ret = true;

  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;

  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call('\1'));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(ret));

  assert(log.log_head_ptr() == contains_call_entry_ptr);
  assert(log.number_of_entries() == 2U);

  assert(log.log_head_ptr() == contains_call_entry_ptr);
  assert(contains_call_entry_ptr->prev == nullptr);
  assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
  assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);

  assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
  assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
  assert(contains_ret_entry_ptr->next == nullptr);

  Log<state::Set> log_copy{ log.info() };

  assert(log_copy.log_head_ptr() != contains_call_entry_ptr);
  assert(log_copy.log_head_ptr() != contains_call_entry_ptr);
  assert(log_copy.log_head_ptr()->entry_id() == 0U);
  assert(&log_copy.log_head_ptr()->op() == &contains_call_entry_ptr->op());
  assert(log_copy.log_head_ptr() == log_copy.log_head_ptr()->match()->match());
  assert(log_copy.log_head_ptr()->prev == nullptr);
  assert(log_copy.number_of_entries() == 2U);
}

//   contains(x) : contains_ret
// |---------------------------|
//
//         insert(x) : insert_ret
//     |---------------------------|
static void test_000(bool insert_ret, bool contains_ret)
{
  constexpr char x = '\1';

  constexpr unsigned contains_entry_id{ 0U };
  constexpr unsigned insert_entry_id{ 1U };

  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;

  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
  insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));

  assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
  assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);

  assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
  assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == insert_ret);
}

//        contains(x) : contains_ret
//      |----------------------------|
//
//    insert(x) : insert_ret
// |-------------------------|
static void test_001(bool insert_ret, bool contains_ret)
{
  constexpr char x = '\1';

  constexpr unsigned insert_entry_id{ 0U };
  constexpr unsigned contains_entry_id{ 1U };

  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;

  insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));

  assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
  assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);

  assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
  assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == insert_ret);
}

//      contains(x) : contains_ret
//    |----------------------------|
//
//       insert(x) : insert_ret
// |----------------------------------|
static void test_002(bool insert_ret, bool contains_ret)
{
  constexpr char x = '\1';

  constexpr unsigned insert_entry_id{ 0U };
  constexpr unsigned contains_entry_id{ 1U };

  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;

  insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
  insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));

  assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
  assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);

  assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
  assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == insert_ret);
}

//     contains(x) : contains_ret
// |----------------------------------|
//
//       insert(x) : insert_ret
//    |---------------------------|
static void test_003(bool insert_ret, bool contains_ret)
{
  constexpr char x = '\1';

  constexpr unsigned contains_entry_id{ 0U };
  constexpr unsigned insert_entry_id{ 1U };

  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;

  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));

  assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
  assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);

  assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
  assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == insert_ret);
}

//   insert(x) : insert_ret     contains(x) : contains_ret
// |------------------------| |---------------------------|
static void test_004(bool insert_ret, bool contains_ret)
{
  constexpr char x = '\1';

  constexpr unsigned insert_entry_id{ 0U };
  constexpr unsigned contains_entry_id{ 1U };

  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;

  insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));

  assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
  assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);

  assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
  assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == (insert_ret && contains_ret));
}

//   contains(x) : contains_ret    insert(x) : insert_ret
// |---------------------------| |------------------------| 
static void test_005(bool insert_ret, bool contains_ret)
{
  constexpr char x = '\1';

  constexpr unsigned contains_entry_id{ 0U };
  constexpr unsigned insert_entry_id{ 1U };

  Log<state::Set> log{ 4U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;

  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
  insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));

  assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
  assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);

  assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
  assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == (insert_ret && !contains_ret));
}

//   insert(x) : insert_ret_0
// |--------------------------|
//
//       insert(x) : insert_ret_1
//     |--------------------------|
static void test_006(bool insert_ret_0, bool insert_ret_1)
{
  constexpr char x = '\1';

  constexpr unsigned insert_0_entry_id{ 0U };
  constexpr unsigned insert_1_entry_id{ 1U };

  EntryPtr<state::Set> insert_call_0_entry_ptr, insert_ret_0_entry_ptr;
  EntryPtr<state::Set> insert_call_1_entry_ptr, insert_ret_1_entry_ptr;

  Log<state::Set> log{ 4U };

  insert_call_0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_call_1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_ret_0_entry_ptr = log.add_ret(insert_call_0_entry_ptr, state::Set::make_ret(insert_ret_0));
  insert_ret_1_entry_ptr = log.add_ret(insert_call_1_entry_ptr, state::Set::make_ret(insert_ret_1));

  assert(insert_call_0_entry_ptr->entry_id() == insert_0_entry_id);
  assert(insert_ret_0_entry_ptr->entry_id() == insert_0_entry_id);

  assert(insert_call_1_entry_ptr->entry_id() == insert_1_entry_id);
  assert(insert_ret_1_entry_ptr->entry_id() == insert_1_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == (!(insert_ret_0 == insert_ret_1)));
}

//   insert(x) : insert_ret_0     insert(x) : insert_ret_1
// |--------------------------| |--------------------------|
static void test_007(bool insert_ret_0, bool insert_ret_1)
{
  constexpr char x = '\1';

  constexpr unsigned insert_0_entry_id{ 0U };
  constexpr unsigned insert_1_entry_id{ 1U };

  EntryPtr<state::Set> insert_call_0_entry_ptr, insert_ret_0_entry_ptr;
  EntryPtr<state::Set> insert_call_1_entry_ptr, insert_ret_1_entry_ptr;

  Log<state::Set> log{ 4U };

  insert_call_0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_ret_0_entry_ptr = log.add_ret(insert_call_0_entry_ptr, state::Set::make_ret(insert_ret_0));
  insert_call_1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_ret_1_entry_ptr = log.add_ret(insert_call_1_entry_ptr, state::Set::make_ret(insert_ret_1));

  assert(insert_call_0_entry_ptr->entry_id() == insert_0_entry_id);
  assert(insert_ret_0_entry_ptr->entry_id() == insert_0_entry_id);

  assert(insert_call_1_entry_ptr->entry_id() == insert_1_entry_id);
  assert(insert_ret_1_entry_ptr->entry_id() == insert_1_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == (insert_ret_0 && !insert_ret_1));
}

//           insert(x) : insert_ret
// |------------------------------------------|
//
//           insert(x) : insert_ret
//   |-------------------------------------|
//
//         contains(x) : contains_ret
//       |----------------------------|
//
static void test_008(bool insert_ret, bool contains_ret)
{
  constexpr char x = '\1';

  constexpr unsigned insert_0_entry_id{ 0U };
  constexpr unsigned insert_1_entry_id{ 1U };
  constexpr unsigned contains_entry_id{ 2U };

  Log<state::Set> log{ 8U };
  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  EntryPtr<state::Set> insert_0_call_entry_ptr, insert_0_ret_entry_ptr;
  EntryPtr<state::Set> insert_1_call_entry_ptr, insert_1_ret_entry_ptr;

  insert_0_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_1_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
  insert_1_ret_entry_ptr = log.add_ret(insert_1_call_entry_ptr, state::Set::make_ret(insert_ret));
  insert_0_ret_entry_ptr = log.add_ret(insert_0_call_entry_ptr, state::Set::make_ret(insert_ret));

  assert(insert_0_call_entry_ptr->entry_id() == insert_0_entry_id);
  assert(insert_0_ret_entry_ptr->entry_id() == insert_0_entry_id);

  assert(insert_1_call_entry_ptr->entry_id() == insert_1_entry_id);
  assert(insert_1_ret_entry_ptr->entry_id() == insert_1_entry_id);

  assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
  assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// !linearizable:
//
// Let x && y be distinct values.
//
//   contains(x) : false 
// |---------------------|
//
//      contains(y) : false
//    |---------------------|
//
//          insert(x) : false
//        |---------------------|
static void test_009()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned contains_x_entry_id{ 0U };
  constexpr unsigned contains_y_entry_id{ 1U };
  constexpr unsigned insert_x_entry_id{ 2U };

  Log<state::Set> log{ 6U };

  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
  EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;

  contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));

  contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
  contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
  insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));

  assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
  assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);

  assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
  assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);

  assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
  assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// !linearizable:
//
// Let x && y be distinct values.
//
//   contains(x) : false 
// |---------------------|
//
//       insert(x) : false
//    |---------------------|
//
//          contains(y) : false
//        |---------------------|
static void test_010()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned contains_x_entry_id{ 0U };
  constexpr unsigned insert_x_entry_id{ 1U };
  constexpr unsigned contains_y_entry_id{ 2U };

  Log<state::Set> log{ 6U };

  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
  EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;

  contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));

  contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
  insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));
  contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));

  assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
  assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);

  assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
  assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);

  assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
  assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// Linearizable:
//
// Let x && y be distinct values.
//
//   insert(x) : true
// |------------------|
//
//      contains(y) : false
//    |---------------------|
//
//         contains(x) : false
//       |---------------------|
static void test_011()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned insert_x_entry_id{ 0U };
  constexpr unsigned contains_y_entry_id{ 1U };
  constexpr unsigned contains_x_entry_id{ 2U };

  Log<state::Set> log{ 6U };

  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
  EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;

  insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));

  insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
  contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
  contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));

  assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
  assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);

  assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
  assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);

  assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
  assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check());
}

// Linearizable:
//
// Let x && y be distinct values.
//
//   erase(x) : false     insert(y) : true
// |------------------| |------------------|
//
//                                               contains(x) : true
//                                 |------------------------------------------------|
//
//                                      contains(y) : false     insert(x) : true
//                                    |---------------------| |------------------|
static void test_012()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  Log<state::Set> log{ 10U };

  EntryPtr<state::Set> erase_x_call_entry_ptr, erase_x_ret_entry_ptr;
  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
  EntryPtr<state::Set> insert_y_call_entry_ptr, insert_y_ret_entry_ptr;
  EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;

  erase_x_call_entry_ptr = log.add_call(state::Set::make_erase_call(x));
  erase_x_ret_entry_ptr = log.add_ret(erase_x_call_entry_ptr, state::Set::make_ret(false));
  insert_y_call_entry_ptr = log.add_call(state::Set::make_insert_call(y));
  contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  insert_y_ret_entry_ptr = log.add_ret(insert_y_call_entry_ptr, state::Set::make_ret(true));
  contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
  insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
  contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(true));

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check());
}

// entry id: X0, call: contains(x)
// entry id: X1, call: insert(x)
// entry id: X0, return: ret: 0
// entry id: X2, call: contains(x)
// entry id: X2, return: ret: 0
// entry id: X3, call: insert(x)
// entry id: X3, return: ret: 1
// entry id: X4, call: contains(x)
// entry id: X4, return: ret: 1
// entry id: X1, return: ret: 0
// entry id: X5, call: contains(x)
// entry id: X5, return: ret: 1
static void test_013()
{
  constexpr char x = '\1';

  Log<state::Set> log{ 12U };

  EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
  EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
  EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
  EntryPtr<state::Set> call_x3_entry_ptr, ret_x3_entry_ptr;
  EntryPtr<state::Set> call_x4_entry_ptr, ret_x4_entry_ptr;
  EntryPtr<state::Set> call_x5_entry_ptr, ret_x5_entry_ptr;

  call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
  call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
  call_x3_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_x3_entry_ptr = log.add_ret(call_x3_entry_ptr, state::Set::make_ret(true));
  call_x4_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x4_entry_ptr = log.add_ret(call_x4_entry_ptr, state::Set::make_ret(true));
  ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
  call_x5_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x5_entry_ptr = log.add_ret(call_x5_entry_ptr, state::Set::make_ret(true));

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check());
}

// Let x && y be distinct.
//
// entry id: X0, call: contains(x)
// entry id: X1, call: insert(x)
// entry id: X0, return: ret: 0
// entry id: Y0, call: contains(y) <- !linearizable
// entry id: Y0, return: ret: 1
// entry id: X2, call: contains(x)
// entry id: X2, return: ret: 0
// entry id: X3, call: insert(x)
// entry id: X3, return: ret: 1
// entry id: X4, call: contains(x)
// entry id: X4, return: ret: 1
// entry id: X1, return: ret: 0
// entry id: X5, call: contains(x)
// entry id: X5, return: ret: 1
static void test_014()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned not_linearizable_entry_id = 2U;

  Log<state::Set> log{ 14U };

  EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
  EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
  EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
  EntryPtr<state::Set> call_x3_entry_ptr, ret_x3_entry_ptr;
  EntryPtr<state::Set> call_x4_entry_ptr, ret_x4_entry_ptr;
  EntryPtr<state::Set> call_x5_entry_ptr, ret_x5_entry_ptr;

  EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;

  call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
  call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
  call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
  call_x3_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_x3_entry_ptr = log.add_ret(call_x3_entry_ptr, state::Set::make_ret(true));
  call_x4_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x4_entry_ptr = log.add_ret(call_x4_entry_ptr, state::Set::make_ret(true));
  ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
  call_x5_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x5_entry_ptr = log.add_ret(call_x5_entry_ptr, state::Set::make_ret(true));

  assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// !linearizable:
//
// Let x && y be distinct values.
//
//   contains(x) : false     contains(y) : true
// |---------------------| |--------------------|
//
//                          insert(x) : true
//                    |----------------------------|
static void test_015()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned contains_x_entry_id{ 0U };
  constexpr unsigned insert_x_entry_id{ 1U };
  constexpr unsigned contains_y_entry_id{ 2U };

  Log<state::Set> log{ 6U };

  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
  EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;

  contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
  contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(true));
  insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));

  assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
  assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);

  assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
  assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);

  assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
  assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// !linearizable:
//
// Let x && y be distinct values.
//
//   contains(x) : false     contains(y) : true     contains(x) : false
// |---------------------| |--------------------| |---------------------|
//
//                             insert(x) : true
//                    |------------------------------|
static void test_016()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned not_linearizable_entry_id = 2U;

  Log<state::Set> log{ 8U };

  EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
  EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
  EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
  EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;

  call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
  call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
  call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
  ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));

  assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// !linearizable:
//
// Let x && y be distinct values.
//
//   contains(x) : false     contains(y) : true     contains(x) : false
// |---------------------| |--------------------| |---------------------|
//
//                                      insert(x) : true
//                    |-----------------------------------------------------|
static void test_017()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned not_linearizable_entry_id = 2U;

  Log<state::Set> log{ 8U };

  EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
  EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
  EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
  EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;

  call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
  call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
  call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
  ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));

  assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// !linearizable:
//
// Let x && y be distinct values.
//
//      contains(y) : true     insert(x) : true
//    |--------------------| |------------------|
//
//                insert(x) : false
// |------------------------------------------------|
static void test_018()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  constexpr unsigned not_linearizable_entry_id = 1U;

  Log<state::Set> log{ 8U };

  EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
  EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
  EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;

  call_x0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
  call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
  ret_x0_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));

  assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

// Linearizable:
//
//   insert(x) : insert_ret
// |------------------------|
//
//               contains(x) : contains_ret
//            |-----------------------------|
//
//                 empty() : empty_ret 
//             |------------------------|
static void test_019(bool insert_ret, bool contains_ret, bool empty_ret)
{
  constexpr char x = '\1';

  Log<state::Set> log{ 8U };

  EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
  EntryPtr<state::Set> call_contains_entry_ptr, ret_contains_entry_ptr;
  EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;

  call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  call_contains_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
  ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(insert_ret));
  ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(empty_ret));
  ret_contains_entry_ptr = log.add_ret(call_contains_entry_ptr, state::Set::make_ret(contains_ret));

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == insert_ret);
}

//                                                          insert(x) : insert_ret
//                                                        |------------------------|
//
//   contains(x) :  contains_ret    contains(x) : contains_ret
// |----------------------------| |----------------------------|
//
//                                                     empty() : empty_ret
//                                                   |----------------------|
static void test_020(bool insert_ret, bool contains_ret, bool empty_ret)
{
  constexpr char x = '\1';

  Log<state::Set> log{ 8U };

  EntryPtr<state::Set> call_contains_0_entry_ptr, ret_contains_0_entry_ptr;
  EntryPtr<state::Set> call_contains_1_entry_ptr, ret_contains_1_entry_ptr;
  EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
  EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;

  call_contains_0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_contains_0_entry_ptr = log.add_ret(call_contains_0_entry_ptr, state::Set::make_ret(contains_ret));
  call_contains_1_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
  call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  ret_contains_1_entry_ptr = log.add_ret(call_contains_1_entry_ptr, state::Set::make_ret(contains_ret));
  ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(empty_ret));
  ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(insert_ret));

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check() == (insert_ret && !contains_ret));
}

// Linearizable:
//
// Let x && y be distinct values.
//
//   contains(x) : false
// |---------------------|
//
//              insert(y) : true
//           |-----------------------------------------------------------|
//
//                            contains(x) : false      empty() : true
//                          |---------------------|  |----------------|
static void test_021()
{
  constexpr char x = '\1';
  constexpr char y = '\2';

  Log<state::Set> log{ 8U };

  EntryPtr<state::Set> call_contains_0_entry_ptr, ret_contains_0_entry_ptr;
  EntryPtr<state::Set> call_contains_1_entry_ptr, ret_contains_1_entry_ptr;
  EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
  EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;

  call_contains_0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(y));
  ret_contains_0_entry_ptr = log.add_ret(call_contains_0_entry_ptr, state::Set::make_ret(false));
  call_contains_1_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  ret_contains_1_entry_ptr = log.add_ret(call_contains_1_entry_ptr, state::Set::make_ret(false));
  call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
  ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(true));
  ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(1));

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(t.check());
}

// Linearizable:
//
//        push(x) : true
// |------------------------|
//
//        push(y) : true
//   |--------------------|
//
//      pop() : (true, x)
//    |------------------|
static void test_stack_history_000()
{
  constexpr char x = '\1';
  constexpr char y = '\2';
  constexpr std::size_t N = 5;

  Log<state::Stack<N>> log{ 6U };
  EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;

  try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
  try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
  try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
  try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));

  assert(!try_push_x_call_entry_ptr->is_partitionable());
  assert(!try_push_y_call_entry_ptr->is_partitionable());
  assert(!try_pop_x_call_entry_ptr->is_partitionable());

  assert(!try_push_x_ret_entry_ptr->is_partitionable());
  assert(!try_push_y_ret_entry_ptr->is_partitionable());
  assert(!try_pop_x_ret_entry_ptr->is_partitionable());

  LinearizabilityTester<state::Stack<N>> t{ log.info() };
  assert(t.check());
}

// push(x):true; push(y):true; pop():x
static void test_stack_history_001()
{
  constexpr char x = '\1';
  constexpr char y = '\2';
  constexpr std::size_t N = 5;

  Log<state::Stack<N>> log{ 6U };
  EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;

  try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
  try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
  try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
  try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));

  assert(!try_push_x_call_entry_ptr->is_partitionable());
  assert(!try_push_y_call_entry_ptr->is_partitionable());
  assert(!try_pop_x_call_entry_ptr->is_partitionable());

  assert(!try_push_x_ret_entry_ptr->is_partitionable());
  assert(!try_push_y_ret_entry_ptr->is_partitionable());
  assert(!try_pop_x_ret_entry_ptr->is_partitionable());

  LinearizabilityTester<state::Stack<N>> t{ log.info() };
  assert(!t.check());
}

// entry id: 0, thread id: 0x2, call: try_push(x)
// entry id: 0, thread id: 0x2, return: ret: 1
// entry id: 1, thread id: 0x3, call: try_push(y)
// entry id: 2, thread id: 0x4, call: try_pop()
// entry id: 2, thread id: 0x4, return: ret: [ok: 1, value: x]
// entry id: 1, thread id: 0x3, return: ret: 1
static void test_stack_history_002()
{
  constexpr char x = '\1';
  constexpr char y = '\2';
  constexpr std::size_t N = 5;

  Log<state::Stack<N>> log{ 8U };
  EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;

  try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
  try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
  try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
  try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
  try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));

  assert(!try_push_x_call_entry_ptr->is_partitionable());
  assert(!try_push_y_call_entry_ptr->is_partitionable());
  assert(!try_pop_x_call_entry_ptr->is_partitionable());

  assert(!try_push_x_ret_entry_ptr->is_partitionable());
  assert(!try_push_y_ret_entry_ptr->is_partitionable());
  assert(!try_pop_x_ret_entry_ptr->is_partitionable());

  LinearizabilityTester<state::Stack<N>> t{ log.info() };
  assert(t.check());
}

// Linearizable:
//
//   push(x) : true       pop() : (true, y)
// |----------------|   |------------------|
//
//     push(y) : true                           push(z) : true
//   |----------------|                |---------------------------------|
//
//                                                  pop() : (true, x)     pop() : (true, z)
//                                               |-------------------| |-------------------|
static void test_stack_history_003()
{
  constexpr char x = '\1';
  constexpr char y = '\2';
  constexpr char z = '\3';
  constexpr std::size_t N = 5;

  Log<state::Stack<N>> log{ 12U };
  EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_push_z_call_entry_ptr, try_push_z_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_pop_y_call_entry_ptr, try_pop_y_ret_entry_ptr;
  EntryPtr<state::Stack<N>> try_pop_z_call_entry_ptr, try_pop_z_ret_entry_ptr;

  try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
  try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
  try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_pop_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
  try_push_z_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(z));
  try_pop_y_ret_entry_ptr = log.add_ret(try_pop_y_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, y));
  try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
  try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
  try_pop_z_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
  try_push_z_ret_entry_ptr = log.add_ret(try_push_z_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
  try_pop_z_ret_entry_ptr = log.add_ret(try_pop_z_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, z));

  LinearizabilityTester<state::Stack<N>> t{ log.info() };
  assert(t.check());
}


// Let x = '\0' && y = '\1'.
//
//   erase(x) : false     insert(y) : true
// |------------------| |------------------|
//
//                                               contains(x) : true
//                                 |------------------------------------------------|
//
//                                      contains(y) : false     insert(x) : true
//                                    |---------------------| |------------------|
static void test_slice_000()
{
  constexpr char x = '\0';
  constexpr char y = '\1';

  Log<state::Set> log{ 10U };

  EntryPtr<state::Set> erase_x_call_entry_ptr, erase_x_ret_entry_ptr;
  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
  EntryPtr<state::Set> insert_y_call_entry_ptr, insert_y_ret_entry_ptr;
  EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;

  erase_x_call_entry_ptr = log.add_call(state::Set::make_erase_call(x));
  erase_x_ret_entry_ptr = log.add_ret(erase_x_call_entry_ptr, state::Set::make_ret(false));
  insert_y_call_entry_ptr = log.add_call(state::Set::make_insert_call(y));
  contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  insert_y_ret_entry_ptr = log.add_ret(insert_y_call_entry_ptr, state::Set::make_ret(true));
  contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
  insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
  insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
  contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(true));

  Slicer<state::Set> slicer{ log.info(), 2U };

  assert(slicer.sublog_info(x).log_head_ptr() == erase_x_call_entry_ptr);
  assert(slicer.sublog_info(y).log_head_ptr() == insert_y_call_entry_ptr);

  assert(slicer.sublog_info(x).number_of_entries() == 6U);
  assert(slicer.sublog_info(y).number_of_entries() == 4U);

  LinearizabilityTester<state::Set> tester_0{ slicer.sublog_info(x) };
  assert(tester_0.check());

  LinearizabilityTester<state::Set> tester_1{ slicer.sublog_info(y) };
  assert(tester_1.check());
}

// Let x = '\0' && y = '\1'.
//
//   contains(x) : false 
// |---------------------|
//
//      contains(y) : false
//    |---------------------|
//
//          insert(x) : false
//        |---------------------|
static void test_slice_001()
{
  constexpr char x = '\0';
  constexpr char y = '\1';

  Log<state::Set> log{ 6U };
  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
  EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;

  contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
  insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));

  contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
  contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
  insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));

  Slicer<state::Set> slicer{ log.info(), 2U };

  assert(slicer.sublog_info(x).log_head_ptr() == contains_x_call_entry_ptr);
  assert(slicer.sublog_info(y).log_head_ptr() == contains_y_call_entry_ptr);

  assert(slicer.sublog_info(x).number_of_entries() == 4U);
  assert(slicer.sublog_info(y).number_of_entries() == 2U);

  LinearizabilityTester<state::Set> tester_0{ slicer.sublog_info(x) };
  assert(!tester_0.check());

  LinearizabilityTester<state::Set> tester_1{ slicer.sublog_info(y) };
  assert(tester_1.check());
}

static void debug()
{
  constexpr char x = '\1';

  Log<state::Set> log{ 2U };

  EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
  contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
  contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(true));

  LinearizabilityTester<state::Set> t{ log.info() };
  Result<state::Set> result;

  t.check(result);
  assert(!result.is_linearizable());

  std::stringstream os;
  result.debug(os);

  assert(os.str() == "Linearizable: No\n"
    "entry id: 0, thread id: 0, call: contains(1)\n"
    "^ previous entries cannot be linearized\n"
    "entry id: 0, thread id: 0, return: ret: 1\n"
    "^ previous entries cannot be linearized\n");
}


static void concurrent_log()
{
  constexpr unsigned number_of_partitions = 1U;

  constexpr char x = '\0';

  ConcurrentLog<state::Set> log{ 6U };

  EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
  EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;

  contains_x_call_entry_ptr = log.push_back(state::Set::make_contains_call(x));
  insert_x_call_entry_ptr = log.push_back(state::Set::make_insert_call(x));
  contains_x_ret_entry_ptr = log.push_back(contains_x_call_entry_ptr, state::Set::make_ret(false));
  insert_x_ret_entry_ptr = log.push_back(insert_x_call_entry_ptr, state::Set::make_ret(false));

  EntryPtr<state::Set> entry_ptr, log_head_ptr{ log.log_head_ptr() };

  assert(log_head_ptr == contains_x_call_entry_ptr);
  assert(log_head_ptr->prev == nullptr);
  assert(log_head_ptr->next == insert_x_call_entry_ptr);
  assert(log_head_ptr->match() == contains_x_ret_entry_ptr);

  entry_ptr = log_head_ptr->next;
  assert(entry_ptr == insert_x_call_entry_ptr);
  assert(entry_ptr->prev == contains_x_call_entry_ptr);
  assert(entry_ptr->next == contains_x_ret_entry_ptr);
  assert(entry_ptr->match() == insert_x_ret_entry_ptr);

  entry_ptr = entry_ptr->next;
  assert(entry_ptr == contains_x_ret_entry_ptr);
  assert(entry_ptr->prev == insert_x_call_entry_ptr);
  assert(entry_ptr->next == insert_x_ret_entry_ptr);
  assert(entry_ptr->match() == contains_x_call_entry_ptr);

  entry_ptr = entry_ptr->next;
  assert(entry_ptr == insert_x_ret_entry_ptr);
  assert(entry_ptr->prev == contains_x_ret_entry_ptr);
  assert(entry_ptr->next == nullptr);
  assert(entry_ptr->match() == insert_x_call_entry_ptr);

  LinearizabilityTester<state::Set> t{ log.info() };
  assert(!t.check());
}

struct WorkerConfiguration
{
  const char max_value;
  const unsigned number_of_ops;
};

static void returns_always_false_worker(
  const WorkerConfiguration& worker_configuration,
  ConcurrentLog<state::Set>& concurrent_log)
{
  std::random_device rd;
  std::mt19937 gen(rd());
  std::uniform_int_distribution<> value_dist('\0', worker_configuration.max_value);
  std::uniform_int_distribution<> percentage_dist(0, 100);

  // each operation returns false
  constexpr bool ret = false;

  char value;
  EntryPtr<state::Set> call_entry_ptr;
  for (unsigned number_of_ops{ 0U };
  number_of_ops < worker_configuration.number_of_ops;
    ++number_of_ops)
  {
    value = value_dist(rd);
    if (percentage_dist(rd) < 30)
    {
      call_entry_ptr = concurrent_log.push_back(state::Set::make_insert_call(value));
      concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
    }
    else if (percentage_dist(rd) < 50)
    {
      call_entry_ptr = concurrent_log.push_back(state::Set::make_erase_call(value));
      concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
    }
    else
    {
      call_entry_ptr = concurrent_log.push_back(state::Set::make_contains_call(value));
      concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
    }
  }
}

template<class F, class ...Args>
void start_threads(unsigned number_of_threads, F&& f, Args&&... args)
{
  std::vector<Thread> threads(number_of_threads);

  for (Thread& thread : threads)
    thread = Thread(std::forward<F>(f), std::forward<Args>(args)...);

  for (Thread& thread : threads)
    thread.join();
}

/// The first "insert" operation should be always marked as non-linearizable.
static void fuzzy_functional_test()
{
  constexpr unsigned number_of_threads = 4U;
  constexpr WorkerConfiguration worker_configuration = { '\7', 12U };
  constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops;

  ConcurrentLog<state::Set> concurrent_log{ 2U * log_size };

  // create history
  start_threads(number_of_threads, returns_always_false_worker,
    std::cref(worker_configuration), std::ref(concurrent_log));

  LinearizabilityTester<state::Set> tester{ concurrent_log.info() };

  assert(!tester.check());
}

void run_tests(){
  test_lru_cache();
  test_atomic_op();
  test_stack();
  test_state_set();
  test_bitset();
  test_state_set_op();
  test_state_stack();
  test_state_stack_op();
  
  test_state_queue();
  test_state_queue_op();
  
  test_linearizability_empty_log();
  test_raw_single_contains_is_linearizable();
  test_raw_single_contains_is_not_linearizable();
  test_log_copy();
  test_single_contains(true);
  test_single_contains(false);

  // Consider a sequential insert(x) && contains(x) operation
  // && their return values on an initially empty set:

  for (bool a : {true, false})
  for (bool b : {true, false})
  {
  test_000(a, b);
  test_001(a, b);
  test_002(a, b);
  test_003(a, b);
  test_004(a, b);
  test_005(a, b);
  test_006(a, b);
  test_007(a, b);
  test_008(a, b);
  }

  // semantically deeper tests

  test_009();
  test_010();
  test_011();
  test_012();
  test_013();
  test_014();
  test_015();
  test_016();
  test_017();
  test_018();

  for (bool a : {true, false})
  for (bool b : {true, false})
  for (bool c : {true, false})
  {
  test_019(a, b, c);
  test_020(a, b, c);
  }

  test_021();

  test_stack_history_000();
  test_stack_history_001();
  test_stack_history_002();
  test_stack_history_003();

  test_slice_000();
  test_slice_001();

  #ifdef _LT_DEBUG_
    debug();
  #endif

  concurrent_log();
  fuzzy_functional_test();

}