module RailroadCrossing {
  var train_state: integer;
  var controller_state: integer;
  var gate_state: bv1;

  next {
    if (train_state == 0) {
      if (controller_state == 0) {
        controller_state' = 1;
        train_state' = 1;
      }
    } else {
      if (train_state == 1) {
        if (controller_state == 2) {
          controller_state' = 3;
          train_state' = 2;
        }
      } else {
        if (train_state == 2) {
          if (controller_state == 0) {
            controller_state' = 1;
            train_state' = 1;
          }
        }
      }
    }
    if (controller_state == 1) {
      if (train_state == 1) {
        gate_state' = 1bv1;
        controller_state' = 2;
      }
    } else {
      if (controller_state == 2) {
        if (train_state == 2) {
          gate_state' = 0bv1;
          controller_state' = 3;
        }
      } else {
        if (controller_state == 3) {
          if (gate_state == 0bv1) {
            controller_state' = 0;
          }
        }
      }
    }

  }
}
