bool Fail = false;
int shared = 6;
int x = 0;
int y = 0;
bool z = true;

chan q_0_1 = [0] of {bit};
chan q_0_2 = [0] of {bit};




proctype A() {
bool can_change_shared = true;
do
  ::atomic{
    z ->
    x = 10;
    };
  ::atomic{
    can_change_shared ->
    q_0_1?0;
    shared = shared+1;
    can_change_shared = false;
    q_0_1?1;
    };
  ::atomic{
    !can_change_shared ->
    q_0_2?0;
    can_change_shared = true;
    q_0_2?1;
    };
od;
}

proctype B() {
bool can_change_shared = false;
do
  ::atomic{
    z ->
    y = 11;
    };
  ::atomic{
    can_change_shared ->
    q_0_2!0;
    shared = shared-1;
    can_change_shared = false;
    q_0_2!1;
    };
  ::atomic{
    !can_change_shared ->
    q_0_1!0;
    can_change_shared = true;
    q_0_1!1;
    };
od;
}

init {
 atomic{
 run A();
 run B();
 };
}