model ATC {

      domain {fixed Sector, fixed Track, fixed Flight}

      state {
            active: Sector! -> Flight
            tooCloseTo: static Track -> static Track
            trajectory: Flight -> Track+
            currentTrack: Flight? -> Track!
            firstTrack: Flight? -> static Track!
            nextTrack[Flight]: Track? -> Track?
            conflict: Flight -> Flight
      }

      inv {
            all f: Flight | f.firstTrack.*nextTrack[f] = f.trajectory

            all f1, f2: Flight | f1 in f2.conflict -> f2 in f1.conflict

            all f1, f2: Flight | f1 in f2.conflict <->
            some t1, t2: Track |
                  (f1!= f2 && t1 in f1.trajectory && t2 in f2.trajectory &&
                        (t1 in t2.tooCloseTo || t2 in t1.tooCloseTo))
      }

      op moveFlight(f: Flight!) {
            all f1: Flight | f.currentTrack' = f.currentTrack.nextTrack[f]
      }

      op amendTrajectory(f: Flight!, t: Track+) {
            f.trajectory' = t
            all f1: Flight | f.firstTrack.*nextTrack[f] = t
      }

      op conflictProbe {
            all f1, f2: Flight | f1 in f2.conflict' <->
            some t1, t2: Track |
                  (f1!= f2 && t1 in f1.currentTrack.*nextTrack[f1] &&
                   t2 in f2.currentTrack.*nextTrack[f2] &&
                        (t1 in t2.tooCloseTo || t2 in t1.tooCloseTo))
      }

      op handoff(f: Flight, fromSect: Sector!, toSect: Sector!) {
            fromSect != toSect
            fromSect.active' = fromSect.active - f
            toSect.active' = toSect.active + f
      }

      assert activeFlights {
            all f, s1, s2 | handoff(f, s1,s2) -> one f.~active
      }

}