//----------------------------
// D2 Model - Feb 24 2001
// Mohsen D. Ghassemi, Viktor Kuncak, Darko Marinov, Mandana Vaziri
//----------------------------
 

sig State {
     currentDB, lastDB, nextDB: Database,
     mode: Mode,
     trialID: option FlightID,
     trial: option Flight,
     trialConflicts: option Conflicts
}



// There are two modes of operation in D2:
// - trial-planning mode; the controller tries different D2 trajectories, and
// - "default" mode; D2 calculates only one D2 trajectory for each flight

sig Mode {}

sig trial extends Mode {}

sig default extends Mode {}

fact TwoModes {
     partition trial, default: Mode
}


sig Database {
     flights: FlightID ->? Flight,
     conflicts: Conflicts,
     d2List: set FlightID
}

sig Flight {
     plan: option FlightPlan,
     track: option Track,
     trajectory: option Trajectory,
     d2Fix: option Fix,
     d2Plan: option Plan,
     d2Trajectory: option Trajectory
}


sig FlightID {}


// We represent `FlightPlan' abstractly, not as a sequence of `Fix'es.

sig FlightPlan {}



sig Fix {}



// We represent `Trajectory' abstractly, not as a sequence of `Track's.

sig Trajectory {}

sig Track {}


sig Conflicts {
     conflictPairs: FlightID -> FlightID,
     d2ConflictPairs: FlightID -> FlightID,
     greyed: set FlightID
}



// Messages that come to D2 from the rest of CTAS (CM)

sig MsgFlightPlan {
     flightID: FlightID,
     plan: FlightPlan
}



sig MsgFlightID {
     flightID: FlightID
}

 
sig MsgTracks {
     track: FlightID ->? Track
}

 
// Messages from D2 to TS

sig MsgSynthesizeTrajectory {
     plan: FlightPlan,
     track: Track
}

 
// Messsages from D2 to CP

sig MsgConflictProbe {
     t1, t2: Trajectory
}



// Messages that come to D2 from the GUI

sig MsgAccept {}

sig MsgReject {}


// Messages from D2 to GUI

sig MsgUpdateGUI {
     db: Database,
     trialID: option FlightID
}

 

////////////////////////////////////////////////////////////////
// Message receival

 

fun addFlightPlan(pre, post: State, msg: MsgFlightPlan) {
     some f = msg.flightID {
           no (pre.nextDB.flights)[f]
           (post.nextDB.flights)[f].plan = msg.plan
           // Reset all the fields except `plan' for the received flight
           // so that old values don't get mixed with the new ones.

           each field: Flight - plan | no (post.nextDB.flights)[f].field
           // frame condition

           each field: State - nextDB.flights | post.field = pre.field
           all ff: FlightID - f |
                 (post.nextDB.flights)[ff] = (pre.nextDB.flights)[ff]
     }
}

 

fun deleteFlightPlan(pre, post: State, msg: MsgFlight) {
     some f = msg.flightID {
           no (post.nextDB.flights)[f]
           // frame condition
           each field: State - nextDB.flights | post.field = pre.field
           all ff: FlightID - f | (post.nextDB.flights)[ff] = (pre.nextDB.flights)[ff]
     }
}

 

fun amendFlightPlan(pre, post: State, msg: MsgFlightPlan) {
     some f = msg.flightID {
           some (pre.nextDB.flights)[f]
           (post.nextDB.flights)[f].plan = msg.plan
           post.currentDB.conflicts.greyed = pre.currentDB.conflicts.greyed + f
           // frame condition
           each field: State - currentDB - nextDB | post.field = pre.field
           each field: Database - conflicts.greyed | post.currentDB.field = pre.currentDB.field
           each field: Database - flights | post.nextDB.field = pre.nextDB.field
           each field: Flight - plan | (post.nextDB.flights)[f].field = (pre.nextDB.flights)[f].field
           all ff: FlightID - f | (post.nextDB.flights)[ff] = (pre.nextDB.flights)[ff]
     }
}

 
fun updateTracks(pre, post: State, msg: MsgTracks) {
     all f: FlightID | some (msg.track)[f] -> (post.nextDB.flights)[f].track = (msg.track)[f]
     // frame condition
     each field: State - nextDB.flights | post.field = pre.field
     all f: FlightID | each field: Flight - track | (post.nextDB.flights)[f].field = (pre.nextDB.flights)[f].field
     all f: FlightID | no (msg.track)[f] -> (post.nextDB.flights)[f].track = (pre.nextDB.flights)[f].track
}

 

