#include "../PLASMA/NDDL/core/Plasma.nddl"
#include "../PLASMA/NDDL/core/PlannerConfig.nddl"



// Global variables

int CPU_BOOT_DUR =              360;
int CPU_SHUTDOWN_DUR =          540;
int HGA_PRE_XMIT =              420;
int UHF_PRE_XMIT =              480;
int COMM_POST_XMIT =            240;

float STATE_COND_TRUE =      1000.0;
float STATE_COND_FALSE =    -1000.0;


/**
 * @brief Control of passive/active enforcement
 */

class Control extends Object {
  bool      Enable_Passive_Checking;
  bool      Enforce_IDD_Claim;
  bool      Enforce_PMA_Claim;
  bool      Enforce_Mobility_Claim;
  bool      Enforce_Comm_Claim;
  bool      Enforce_Mobility_PMA_MUTEX;
  bool      Enforce_Mobility_HZ_MUTEX;
  bool      Enforce_Mobility_Comm_MUTEX;
  bool      Enforce_Mobility_IDD_MUTEX;
  bool      Enforce_UHF_PMA_MUTEX;
  bool      Enforce_UHF_IDD_MUTEX;
  bool      Enforce_IPS_MT_MUTEX;
  bool      Enforce_IPS_IDD_MUTEX;
  bool      Enforce_GFA_IDD_MUTEX;
  bool      Enforce_GFA_HGA_MUTEX;
  bool      Enforce_RAT_PMA_MUTEX;

  Control() {}



/**
 * @brief initial conditions - need to add energy and data later
 */
  predicate incon {
    bool    idd_stowed;
    eq(duration, 1);
  }

}

Control::incon {
  if (idd_stowed == true) {
    IDD_Stowed is0;
    starts(is0.change c5);
    eq(c5.quantity, STATE_COND_TRUE);
  }
  if (idd_stowed == false) {
    IDD_Unstowed iu0;
    starts(iu0.change c6);
    eq(c6.quantity, STATE_COND_TRUE);
  }
}



/**
 * @brief model for Instrument Positioning System
 */

class IPS extends Object {

  IPS() {}

  predicate APXS_START {
    int          dur;
    int          priority;
    eq(duration, dur);
      }

  predicate APXS_ACQ {
    int          dur;
    int          priority;
    eq(duration, dur);
      }

  predicate APXS_OFF {
    int          dur;
    int          priority;
    eq(duration, dur);
        }

  predicate MB_START {
    int           dur;
    int          priority;
    eq(duration, dur);
      }

  predicate MB_ACQ {
    int           dur;
    int          priority;
    eq(duration, dur);
      }

  predicate MB_OFF {
    int           dur;
    int          priority;
    eq(duration, dur);
  }

