#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); } }