////////////////////////////////////////////////////////////////
// Periodic timer

 

fun incorporate(pre, post: State) {
     // move current database to last
     post.lastDB = pre.currentDB
     // move next database to current
     post.currentDB = pre.nextDB
     pre.mode = trial -> post.trial.track = (pre.nextDB.flights)[pre.trialID].track
     pre.mode = default -> post.trial.track = pre.trial.track
     changedGUI(post)
     // frame condition
     each field: State - lastDB - currentDB - trial.track | post.field = pre.field
}

 

////////////////////////////////////////////////////////////////

// Computation

// determine `d2Fix' based on the type of the flight; we model the
// actual determination as being completely non-deterministic

fun determineD2Fix(i: Flight) {
     one i.d2Fix
}



// compute `d2Plan' based on the actual `plan' and `d2Fix'

fun computeD2Plan(i: Flight) {
     one i.d2Plan
}

 

fun computeD2Fixes(pre, post: State) {
     all f: FlightID | some (pre.currentDB.flights)[f].plan ->
                                         determineD2Fix((post.currentDB.flights)[f]) and
                                         computeD2Plan((post.currentDB.flights)[f])
     // frame condition
     each field: State - currentDB.flights | post.field = pre.field
     all f: FlightID | some (pre.currentDB.flights)[f].plan ->
                                         each field: Flight - d2Fix - d2Plan |
                                               (post.currentDB.flights)[f].field =
                                               (pre.currentDB.flights)[f].field
     all f: FlightID | no (pre.currentDB.flights)[f].plan -> (post.currentDB.flights)[f].d2Fix = (pre.currentDB.flights)[f].d2Fix
}

 

// synthesize trajectory based on the `track', `plan', and aircraft type;
// we model trajectory synthesis as being completely non-deterministic

fun synthesizeTrajectory(m: MsgSynthesizeTrajectory): Trajectory {}


