Skip to content

Airport Simulation

Suppose we have been tasked with writing a program that simulates a runway at an airport. This airport is very small, so it only has one runway, which is used for both takeoffs and landings. We want to verify that the runway is always used safely, by checking the following informal specification:

  1. The runway has two modes: departure mode and arrival mode. The two modes can never be active at the same time. Neither mode is active at the beginning of the day.

  1. At any given moment, there is a waiting list of planes that need to land at the airport and planes that need to leave the airport. These are modeled with counters W_A for the number of planes waiting to arrive, and W_D for the number of planes waiting to depart.

  2. At any moment, a plane is either waiting to arrive, waiting to depart, or on the runway. Once a plane has started arriving or departing, the corresponding counter (W_A or W_D) is decremented. There is no need to keep track of planes once they have arrived or departed. Additionally, once a plane is waiting to arrive or depart, it continues waiting until it has arrived or departed.

  3. It takes 5 minutes for a plane to arrive or depart. During these 5 minutes, no other plane may use the runway. We can keep track of how long a plane has been on the runway with the Runway_Counter. If the Runway_Counter is at 0, then there is currently no plane using the runway, and it is clear for another plane to begin arriving or departing. Once the Runway_Counter reaches 5, we can reset it at the next clock tick. One clock tick represents 1 minute.

  4. If there is at least one plane waiting to depart and no cars waiting to arrive, then the runway is set to departure mode (and vice versa for arrivals).

  5. If both modes of the runway are inactive and planes become ready to depart and arrive simultaneously, the runway will activate arrival mode first. If the runway is in arrival mode and there are planes waiting to depart, no more than 3 planes may arrive from that time point. When either no more planes are waiting to arrive or 3 planes have arrived, the runway switches to departure mode. If the runway is on arrival mode and no planes are waiting to depart, then the runway may stay in arrival mode until a plane is ready to depart, from which time the 3-plane limit is imposed (and vice versa for departures). Put simply, if any planes are waiting for a mode that is inactive, that mode will become active no more than 15 minutes later (5 minutes for each of 3 planes).

To encode all this in CN, we first need a way to describe the state of the runway at a given time. We can use a struct that includes the following fields:

  • ModeA and ModeD to represent the arrival and departure modes, respectively. We can define constants for ACTIVE and INACTIVE, as described in the Constants section above.

  • W_A and W_D to represent the number of planes waiting to arrive and depart, respectively.

  • Runway_Time to represent the time (in minutes) that a plane has spent on the runway while arriving or departing.

  • Plane_Counter to represent the number of planes that have arrived or departed while planes are waiting for the other mode. This will help us keep track of the 3-plane limit as described in (6).

exercises/runway/state.h
#define INACTIVE 0
    /*@ function (i32) INACTIVE () @*/
    static int c_INACTIVE() /*@ cn_function INACTIVE; @*/ { return INACTIVE; }

#define ACTIVE 1
    /*@ function (i32) ACTIVE () @*/
    static int c_ACTIVE() /*@ cn_function ACTIVE; @*/ { return ACTIVE; }

struct State {
  int ModeA;
  int ModeD;

  int W_A;
  int W_D;

  int Runway_Time;
  int Plane_Counter;
};

Next, we need to specify what makes a state valid. We must define a rigorous specification in order to ensure that the runway is always safe and working as intended. Try thinking about what this might look like before looking at the code below.

exercises/runway/valid_state.h
/*@
function (boolean) valid_state (struct State s) {
     (s.ModeA == INACTIVE() || s.ModeA == ACTIVE()) &&
     (s.ModeD == INACTIVE() || s.ModeD == ACTIVE()) &&
     (s.ModeA == INACTIVE() || s.ModeD == INACTIVE()) &&

     (s.W_A >= 0i32 && s.W_D >= 0i32) &&
     (0i32 <= s.Runway_Time && s.Runway_Time <= 5i32) && 
     (0i32 <= s.Plane_Counter && s.Plane_Counter <= 3i32) && 

     (s.ModeA == INACTIVE() && s.ModeD == INACTIVE() 
        implies s.Plane_Counter == 0i32) &&
     (s.Runway_Time > 0i32 
        implies (s.ModeA == ACTIVE() || s.ModeD == ACTIVE())) &&

     (s.Plane_Counter > 0i32 && s.ModeA == ACTIVE() implies s.W_D > 0i32) &&
     (s.Plane_Counter > 0i32 && s.ModeD == ACTIVE() implies s.W_A > 0i32)
}
@*/

Let's walk through the specifications in valid_state:

  • The first two lines ensure that both modes in our model behave as intended: they can only be active or inactive. Any other value for these fields would be invalid.

  • The third line says that either arrival mode or departure mode must be inactive. This specification ensures that the runway is never in both modes at the same time.

  • The fourth line says that the number of planes waiting to arrive or depart must be non-negative. This makes sense: we can't have a negative number of planes!

  • The fifth line ensures that the runway time is between 0 and 5. This addresses how a plane takes 5 minutes on the runway as described in (4).

  • The sixth line ensures that the plane counter is between 0 and 3. This is important for the 3-plane limit as described in (6).

  • The seventh line refers to the state at the beginning of the day. If both modes are inactive, then the day has just begun, and thus no planes have departed yet. This is why the plane counter must be 0.

  • The eighth line says that if there is a plane on the runway, then one of the modes must be active. This is because a plane can only be on the runway if it is either arriving or departing.

  • The final two lines ensure that we are incrementing Plane_Counter only if there are planes waiting for the other mode, as described in (6).

