/* traffic simulation:
 *
 *               +----------------------+
 *               |                      |
 *               |    ..............    |
 *               |    .   >B[2]>   .    |
 *               |    .    +--+    .    |
 *               | v  .    |  |    . ^  |
 *  +------------+A[3]     +--+    .A[2]|
 *  |              v      <B[3]<   . ^  |
 *  |    ........           ........    |
 *  | v  .   >A[1]>     ^               |
 *  |B[0].    +--+     B[1]+------------+
 *  | v  .    |  |    . ^  |
 *  |    .    +--+    .    |
 *  |    .   <A[0]<   .    |
 *  |    ..............    |
 *  |                      |
 *  +----------------------+
 *
 */

#include "predicates"

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;
}