fun computeTrajectories(pre, post: State) {
     all f: FlightID | some (pre.currentDB.flights)[f].plan -> {
                                               some m: MsgSynthesizeTrajectory {
                                                     m.track = (post.currentDB.flights)[f].track
                                                     m.plan = (post.currentDB.flights)[f].plan
                                                     (post.currentDB.flights)[f].trajectory = synthesizeTrajectory(m)
                                               }
                                               some m: MsgSynthesizeTrajectory {
                                                     m.track = (post.currentDB.flights)[f].track
                                                     m.plan = (post.currentDB.flights)[f].d2Plan
                                                     (post.currentDB.flights)[f].d2Trajectory = synthesizeTrajectory(m)
                                               }
     // frame condition
     each field: State - currentDB.flights | post.field = pre.field
     all f: FlightID | some (pre.currentDB.flights)[f].plan ->
                                         each field: Flight - trajectory - d2trajectory |
                                               (post.currentDB.flights)[f].field = (pre.currentDB.flights)[f].field
     all f: FlightID | no (pre.currentDB.flights)[f].plan -> (post.currentDB.flights)[f] = (pre.currentDB.flights)[f]
}

 

// decide if `d2Trajectory' is significantly shorter than regular `trajectory'
// we model this completely non-deterministic

fun betterEnough(d2Trajectory, trajectory: Trajectory) {}
 

fun computeD2List(pre, post: State) {
     all f: FlightID | f in post.currentDB.d2List <->
         betterEnough((pre.currentDB.flights)[f].d2Trajectory,
               (pre.currentDB.flights)[f].trajectory)
     // frame condition
     each field: State - currentDB.d2List | post.field = pre.field
}

 
// predict if there is a conflict between two trajectories;
// we model conflict prediction as being completely non-deterministic

fun predictConflicts(m: MsgConflictProbe) {}
 

fun computeConflictPairs(pre, post: State) {
     all f1, f2: FlightID |
     some i1 = (post.currentDB.flights)[f1], i2 = (post.currentDB.flights)[f2] {
           f1->f2 in post.currentDB.conflicts.conflictPairs <->
           some m: MsgConflictProbe {
                 m.t1 = i1.trajectory
                 m.t2 = i2.trajectory
                 predictConflict(m)
           }
           and
           f1->f2 in post.currentDB.conflicts.d2ConflictPairs <->
           some m: MsgConflictProbe {
                 m.t1 = i1.d2Trajectory
                 m.t2 = i2.trajectory
                 predictConflict(m)
           }
     }
     // frame condition
     each field: State - currentDB.conflicts.conflictPairs - currentDB.conflicts.d2ConflictPairs | post.field = pre.field
}

 

////////////////////////////////////////////////////////////////
// Initialization

fun Conflicts::init() {
     with this {
           no conflictPairs
           no d2ConflictPairs
           no greyed
     }
}

 

fun Database::init() {
     with this {
           all f: FlightID | no flights[f]
           conflicts.init()
           no d2List
     }
}

 

fun initialState():State {
     with result {
         currentDB.init()
         lastDB.init()
         nextDB.init()
         mode = default
         no trial
         no trialID
         no trialConflicts
     }
}

 

////////////////////////////////////////////////////////////////

// Trial-planning mode

 

fun Trial::init(i: Flight) {
     with this {
           plan = i.d2Plan
           track = i.track
           trajectory = i.d2Trajectory
           d2Fix = i.d2Fix
           d2Plan = i.d2Plan
           d2Trajectory = i.d2Trajectory
     }
}

 

fun enterTrialPlanning(pre, post: State, msg: MsgFlight) {
     pre.mode = default
     post.mode = trial
     some db: Database {
           (db = pre.lastDB or db = pre.currentDB)
           some f = msg.flightID {
                 post.trialID = f
                 (post.trial).init((db.flights)[f])
                 with post.trialConflicts {
                       all f1, f2: FlightID {
                             f1->f2 in conflictPairs <->
                             f1 != f and f2 != f and f1->f2 in db.conflicts.conflictPairs
                       }                            
                       d2ConflictPairs = db.conflicts.d2ConflictPairs
                       greyed = db.conflicts.greyed - f
                 }
           }
     }
     changedGUI(post)
     // frame condition
     each field: State - mode - trialID - trial - trialConflicts | post.field = pre.field
}

 

fun acceptTrialPlan(pre, post: State, msg: MsgAccept) {
     pre.mode = trial
     post.mode = default
     some m: MsgFlightPlan {
           m.flightID = pre.trialID
           m.plan = pre.trial.plan
           requestAmendement(m)
     }
     changedGUI(post)
     // frame condition
     each field: State - mode | post.field = pre.field
}

 

fun rejectTrialPlan(pre, post: State, msg: MsgReject) {
     pre.mode = trial
     post.mode = default
     no trialID
     no trial
     no trialConflicts
     changedGUI(post)
     // frame condition
     each field: State - mode - trialID - trial - trialConflicts | post.field = pre.field
}

 

fun trialPredictConflict(f: FlightID) {
     some db: Database {
           (db = pre.lastDB or db = pre.currentDB)
           some m: MsgConflictProbe {
                 m.t1 = post.trial.trajectory
                 m.t2 = (pre.db.flights)[f].trajectory
                 predictConflict(m)
           }
     }
}

 

fun changeTrialPlan(pre, post: State, msg: MsgFlightPlan) {
     pre.mode = trial
     some f = pre.trialID {
           f = msg.flightID
           post.trial.plan = msg.plan
           some m: MsgSynthesizeTrajectory {
                 m.track = (post.trial)[f].track
                 m.plan = (post.trial)[f].plan
                 (post.trial)[f].trajectory = synthesizeTrajectory(m)
           }
           all f1, f2: FlightID {
                 f1->f2 in post.trialConflicts.conflictPairs <->
                 (f1 != f and f2 != f and f1->f2 in pre.trialConflicts.conflictPairs)
                 or
                 (f1 = f and f2 != f and trialPredictConflict(f2))
                 or
                 (f1 != f and f2 = f and trialPredictConflict(f1))
           }
     }
     changedGUI(post)
     // frame condition
     each field: State - trial.plan - trail.trajectory - trialConflicts | post.field = pre.field
     each field: Conflicts - conflictPairs | post.trialConflicts.field = pre.trialConflicts.field
}

 
////////////////////////////////////////////////////////////////
// Messages that D2 sends to back to the rest of CTAS


fun requestAmendement(m: MsgFlightPlan) {}



////////////////////////////////////////////////////////////////
// Messages that D2 sends to GUI to tell it what to show

fun updateGUI(m: MsgUpdateGUI) {}


fun changedGUI(s: State) {
     some m: MsgUpdateGUI {
           s.mode = trial -> {
                 (m.db.flights)[s.trialID] = s.trial
                 all f: FlightID - s.trialID | (m.db.flights)[f] = (s.lastDB.flights)[f]
                 m.db.conflicts = s.trialConflicts
                 each field: Database - flights - conflicts | m.db.field = s.lastDB.field
                 m.trialID = s.trialID
           }
           s.mode = default -> {
                 m.db = lastDB
                 no m.trialID
           }
           updateGUI(m)
     }
}