Now that we have the tools to reason about the state of the runway formally, let's start writing some functions.

First, let's look at an initialization function and functions to update Plane_Counter. Step through these yourself and make sure you understand the reasoning behind each specification.

exercises/runway/funcs1.h
struct State init()
/*@ requires true;
    ensures valid_state(return);
@*/
{
    struct State initial = {INACTIVE,INACTIVE,0,0,0,0};
    return initial;
}

struct State increment_Plane_Counter(struct State s)
/*@ requires valid_state(s);
             0i32 <= s.Plane_Counter;
             s.Plane_Counter <= 2i32;
             s.ModeA == ACTIVE() || s.ModeD == ACTIVE();
             s.ModeA == ACTIVE() implies s.W_D > 0i32;
             s.ModeD == ACTIVE() implies s.W_A > 0i32;
    ensures  valid_state(return);
             s.Plane_Counter == return.Plane_Counter - 1i32;
             s.Runway_Time == return.Runway_Time;
             s.ModeA == return.ModeA;
             s.ModeD == return.ModeD;
             s.W_A == return.W_A;
             s.W_D == return.W_D;
@*/
{
  struct State temp = s;
  temp.Plane_Counter = s.Plane_Counter + 1;
  return temp;
}

struct State reset_Plane_Counter(struct State s)
/*@ requires valid_state(s);
    ensures  valid_state(return);
             return.Plane_Counter == 0i32;
             s.Runway_Time == return.Runway_Time;
             s.ModeA == return.ModeA;
             s.ModeD == return.ModeD;
             s.W_A == return.W_A;
             s.W_D == return.W_D;
@*/
{
  struct State temp = s;
  temp.Plane_Counter = 0;
  return temp;
}

Exercise: Now try adding your own specifications to the following functions. Make sure that you specify a valid state as a pre- and post-condition for every function. If you get stuck, the solution is in the solutions folder.

exercises/runway/funcs2.c
#include "state.h"
#include "valid_state.h"
#include "funcs1.h"

struct State increment_Runway_Time(struct State s)
{
  struct State temp = s;
  temp.Runway_Time = s.Runway_Time + 1;
  return temp;
}

struct State reset_Runway_Time(struct State s)
{
  struct State temp = s;
  temp.Runway_Time = 0;
  return temp;
}

struct State arrive(struct State s)
{
  struct State temp = s;
  temp.W_A = s.W_A - 1;
  if (s.W_D > 0) {
    temp = increment_Plane_Counter(temp);
  }
  return temp;
}

struct State depart(struct State s)
{
  struct State temp = s;
  temp.W_D = s.W_D - 1;
  if (s.W_A > 0) {
    temp = increment_Plane_Counter(temp);
  }
  return temp;
}

struct State switch_modes(struct State s) 
{
  struct State temp = s;
  if (s.ModeA == INACTIVE) {
    // if arrival mode is inactive, make it active
    temp.ModeA = ACTIVE;
  } else {
    // if arrival mode is active, make it inactive
    temp.ModeA = INACTIVE;
  }
  if (s.ModeD == INACTIVE) {
    // if departure mode is inactive, make it active
    temp.ModeD = ACTIVE;
  } else {
    // if departure mode is active, make it inactive
    temp.ModeD = INACTIVE;
  }
  return temp;
}

// This function represents what happens every minute at the airport. 
// One `tick` corresponds to one minute.
struct State tick(struct State s)
{
    // Plane on the runway
    if (s.Runway_Time > 0)
    {
      if (s.Runway_Time == 5)
      {
        s = reset_Runway_Time(s);
      } else {
        s = increment_Runway_Time(s);
      }
      return s;
    }
    // Plane chosen to arrive
    else if (s.ModeA == ACTIVE && s.W_A > 0 && s.Plane_Counter < 3) {
      s = arrive(s);
      s = increment_Runway_Time(s);
      return s;
    } 
    // Plane chosen to depart
    else if (s.ModeD == ACTIVE && s.W_D > 0 && s.Plane_Counter < 3) {
      s = depart(s);
      s = increment_Runway_Time(s);
      return s;
    }
    // Need to switch modes
    else {
      // Need to switch from arrival to departure mode
      if (s.ModeA == ACTIVE) {
        s = reset_Plane_Counter(s);
        s = switch_modes(s);
        // If there are planes waiting to depart, let one depart
        if (s.W_D > 0) {
          s = depart(s);
          s = increment_Runway_Time(s);
        }
        return s;
      }
      // Need to switch from departure to arrival mode
      else if (s.ModeD == ACTIVE) {
        s = reset_Plane_Counter(s);
        s = switch_modes(s);

        // If there are planes waiting to arrive, let one arrive
        if (s.W_A > 0) {
          s = arrive(s);
          s = increment_Runway_Time(s);
        }
        return s;
      }
      // If neither mode is active, then it must be the beginning of the day.
      else {
        if (s.W_A > 0) {
          s.ModeA = ACTIVE;
          s = arrive(s);
          s = increment_Runway_Time(s);
          return s;
        } else if (s.W_D > 0) {
          s.ModeD = ACTIVE;
          s = depart(s);
          s = increment_Runway_Time(s);
          return s;
        } else {
          // No planes are waiting, so we choose arrival mode and wait
          s.ModeA = ACTIVE;
          return s;
        }
      }
    }
}

Acknowledgment of Support and Disclaimer

This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google. The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).