/* traffic simulation:
 *
 * road A: 0 -> 1 -> 2 -> 3 -> 0
 * road B: 0 -> 1 -> 2 -> 3 -> 0
 *              
 * 1 and 3 denote positions at the crossing,
 * 0 and 2 denote open road.
 *
 * crossing layout (counterclockwise): A[1] -> B[1] -> B[3] -> A[3]
 */

bool roadA[4] = false;
bool roadB[4] = false;
bool blocked = false;

active proctype traffic()
{
  roadA[0] = true;
  roadA[1] = true;
  roadA[2] = true;
  roadA[3] = true;

  do 

  /* from open road to crossing */
  :: atomic { roadA[0] & !roadA[1] -> roadA[0] = false; roadA[1] = true; }
  :: atomic { roadA[2] & !roadA[3] -> roadA[2] = false; roadA[3] = true; }
  :: atomic { roadB[0] & !roadB[1] -> roadB[0] = false; roadB[1] = true; }
  :: atomic { roadB[2] & !roadB[3] -> roadB[2] = false; roadB[3] = true; }

  /* A[1] enters the crossing */
  :: atomic { roadA[1] & !roadB[1] && !roadA[0] -> roadA[1] = false; roadA[0] = true; }
  :: atomic { roadA[1] & !roadB[1] && !roadA[2] -> roadA[1] = false; roadA[2] = true; }
  :: atomic { roadA[1] & !roadB[1] && !roadB[2] -> roadA[1] = false; roadB[2] = true; }

  /* B[1] enters the crossing */
  :: atomic { roadB[1] & !roadB[3] && !roadB[0] -> roadB[1] = false; roadB[0] = true; }
  :: atomic { roadB[1] & !roadB[3] && !roadB[2] -> roadB[1] = false; roadB[2] = true; }
  :: atomic { roadB[1] & !roadB[3] && !roadA[2] -> roadB[1] = false; roadA[2] = true; }

  /* B[3] enters the crossing */
  :: atomic { roadB[3] & !roadA[3] && !roadB[0] -> roadB[3] = false; roadB[0] = true; }
  :: atomic { roadB[3] & !roadA[3] && !roadB[2] -> roadB[3] = false; roadB[2] = true; }
  :: atomic { roadB[3] & !roadA[3] && !roadA[0] -> roadB[3] = false; roadA[0] = true; }

  /* A[3] enters the crossing */
  :: atomic { roadA[3] & !roadA[1] &&  !roadA[0] -> roadA[3] = false; roadA[0] = true; }
  :: atomic { roadA[3] & !roadA[1] &&  !roadA[2] -> roadA[3] = false; roadA[2] = true; }
  :: atomic { roadA[3] & !roadA[1] &&  !roadB[0] -> roadA[3] = false; roadB[0] = true; }

  :: else -> break;
  od;
  
  blocked = true;
}