int lk, r_want, r_lock, sleep_q;
enum { Wakeme, Running } State;

void _before()
{
  lk = r_want = r_lock = sleep_q = 0;
  State = Running;
}

void _hash(unsigned int *h)
{
  _hash_int(lk, h);
  _hash_int(r_want, h);
  _hash_int(r_lock, h);
  _hash_int(sleep_q, h);
  _hash_int(State, h);
}

void _print(char *tmp)
{
  sprintf(tmp, "   lk = %i\n", lk);
  sprintf(&tmp[strlen(tmp)], "   r_want = %i\n", r_want);
  sprintf(&tmp[strlen(tmp)], "   r_lock = %i\n", r_lock);
  sprintf(&tmp[strlen(tmp)], "   sleep_q = %i\n", sleep_q);

  State == Wakeme ?
    sprintf(&tmp[strlen(tmp)], "   State = Wakeme\n") :
    sprintf(&tmp[strlen(tmp)], "   State = Running\n");
}

%%

c3;   (lk == 0);          {lk = 1;};                      c11;
c5;   -;                  {r_want = 1;};                  c6;
c6;   (sleep_q == 0);     {sleep_q = 1;};                 c8;
c8;   -;                  {lk = 0;};                      c9;
c9;   -;                  {State = Wakeme;};              c10;
c10;  -;                  {sleep_q = 0;};                 c12;
c11;  (r_lock == 1);      -;                              c5;
c11;  (r_lock == 0);      -;                              c14;
c12;  (State == Running); -;                              c3;
c14;  (r_lock == 0);      #progress;                      c15;
c14;  (r_lock == 1);      #progress,_c14_assert_violated; c15;
c15;  -;                  {r_lock = 1;};                  c16;
c16;  -;                  {lk = 0;};                      c3;

c14_assert_ok;
_c14_assert_violated;

s1;  -;                 {r_lock = 0;};      s2;
s2;  (lk == 0);         -;                  s15;
s5;  -;                 {r_want = 0;};      s6;
s6;  (lk == 0);         -;                  s7;
s7;  (sleep_q == 0);    {sleep_q = 1;};     s11;
s9;  -;                 {State = Running;}; s13;
s11; (State == Wakeme); -;                  s9;
s11; (State != Wakeme); -;                  s13;
s13; -;                 {sleep_q = 0;};     s1;
s15; (r_want == 1);     -;                  s5;
s15; (r_want != 1);     -;                  s1;

no_progress;
#progress; -; -; no_progress;