  predicate MI {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

  predicate RAT {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

  predicate IDD_MOVE {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

  predicate IDD_STOW {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

  predicate IDD_UNSTOW {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

}

IPS::APXS_START {
  Control c0;
  // Flight Rule Passive Checking

  if (c0.Enable_Passive_Checking) {
    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

    // flight rule: rover must be stationary
    //  contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);


    // flight rule: need CPU in avail state
    //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr4);
    eq(fr4.quantity, -1.0);
    ends(ca0.change fr5);
    eq(fr5.quantity, 1.0);

  // flight rule: cannot start APXS while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr6);
    eq(fr6.quantity, -1.0);
    ends(ui0.change fr7);
    eq(fr7.quantity, 1.0);
  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Disallow IDD actuation during IPS activities
  if (c0.Enforce_IPS_IDD_MUTEX == true) {
    Active_IPS_IDD aii;
    equals(aii.IPS_IDD_MUTEX mx8);
    neq(mx8.state, MERGED);
  }
  // Flight Rule: connot use miniTES while starting or stopping APXS or MB
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: cannot start or stop APXS/MB during UHF 
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }

}


IPS::APXS_ACQ {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

  // flight rule: rover must be stationary
  //  contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  }
  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Disallow IDD actuation during IPS activities
  if (c0.Enforce_IPS_IDD_MUTEX == true) {
    Active_IPS_IDD aii;
    equals(aii.IPS_IDD_MUTEX mx8);
    neq(mx8.state, MERGED);
  }

}

IPS::APXS_OFF {
  Control c0;

  // Flight Rule Passive Checking

  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

    // flight rule: rover must be stationary
    //  contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr4);
    eq(fr4.quantity, -1.0);
    ends(ca0.change fr5);
    eq(fr5.quantity, 1.0);

  // flight rule: cannot stop and readout APXS while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr6);
    eq(fr6.quantity, -1.0);
    ends(ui0.change fr7);
    eq(fr7.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Disallow IDD actuation during IPS activities
  if (c0.Enforce_IPS_IDD_MUTEX == true) {
    Active_IPS_IDD aii;
    equals(aii.IPS_IDD_MUTEX mx8);
    neq(mx8.state, MERGED);
  }
  // Flight Rule: connot use miniTES while starting or stopping APXS or MB
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: cannot start or stop APXS/MB during UHF 
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }

}


IPS::MB_ACQ {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

    // flight rule: rover must be stationary
    // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Disallow IDD actuation during IPS activities
  if (c0.Enforce_IPS_IDD_MUTEX == true) {
    Active_IPS_IDD aii;
    equals(aii.IPS_IDD_MUTEX mx8);
    neq(mx8.state, MERGED);
  }

}

IPS::MB_START {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

    // flight rule: rover must be stationary
    // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr4);
    eq(fr4.quantity, -1.0);
    ends(ca0.change fr5);
    eq(fr5.quantity, 1.0);

  // flight rule: cannot start MB while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr6);
    eq(fr6.quantity, -1.0);
    ends(ui0.change fr7);
    eq(fr7.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Disallow IDD actuation during IPS activities
  if (c0.Enforce_IPS_IDD_MUTEX == true) {
    Active_IPS_IDD aii;
    equals(aii.IPS_IDD_MUTEX mx8);
    neq(mx8.state, MERGED);
  }
  // Flight Rule: connot use miniTES while starting or stopping APXS or MB
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: cannot start or stop APXS/MB during UHF 
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }

}

IPS::MB_OFF {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

    // flight rule: rover must be stationary
    // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr4);
    eq(fr4.quantity, -1.0);
    ends(ca0.change fr5);
    eq(fr5.quantity, 1.0);

  // flight rule: cannot stop and readout MB while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr6);
    eq(fr6.quantity, -1.0);
    ends(ui0.change fr7);
    eq(fr7.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Flight Rule: connot use miniTES while starting or stopping APXS or MB
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: cannot start or stop APXS/MB during UHF 
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }
}

IPS::MI {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);
    
  // flight rule: cannot use MI while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ui0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ms0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ca0.change fr6);
    eq(fr6.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Flight Rule: do not move IDD during MTES
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: should not be using any actuators during GET_FINE_ATTITUDE 
  if (c0.Enforce_GFA_IDD_MUTEX == true) {
    Active_GFA_IDD agi;
    equals(agi.GFA_IDD_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
  // Disallow IDD actuation while moving rover
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Disallow IDD actuation during UHF
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }

}

IPS::RAT {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

    RAT_Idle ri0;
    starts(ri0.change c4);
    eq(STATE_COND_FALSE, c4.quantity);
    ends(ri0.change c5);
    eq(c5.quantity, STATE_COND_TRUE);

  // flight rule: cannot use RAT while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ui0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ms0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ca0.change fr6);
    eq(fr6.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Flight Rule: cannot use Pancams while RAT is in use
  if (c0.Enforce_RAT_PMA_MUTEX == true) {
    Active_RAT_PMA arp;
    equals(arp.RAT_PMA_MUTEX mx3);
    neq(mx3.state, MERGED);
  }

  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Flight Rule: cannot perform UHF Comm while RAT is in use
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }
  // Disallow IDD actuation during IPS activities
  if (c0.Enforce_IPS_IDD_MUTEX == true) {
    Active_IPS_IDD aii;
    equals(aii.IPS_IDD_MUTEX mx8);
    neq(mx8.state, MERGED);
  }

}

IPS::IDD_MOVE {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

  // equals(IDDuse.Active ia);
  // not equal IDDuse.Idle

    IDD_Idle ii0;
    starts(ii0.change c2);
    eq(STATE_COND_FALSE, c2.quantity);
    ends(ii0.change c3);
    eq(c3.quantity, STATE_COND_TRUE);

  // flight rule: rover must be stationary
  //  contained_by(MobilityState.Stationary rs);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: cannot move IDD while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ui0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: IDD must be unstowed to move it
  // contained_by(IDDstate.Unstowed iu);

    IDD_Unstowed iu0;
    starts(iu0.change f7);
    eq(f7.quantity, -1.0);
    ends(iu0.change f8);
    eq(f8.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr9);
    eq(fr9.quantity, -1.0);
    ends(ca0.change fr10);
    eq(fr10.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Flight Rule: do not move IDD during MTES
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: should not be using any actuators during GET_FINE_ATTITUDE 
  if (c0.Enforce_GFA_IDD_MUTEX == true) {
    Active_GFA_IDD agi;
    equals(agi.GFA_IDD_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
  // Disallow IDD actuation while moving rover
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Disallow IDD actuation during UHF
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }

}

IPS::IDD_STOW {
  Control c0;

  // Flight Rule Passive Checking  
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

  // equals(IDDuse.Active ia);
  // not equal IDDuse.Idle

    IDD_Idle ii0;
    starts(ii0.change c2);
    eq(STATE_COND_FALSE, c2.quantity);
    ends(ii0.change c3);
    eq(c3.quantity, STATE_COND_TRUE);

  // contained_by(IDDState::Unstowed u);
  // meets(IDDState::Stowed s);

    IDD_Stowed is0;
    ends(is0.change c5);
    eq(c5.quantity, STATE_COND_TRUE);
    IDD_Unstowed iu0;
    starts(iu0.change c6);
    eq(c6.quantity, -1.0);
    ends(iu0.change c8);
    sum(c8.quantity, STATE_COND_FALSE, 1.0);

  // flight rule: cannot move IDD while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ui0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ms0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ca0.change fr6);
    eq(fr6.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Flight Rule: do not move IDD during MTES
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: should not be using any actuators during GET_FINE_ATTITUDE 
  if (c0.Enforce_GFA_IDD_MUTEX == true) {
    Active_GFA_IDD agi;
    equals(agi.GFA_IDD_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
  // Disallow IDD actuation during UHF
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }

}

IPS::IDD_UNSTOW {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    IDD_Claim ic0;
    starts(ic0.change tx);
    eq(tx.quantity, -1.0);
    ends(ic0.change ty);
    eq(ty.quantity, 1.0);

  // equals(IDDuse.Active ia);
  // not equal IDDuse.Idle

    IDD_Idle ii0;
    starts(ii0.change c2);
    eq(STATE_COND_FALSE, c2.quantity);
    ends(ii0.change c3);
    eq(c3.quantity, STATE_COND_TRUE);

  // contained_by(IDDState::Stowed u);
  // meets(IDDState::Unstowed s);

    IDD_Unstowed iu0;
    ends(iu0.change c5);
    eq(c5.quantity, STATE_COND_TRUE);
    IDD_Stowed is0;
    starts(is0.change c6);
    eq(c6.quantity, -1.0);
    ends(is0.change c8);
    sum(c8.quantity, STATE_COND_FALSE, 1.0);

  // flight rule: cannot move IDD while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ui0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ms0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ca0.change fr6);
    eq(fr6.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_IDD_Claim == true) {
    Active_IDD_Claim aic;
    equals(aic.IDD_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Flight Rule: do not move IDD during MTES
  if (c0.Enforce_IPS_MT_MUTEX == true) {
    Active_IPS_MT aim;
    equals(aim.IPS_MT_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Flight Rule: should not be using any actuators during GET_FINE_ATTITUDE 
  if (c0.Enforce_GFA_IDD_MUTEX == true) {
    Active_GFA_IDD agi;
    equals(agi.GFA_IDD_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
  // Disallow IDD actuation while moving rover
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }
  // Disallow IDD actuation during UHF
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx6);
    neq(mx6.state, MERGED);
  }

}



/**
 * @brief model for PanCam Mast Assembly
 */

class PMA extends Object {

  PMA() {}

  predicate PANCAM_MOSAIC {
    int      dur;
    int          priority;
    eq(duration, dur);
  }

  predicate PANCAM_SINGLE_POSITION {
    int      dur;
    int          priority;
    eq(duration, dur);
  }

  predicate NAVCAM_MOSAIC {
    int      dur;
    int          priority;
    eq(duration, dur);
  }

  predicate NAVCAM_SINGLE_POSITION {
    int      dur;
    int          priority;
    eq(duration, dur);
  }

  predicate MTES_8_MRAD {
    int      dur;
    int          priority;
    eq(duration, dur);
  }

  predicate MTES_20_MRAD {
    int      dur;
    int          priority;
    eq(duration, dur);
  }

  predicate GET_FINE_ATTITUDE {
    int      dur;
    int          priority;
    eq(duration, dur);
  }

}


PMA::PANCAM_MOSAIC {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    PMA_Claim pc0;
    starts(pc0.change tx);
    eq(tx.quantity, -1.0);
    ends(pc0.change ty);
    eq(ty.quantity, 1.0);

    Numof_Imaging ni0;
    starts(ni0.change ic1);
    eq(ic1.quantity, -1.0);
    ends(ni0.change ic2);
    eq(ic2.quantity, 1.0);

  // flight rule: cannot use Pancams while IDD is active
  // contained_by(IDDuse.Idle ii);

    IDD_Idle ii0;
    starts(ii0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ii0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: cannot use Pancams while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ui0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary  ms0;
    starts(ms0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ms0.change fr6);
    eq(fr6.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr7);
    eq(fr7.quantity, -1.0);
    ends(ca0.change fr8);
    eq(fr8.quantity, 1.0);

    RAT_Idle ri0;
    starts(ri0.change fr9);
    eq(fr9.quantity, -1.0);
    ends(ri0.change fr10);
    eq(fr10.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_PMA_Claim == true) {
    Active_PMA_Claim apc;
    equals(apc.PMA_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_PMA_MUTEX == true) {
    Active_Mobility_PMA amp;
    equals(amp.Mobility_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }
  // Flight Rule: cannot use Pancams while RAT is in use
  if (c0.Enforce_RAT_PMA_MUTEX == true) {
    Active_RAT_PMA arp;
    equals(arp.RAT_PMA_MUTEX mx3);
    neq(mx3.state, MERGED);
  }

}

PMA::PANCAM_SINGLE_POSITION {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    PMA_Claim pc0;
    starts(pc0.change tx);
    eq(tx.quantity, -1.0);
    ends(pc0.change ty);
    eq(ty.quantity, 1.0);

    Numof_Imaging ni0;
    starts(ni0.change ic1);
    eq(ic1.quantity, -1.0);
    ends(ni0.change ic2);
    eq(ic2.quantity, 1.0);

  // flight rule: cannot use Pancams while IDD is active
  // contained_by(IDDuse.Idle ii);

    IDD_Idle ii0;
    starts(ii0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ii0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: cannot use Pancams while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ui0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary  ms0;
    starts(ms0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ms0.change fr6);
    eq(fr6.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr7);
    eq(fr7.quantity, -1.0);
    ends(ca0.change fr8);
    eq(fr8.quantity, 1.0);

    RAT_Idle ri0;
    starts(ri0.change fr9);
    eq(fr9.quantity, -1.0);
    ends(ri0.change fr10);
    eq(fr10.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_PMA_Claim == true) {
    Active_PMA_Claim apc;
    equals(apc.PMA_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_PMA_MUTEX == true) {
    Active_Mobility_PMA amp;
    equals(amp.Mobility_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }
  // Flight Rule: cannot use Pancams while RAT is in use
  if (c0.Enforce_RAT_PMA_MUTEX == true) {
    Active_RAT_PMA arp;
    equals(arp.RAT_PMA_MUTEX mx3);
    neq(mx3.state, MERGED);
  }

}


PMA::NAVCAM_MOSAIC {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    PMA_Claim pc0;
    starts(pc0.change tx);
    eq(tx.quantity, -1.0);
    ends(pc0.change ty);
    eq(ty.quantity, 1.0);

    Numof_Imaging ni0;
    starts(ni0.change ic1);
    eq(ic1.quantity, -1.0);
    ends(ni0.change ic2);
    eq(ic2.quantity, 1.0);

  // flight rule: cannot use Navcams while IDD is active
  //contained_by(IDDuse.Idle ii);

    IDD_Idle ii0;
    starts(ii0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ii0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: cannot use Navcams while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ui0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ms0.change fr6);
    eq(fr6.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr7);
    eq(fr7.quantity, -1.0);
    ends(ca0.change fr8);
    eq(fr8.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_PMA_Claim == true) {
    Active_PMA_Claim apc;
    equals(apc.PMA_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_PMA_MUTEX == true) {
    Active_Mobility_PMA amp;
    equals(amp.Mobility_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }

}

PMA::NAVCAM_SINGLE_POSITION {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {
  
    PMA_Claim pc0;
    starts(pc0.change tx);
    eq(tx.quantity, -1.0);
    ends(pc0.change ty);
    eq(ty.quantity, 1.0);

    Numof_Imaging ni0;
    starts(ni0.change ic1);
    eq(ic1.quantity, -1.0);
    ends(ni0.change ic2);
    eq(ic2.quantity, 1.0);

  // flight rule: cannot use Navcams while IDD is active
  //contained_by(IDDuse.Idle ii);

    IDD_Idle ii0;
    starts(ii0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ii0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: cannot use Navcams while UHF is in use
  //  contained_by(UHFuse.Idle i);

    UHF_Idle ui0;
    starts(ui0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ui0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ms0.change fr6);
    eq(fr6.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr7);
    eq(fr7.quantity, -1.0);
    ends(ca0.change fr8);
    eq(fr8.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_PMA_Claim == true) {
    Active_PMA_Claim apc;
    equals(apc.PMA_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_PMA_MUTEX == true) {
    Active_Mobility_PMA amp;
    equals(amp.Mobility_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }

}


PMA::MTES_8_MRAD {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {
  
    PMA_Claim pc0;
    starts(pc0.change tx);
    eq(tx.quantity, -1.0);
    ends(pc0.change ty);
    eq(ty.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ca0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: cannot use MTES while IDD is active
  //  contained_by(IDDuse.Idle ii);

    IDD_Idle ii0;
    starts(ii0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ii0.change fr6);
    eq(fr6.quantity, 1.0);

    RAT_Idle ri0;
    starts(ri0.change fr9);
    eq(fr9.quantity, -1.0);
    ends(ri0.change fr10);
    eq(fr10.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_PMA_Claim == true) {
    Active_PMA_Claim apc;
    equals(apc.PMA_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_PMA_MUTEX == true) {
    Active_Mobility_PMA amp;
    equals(amp.Mobility_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }
  // Flight Rule: cannot use MiniTES while RAT is in use
  if (c0.Enforce_RAT_PMA_MUTEX == true) {
    Active_RAT_PMA arp;
    equals(arp.RAT_PMA_MUTEX mx3);
    neq(mx3.state, MERGED);
  }

}


PMA::MTES_20_MRAD {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    PMA_Claim pc0;
    starts(pc0.change tx);
    eq(tx.quantity, -1.0);
    ends(pc0.change ty);
    eq(ty.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ca0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: cannot use MTES while IDD is active
  //  contained_by(IDDuse.Idle ii);

    IDD_Idle ii0;
    starts(ii0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ii0.change fr6);
    eq(fr6.quantity, 1.0);

    RAT_Idle ri0;
    starts(ri0.change fr9);
    eq(fr9.quantity, -1.0);
    ends(ri0.change fr10);
    eq(fr10.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_PMA_Claim == true) {
    Active_PMA_Claim apc;
    equals(apc.PMA_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_PMA_MUTEX == true) {
    Active_Mobility_PMA amp;
    equals(amp.Mobility_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }
  // Flight Rule: cannot use MiniTES while RAT is in use
  if (c0.Enforce_RAT_PMA_MUTEX == true) {
    Active_RAT_PMA arp;
    equals(arp.RAT_PMA_MUTEX mx3);
    neq(mx3.state, MERGED);
  }

}


PMA::GET_FINE_ATTITUDE {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    PMA_Claim pc0;
    starts(pc0.change tx);
    eq(tx.quantity, -1.0);
    ends(pc0.change ty);
    eq(ty.quantity, 1.0);

    Numof_Imaging ni0;
    starts(ni0.change ic1);
    eq(ic1.quantity, -1.0);
    ends(ni0.change ic2);
    eq(ic2.quantity, 1.0);

  // IDD and IPS instruments cannot be used during get fine attitude

    IDD_Idle ii0;
    starts(ii0.change c1);
    eq(c1.quantity, -1.0);
    ends(ii0.change c2);
    eq(c2.quantity, 1.0);

    RAT_Idle ri0;
    starts(ri0.change fr9);
    eq(fr9.quantity, -1.0);
    ends(ri0.change fr10);
    eq(fr10.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

 // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ca0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: cannot use HGA during this operation
  // contained_by(HGAuse.Idle hi);

    HGA_Idle hi0;
    starts(hi0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(hi0.change fr6);
    eq(fr6.quantity, 1.0);

  // flight rule: cannot use Pancams while UHF is in use
  //  contained_by(UHFuse.Idle ui);

    UHF_Idle ui0;
    starts(ui0.change fr7);
    eq(fr7.quantity, -1.0);
    ends(ui0.change fr8);
    eq(fr8.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_PMA_Claim == true) {
    Active_PMA_Claim apc;
    equals(apc.PMA_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  // Flight Rule: cannot use Pancams or Navcams while UHF is in use
  if (c0.Enforce_UHF_PMA_MUTEX == true) {
    Active_UHF_PMA aup;
    equals(aup.UHF_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }
  // Flight Rule: cannot use Pancams while RAT is in use
  if (c0.Enforce_RAT_PMA_MUTEX == true) {
    Active_RAT_PMA arp;
    equals(arp.RAT_PMA_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  // Prevents moving HGA while acquiring fine attitude knowledge
  if (c0.Enforce_GFA_HGA_MUTEX == true) {
    Active_GFA_HGA agh;
    equals(agh.GFA_HGA_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
  // Flight Rule: should not be using any actuators during GET_FINE_ATTITUDE 
  if (c0.Enforce_GFA_IDD_MUTEX == true) {
    Active_GFA_IDD agi;
    equals(agi.GFA_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }

}



/**
 * @brief model for Mobility system
 */

class Mobility extends Object {

  Mobility() {}

  predicate ROVER_ROLL {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

  predicate HAZCAM_FRONT {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

  predicate HAZCAM_REAR {
    int        dur;
    int          priority;
    eq(duration, dur);
  }

}

Mobility::ROVER_ROLL {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    Mobility_Claim mc0;
    starts(mc0.change tx);
    eq(tx.quantity, -1.0);
    ends(mc0.change ty);
    eq(ty.quantity, 1.0);

  // equals(MobilityState.Driving dr);
  // not equal MobilityState.Stationary

    Mobility_Stationary ms0;
    starts(ms0.change c2);
    eq(STATE_COND_FALSE, c2.quantity);
    ends(ms0.change c3);
    eq(c3.quantity, STATE_COND_TRUE);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ca0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule: IDD must be stowed to drive
  // contained_by(IDDState::Stowed u);

    IDD_Stowed is0;
    starts(is0.change f7);
    eq(f7.quantity, -1.0);
    ends(is0.change f8);
    eq(f8.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_Mobility_Claim == true) {
    Active_Mobility_Claim amc;
    equals(amc.Mobility_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_PMA_MUTEX == true) {
    Active_Mobility_PMA amp;
    equals(amp.Mobility_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }
  if (c0.Enforce_Mobility_HZ_MUTEX == true) {
    Active_Mobility_HZ amh;
    equals(amh.Mobility_HZ_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  if (c0.Enforce_Mobility_Comm_MUTEX == true) {
    Active_Mobility_Comm amc;
    equals(amc.Mobility_Comm_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
  if (c0.Enforce_Mobility_IDD_MUTEX == true) {
    Active_Mobility_IDD ami;
    equals(ami.Mobility_IDD_MUTEX mx5);
    neq(mx5.state, MERGED);
  }

}

    
Mobility::HAZCAM_FRONT {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    Numof_Imaging ni0;
    starts(ni0.change ic1);
    eq(ic1.quantity, -1.0);
    ends(ni0.change ic2);
    eq(ic2.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);
    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ca0.change fr4);
    eq(fr4.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_Mobility_HZ_MUTEX == true) {
    Active_Mobility_HZ amh;
    equals(amh.Mobility_HZ_MUTEX mx3);
    neq(mx3.state, MERGED);
  }

}

Mobility::HAZCAM_REAR {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    Numof_Imaging ni0;
    starts(ni0.change ic1);
    eq(ic1.quantity, -1.0);
    ends(ni0.change ic2);
    eq(ic2.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ca0.change fr4);
    eq(fr4.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_Mobility_HZ_MUTEX == true) {
    Active_Mobility_HZ amh;
    equals(amh.Mobility_HZ_MUTEX mx3);
    neq(mx3.state, MERGED);
  }

}



/**
 * @brief model for Communications System
 *
 * Note that the comm activities have start_time as a parameter
 * because the planner is not allowed to determine (or change) start
 * hence, there can be no flexibility in the start of comm activities
 **/

class Comm extends Object {

  Comm() {}

  predicate X_COMM_HGA {
    int        dur;
    int          priority;
    eq(duration, dur);
  }
  predicate UHF_COMM {
    int        dur;
    int          priority;
    eq(duration, dur);
  }
}

Comm::X_COMM_HGA {
  Control c0;

  // Flight Rule Passive Checking
  
  // flight rule on non-overlapping comms only appies to setup and
  // transmit phases, it does not apply to the cleanup phase
  if (c0.Enable_Passive_Checking) {

    Comm_Claim cc0;
    starts(cc0.change c1);
    eq(c1.quantity, -1.0);
    
    any(cc0.change c2);
    temporaldistance(c2.time, COMM_POST_XMIT, end);
    eq(c2.quantity, 1.0);


  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr1);
    eq(fr1.quantity, -1.0);
    ends(ms0.change fr2);
    eq(fr2.quantity, 1.0);

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr3);
    eq(fr3.quantity, -1.0);
    ends(ca0.change fr4);
    eq(fr4.quantity, 1.0);

  // flight rule on mutual exclusion with HGA only appies to setup and
  // transmit phases, it does not apply to the cleanup phase
  //  contains(HGAuse.Active a);

    HGA_Idle hi0;
    starts(hi0.change fr5);
    eq(fr5.quantity, STATE_COND_FALSE);  
    any(hi0.change fr6);
    temporaldistance(fr6.time, COMM_POST_XMIT, end);  
    eq(fr6.quantity, STATE_COND_TRUE); 
  }


  // Flight Rule Active Enforcement

  if (c0.Enforce_Comm_Claim == true) {
    Active_Comm_Claim acc;
    equals(acc.Comm_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_Mobility_Comm_MUTEX == true) {
    Active_Mobility_Comm amc;
    equals(amc.Mobility_Comm_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
  // Prevents moving HGA while acquiring fine attitude knowledge
  if (c0.Enforce_GFA_HGA_MUTEX == true) {
    Active_GFA_HGA agh;
    equals(agh.GFA_HGA_MUTEX mx4);
    neq(mx4.state, MERGED);
  }

}


Comm::UHF_COMM {
  Control c0;

  // Flight Rule Passive Checking
  
  // flight rule on non-overlapping comms only appies to setup and
  // transmit phases, it does not apply to the cleanup phase
  if (c0.Enable_Passive_Checking) {

    Comm_Claim cc0;
    starts(cc0.change c1);
    eq(c1.quantity, -1.0);

    any(cc0.change c2);
    temporaldistance(c2.time, COMM_POST_XMIT, end);
    eq(c2.quantity, 1.0);

  // flight rule on mutual exclusion with UHF only appies to setup and
  // transmit phases, it does not apply to the cleanup phase
  //  contains(UHFuse.Active a);

    UHF_Idle ui0;
    starts(ui0.change fr2);
    eq(fr2.quantity, STATE_COND_FALSE);  
    any(ui0.change fr4);
    temporaldistance(fr4.time, COMM_POST_XMIT, end);  
    eq(fr4.quantity, STATE_COND_TRUE); 

  // flight rule: need CPU in avail state
  //  contained_by(CPUstate.Avail av);

    CPU_Avail ca0;
    starts(ca0.change fr5);
    eq(fr5.quantity, -1.0);
    ends(ca0.change fr6);
    eq(fr6.quantity, 1.0);

  // flight rule: rover must be stationary
  // contained_by(MobilityState.Stationary ms);

    Mobility_Stationary ms0;
    starts(ms0.change fr7);
    eq(fr7.quantity, -1.0);
    ends(ms0.change fr8);
    eq(fr8.quantity, 1.0);

  }

  // Flight Rule Active Enforcement

  if (c0.Enforce_Comm_Claim == true) {
    Active_Comm_Claim acc;
    equals(acc.Comm_Claimed mx1);
    neq(mx1.state, MERGED);
  }
  if (c0.Enforce_UHF_PMA_MUTEX == true) {
    Active_UHF_PMA aup;
    equals(aup.UHF_PMA_MUTEX mx2);
    neq(mx2.state, MERGED);
  }
  if (c0.Enforce_UHF_IDD_MUTEX == true) {
    Active_UHF_IDD aui;
    equals(aui.UHF_IDD_MUTEX mx3);
    neq(mx3.state, MERGED);
  }
  if (c0.Enforce_Mobility_Comm_MUTEX == true) {
    Active_Mobility_Comm amc;
    equals(amc.Mobility_Comm_MUTEX mx4);
    neq(mx4.state, MERGED);
  }
}

/**
 * @brief model for CPU
 * for now, not including the DEEP_SLEEP
 **/


class CPU extends Timeline {
  CPU() {}

  predicate CPU_ON {
    int        dur;
    int          priority;
    eq(duration, dur);
  }
}


CPU::CPU_ON {
  Control c0;

  // Flight Rule Passive Checking
  if (c0.Enable_Passive_Checking) {

    CPU_Avail ca0;
    any(ca0.change tx);
    temporaldistance(start, CPU_BOOT_DUR, tx.time);
    eq(tx.quantity, STATE_COND_TRUE); 

    CPU_NotAvail cn0;
    any(cn0.change fr2);
    temporaldistance(start, CPU_BOOT_DUR, fr2.time);
    eq(fr2.quantity, STATE_COND_FALSE); 

    any(ca0.change fr4);
    temporaldistance(fr4.time, CPU_SHUTDOWN_DUR, end);
    eq(fr4.quantity, STATE_COND_FALSE); 

    any(cn0.change fr3);
    temporaldistance(fr3.time, CPU_SHUTDOWN_DUR, end);
    eq(fr3.quantity, STATE_COND_TRUE);
  }

}



/**
 * @brief Claims and Mutual Exclusions
 */


class Active_PMA_Claim extends Timeline {
  Active_PMA_Claim() {}

  predicate PMA_Claimed {}
}

class Active_IDD_Claim extends Timeline {
  Active_IDD_Claim() {}

  predicate IDD_Claimed {}
}

class Active_Mobility_Claim extends Timeline {
  Active_Mobility_Claim() {}

  predicate Mobility_Claimed {}
}

class Active_Comm_Claim extends Timeline {
  Active_Comm_Claim() {}

  predicate Comm_Claimed {}

}


class Active_Mobility_PMA extends Timeline {
  Active_Mobility_PMA() {}

  predicate Mobility_PMA_MUTEX {}
}

class Active_Mobility_HZ extends Timeline {
  Active_Mobility_HZ() {}

  predicate Mobility_HZ_MUTEX {}
}

class Active_Mobility_Comm extends Timeline {
  Active_Mobility_Comm() {}

  predicate Mobility_Comm_MUTEX {}
}

class Active_Mobility_IDD extends Timeline {
  Active_Mobility_IDD() {}

  predicate Mobility_IDD_MUTEX {}
}


class Active_UHF_PMA extends Timeline {
  Active_UHF_PMA() {}

  predicate UHF_PMA_MUTEX {}
}

class Active_UHF_IDD extends Timeline {
  Active_UHF_IDD() {}

  predicate UHF_IDD_MUTEX {}
}

class Active_RAT_PMA extends Timeline {
  Active_RAT_PMA() {}

  predicate RAT_PMA_MUTEX {}
}

class Active_IPS_MT extends Timeline {
  Active_IPS_MT() {}

  predicate IPS_MT_MUTEX {}
}

class Active_IPS_IDD extends Timeline {
  Active_IPS_IDD() {}

  predicate IPS_IDD_MUTEX {}
}

class Active_GFA_IDD extends Timeline {
  Active_GFA_IDD() {}

  predicate GFA_IDD_MUTEX {}
}

class Active_GFA_HGA extends Timeline {
  Active_GFA_HGA() {}

  predicate GFA_HGA_MUTEX {}
}



/**
 * @brief Unit Capacity Resources
 */


class Unit_Capacity_Resource extends Resource {
  Unit_Capacity_Resource(float initCap) {
    super(initCap, 0.0, 10.0, +inf, +inf, -inf, -inf);
  }
}

class PMA_Claim extends Unit_Capacity_Resource {
  PMA_Claim(float initCap) {
    super(initCap);
  }
}

class IDD_Claim extends Unit_Capacity_Resource {
  IDD_Claim(float initCap) {
    super(initCap);
  }
}

class Mobility_Claim extends Unit_Capacity_Resource {
  Mobility_Claim(float initCap) {
    super(initCap);
  }
}

// there can be no overlap between comm sessions
class Comm_Claim extends Unit_Capacity_Resource {
  Comm_Claim(float initCap) {
    super(initCap);
  }
}


/**
 * @brief State Condition resources
 */


class State_Condition extends Resource {

  State_Condition(float initCap) {
    super(initCap, 0.0, +inf, +inf, +inf, -inf, -inf);
  }
}


// CPU needed flight rule
class CPU_Avail extends State_Condition {
  CPU_Avail(float initCap) {
    super(initCap);
  }
}

class CPU_NotAvail extends State_Condition {
  CPU_Avail(float initCap) {
    super(initCap);
  }
}


// IDD stowed and unstowed flight rules
class IDD_Stowed extends State_Condition {
  IDD_Stowed(float initCap) {
    super(initCap);
  }
}

class IDD_Unstowed extends State_Condition {
  IDD_Unstowed(float initCap) {
    super(initCap);
  }
}


// mutual exclusions with IDD actuation
//  class IDD_Active extends State_Condition {
//    IDD_Active(float initCap) {
//      super(initCap);
//    }
//  }

class IDD_Idle extends State_Condition {
  IDD_Idle(float initCap) {
    super(initCap);
  }
}

// mutual exclusions with driving
class Mobility_Stationary extends State_Condition {
  Mobility_Stationary(float initCap) {
    super(initCap);
  }
}


class UHF_Idle extends State_Condition {
  UHF_Idle(float initCap) {
    super(initCap);
  }
}

class HGA_Idle extends State_Condition {
  HGA_Idle(float initCap) {
    super(initCap);
  }
}

class RAT_Idle extends State_Condition {
  RAT_Idle(float initCap) {
    super(initCap);
  }
}



/**
 * @brief numeric resources
 */


// maximum overlap in imaging is up to the TUL
class Numof_Imaging extends Resource {
  Numof_Imaging(float initCap, float llmax) {
    super(initCap, 0.0, llmax, +inf, +inf, -inf, -inf);
  }
}