bool v = 0;
bool r = 0;
bool a = 0;

bool x = 0;
bool y = 0;

active proctype S()
{
  do :: true ->
    if
    :: true -> x = 1;
    :: true -> x = 2;
    fi;
    v = x;
    r = 1;

    if :: a == 1 -> skip; fi;
    r = 0;

    if :: a == 0 -> skip; fi;
  od;
}

active proctype R()
{
  do :: true ->
    if :: r == 1 -> skip; fi;
    y = x;
    a = 1;

    if :: r == 0 -> skip; fi;
    a = 0;
  od;
}