GomX-3.modest

/*****************************************************************************************************************************************************
    Input data for the model was changed in minutes to prevent state-space explosions
    
    Description: 
    This data was generated by the convertdata.py Python script that can be found in the folder ../data/
    Arrays set to transient arrays to prevent unnecessary expansion of the total state space
    One global clock used for the X- and L-Band jobs instead of 4 local clocks as the jobs are executed separately anyways so no clock interference
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
clock clk, job_clk;

transient int(0 .. 4320)[] L_Band_Inmarsat_3F2_data = [89, 182, 187, 280, 283, 375, 378, 471, 474, 567, 572, 665, 673, 766, 774, 867, 871, 964, 967, 1060, 1063, 1156, 1159, 1251, 1256, 1349, 1356, 1449, 1458, 1550, 1556, 1649, 1652, 1745, 1748, 1841, 1843, 1936, 1940, 2033, 2040, 2133, 2141, 2234, 2241, 2333, 2337, 2430, 2433, 2526, 2528, 2621, 2625, 2717, 2723, 2816, 2825, 2918, 2925, 3018, 3022, 3115, 3118, 3211, 3213, 3306, 3309, 3402, 3407, 3500, 3508, 3601, 3609, 3702, 3707, 3800, 0];
transient int(0 .. 4320)[] L_Band_Inmarsat_3F3_data = [45, 138, 142, 235, 238, 331, 333, 426, 429, 522, 528, 621, 629, 722, 729, 822, 827, 920, 923, 1016, 1018, 1111, 1114, 1207, 1212, 1305, 1313, 1406, 1414, 1506, 1512, 1604, 1608, 1701, 1703, 1796, 1799, 1892, 1896, 1989, 1996, 2089, 2098, 2190, 2196, 2289, 2293, 2385, 2388, 2481, 2484, 2577, 2580, 2673, 2680, 2773, 2781, 2874, 2881, 2973, 2977, 3070, 3073, 3166, 3168, 3261, 3265, 3358, 3363, 3456, 3465, 3558, 3565, 3658, 3662, 3755, 3758, 3851, 0];
transient int(0 .. 4320)[] Sun_data                 = [19, 77, 111, 169, 203, 261, 294, 352, 386, 444, 478, 536, 570, 628, 661, 719, 753, 811, 845, 903, 937, 995, 1028, 1087, 1120, 1178, 1212, 1270, 1303, 1362, 1395, 1454, 1487, 1545, 1579, 1637, 1670, 1729, 1762, 1821, 1854, 1913, 1946, 2004, 2037, 2096, 2129, 2188, 2221, 2280, 2313, 2372, 2404, 2463, 2496, 2555, 2588, 2647, 2680, 2739, 2771, 2831, 2863, 2922, 2955, 3014, 3047, 3106, 3138, 3198, 3230, 3289, 3322, 3381, 3413, 3473, 3505, 3565, 3597, 3657, 3689, 3748, 3780, 3840, 3872, 3932, 0];
transient int(0 .. 4320)[] UHF_data                 = [1015, 1019, 1107, 1116, 1201, 1211, 1296, 1306, 1392, 1400, 1489, 1492, 2481, 2489, 2575, 2584, 2670, 2680, 2765, 2774, 2861, 2868, 0];
transient int(0 .. 4320)[] X_Band_Kourou_data       = [399, 408, 496, 502, 1089, 1096, 1183, 1192, 1773, 1781, 1867, 1877, 2556, 2566, 2653, 2659, 3240, 3250, 3339, 3343, 0];
transient int(0 .. 4320)[] X_Band_Toulouse_data     = [114, 123, 1010, 1017, 1103, 1113, 1199, 1209, 1296, 1305, 1391, 1401, 1487, 1497, 1584, 1589, 2477, 2486, 2572, 2582, 2668, 2678, 2765, 2774, 2860, 2870, 2956, 2964, 0];

//The following sizes are the maximum array index sizes plus an artificial '0' to prevent array out of bounds after last job execution so (0 .. *_data_size)
const int L_Band_Inmarsat_3F2_data_size = 75;
const int L_Band_Inmarsat_3F3_data_size = 77;
const int Sun_data_size                 = 85;
const int UHF_data_size                 = 21;
const int X_Band_Kourou_data_size       = 19;
const int X_Band_Toulouse_data_size     = 27;

/*****************************************************************************************************************************************************
    Constants
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
//Time constants in minutes:
const int L_slew_preheat        = 40;
const int X_slew_preheat        = 20;
const int slewing               = 10;

//Battery constants:
const int Bat_cap               = 149760000;    //mJ
const int SoC_lb                = 59904000;     //40% SoC in mJ

//Power consumption constants in mJ/s * 60 seconds (mj/min):
const int Background_Power      = 2989 * 60;    // 179340 mJ/min
const int L_Power               = 3863 * 60;    // 231780 mJ/min
const int X_Power               = 11945 * 60;   // 716700 mJ/min
const int UHF_Power             = 2630 * 60;    // 157800 mJ/min
const int Slew_Preheat_Power    = 414 * 60;     // 24840  mJ/min

//Power generation constants in mJ/s * 60 seconds (mJ/min):
const int X_PV_Power            = 5700 * 60;    // 342000 mJ/min
const int L_PV_Power            = 6100 * 60;    // 366000 mJ/min

//Maximum load constant in mJ/s * 60 seconds (mJ/min)
const int maxload               = 20000 * 60;   // 1200000 mJ/min

//Cost-reward constants:
const int maxReward             = 1000;
const int minReward             = 10; 

//Scheduling interval in minutes
const int sched_interval        = 600;

//End time of schedule in minutes
const int end                   = 2160;

/*****************************************************************************************************************************************************
    Globals
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
int(-maxload .. maxload) load   = Background_Power;   //Electrical load in mW (mJ/s), which is at least 2989 since this is the background load
int(0 .. Bat_cap) SoC           = 119808000;          //80% SoC in mJ
int(0 .. 4320) last_a_time      = 0;                  //Time of last action executed
int(0 .. 4320) current_a_time   = 0;                  //Time of current action executed

//Job iteration counters limited to max data array index + 1. 
int(0 .. L_Band_Inmarsat_3F2_data_size+1) L_3F2_i   = 0;
int(0 .. L_Band_Inmarsat_3F3_data_size+1) L_3F3_i   = 0;
int(0 .. Sun_data_size+1) Sun_i                     = 0;
int(0 .. UHF_data_size+1) UHF_i                     = 0;
int(0 .. X_Band_Kourou_data_size+1) X_Kourou_i      = 0;
int(0 .. X_Band_Toulouse_data_size+1) X_Toulouse_i  = 0;
int(0 .. 3900) Battery_i                            = 0;

//Job actions
action tick_b, tick_sched;
action L_3F2_slew_preheat, L_3F2_start, L_3F2_slewback, L_3F2_end;
action L_3F3_slew_preheat, L_3F3_start, L_3F3_slewback, L_3F3_end;
action PV_aligned_start, PV_aligned_end, PV_notaligned_start, PV_notaligned_end;
action UHF_start, UHF_end, UHF_skip;
action X_Kourou_slew_preheat, X_Kourou_start, X_Kourou_slewback, X_Kourou_end;
action X_Toulouse_slew_preheat, X_Toulouse_start, X_Toulouse_slewback, X_Toulouse_end;

//Update battery actions
action update_PV;
action update_UHF;
action update_X_Band_Kourou;
action update_X_Band_Toulouse;
action update_L_Band_Inmarsat_3F2;
action update_L_Band_Inmarsat_3F3;

//Scheduler and skip actions
action Sched_3F2, Skip_3F2, Sched_3F3, Skip_3F3, Sched_Kourou, Skip_Kourou, Sched_Toulouse, Skip_Toulouse, Sched_Nothing;

//Boolean that determines if a L-band job is aligned with inmarsat. This has an influence on the amount of PV generation.
bool is_aligned = false;

//Execution counters. Start X-Band_heur with 2 to make sure that an L-job can begin
int(0 .. 100)[] L_X_counter = [0, 0, 0, 0, 0, 2]; //[3F2, 3F3, X-Kourou, X-Toulouse, X-Band_heur, L-Band_heur]

/*****************************************************************************************************************************************************
    Model E<> and Xmin<> properties

    Description:
    - The property "Iterator within bounds" checks that the iterator stays within the array bounds + 1 as explained in the Globals description. \
    The iterator should never be higher than size+1 as this implies that the automaton didn't deadlock at the last array element. This property should NOT hold.
    - The property "No deadlock" checks if there is a deadlock in the model until the specified clock value
    - The property "Generated Schedule until clk=" is a property that checks the minimum-cost path until the specified clock value
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
transient int cost = 0;

//property "Iterator within bounds"           = E<>(X_Kourou_i > X_Band_Kourou_data_size+1);
//property "No deadlock"                      = E<>(clk >= 240);
property "Generated Schedule until clk="    = Xmin(S(cost), clk >= end);

/*****************************************************************************************************************************************************
    Battery job process

    Job characteristics:
    - Battery capacity: 149760000 mJ

    Model description:
    With every update of a job process in the satelite it is checked whether this job can be completed in the SoC that is left without dropping below 40%.
    When the SoC reaches the Bat_cap the value of the SoC does not increase any further.
    When the SoC would still be bounded between Bat_cap and SoC_lb after the execution of the job, then the SoC is updated accordingly.
    When the SoC would drop below the 40% SoC_lb during a job process then the model is halted.

    Notes: 
    - SoC = maximum capacity when current SoC + accumulated load is higher than the maximum capacity of the battery
    - Unwanted behaviour to reach SoC lower bound => Assign the maximum reward
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process Battery_job()
{
    do
    { 
        //Sync scheduler with global clock
        alt
        {   
            //Max SoC of battery is reached
            :: when ((SoC - load * (current_a_time - last_a_time)) >= Bat_cap) alt { 
                :: update_PV                    {= SoC = Bat_cap =}                         
                :: update_UHF                   {= SoC = Bat_cap =} 
                :: update_X_Band_Kourou         {= SoC = Bat_cap =} 
                :: update_X_Band_Toulouse       {= SoC = Bat_cap =} 
                :: update_L_Band_Inmarsat_3F2   {= SoC = Bat_cap =}
                :: update_L_Band_Inmarsat_3F3   {= SoC = Bat_cap =}
                }
            //SoC is between bounds
            :: when ((SoC - load * (current_a_time - last_a_time)) > SoC_lb && (SoC - load * (current_a_time - last_a_time)) < Bat_cap) alt { 
                :: update_PV                    {= SoC -= load * (current_a_time - last_a_time) =} 
                :: update_UHF                   {= SoC -= load * (current_a_time - last_a_time) =} 
                :: update_X_Band_Kourou         {= SoC -= load * (current_a_time - last_a_time) =} 
                :: update_X_Band_Toulouse       {= SoC -= load * (current_a_time - last_a_time) =} 
                :: update_L_Band_Inmarsat_3F2   {= SoC -= load * (current_a_time - last_a_time) =} 
                :: update_L_Band_Inmarsat_3F3   {= SoC -= load * (current_a_time - last_a_time) =} 
                }
            //Lower bound is reached! Unwanted behaviour so maximum reward
            :: when ((SoC - load * (current_a_time - last_a_time)) <= SoC_lb) alt { 
                :: update_PV                    {= cost = maxReward =}; 
                   stop 
                :: update_UHF                   {= cost = maxReward =}; 
                   stop 
                :: update_X_Band_Kourou         {= cost = maxReward =}; 
                   stop 
                :: update_X_Band_Toulouse       {= cost = maxReward =}; 
                   stop 
                :: update_L_Band_Inmarsat_3F2   {= cost = maxReward =}; 
                   stop 
                :: update_L_Band_Inmarsat_3F3   {= cost = maxReward =}; 
                   stop 
                }
        }
    }
}

/*****************************************************************************************************************************************************
    L-band 3F2 job process

    Job characteristics:
    - Preheat time:         30 minutes
    - Power consumption:    3863 * 60 (231780)

    Model description:
    Carry out a L_Band job in the Inmarsat3F2 area.
    Stages:
    1 - Slew and preheat combined
    2 - Start actual job as defined in time window
    3 - Slew back
    4 - End job after slewing back
    The automaton breaks when the iterator points to the artificial "0" element in the array.
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process L_Band_Inmarsat_3F2_job()
{
    invariant(clk <= (L_Band_Inmarsat_3F2_data[L_3F2_i] - L_slew_preheat)) alt
    {
        :: when (clk >= (L_Band_Inmarsat_3F2_data[L_3F2_i] - L_slew_preheat) && L_3F2_i <= L_Band_Inmarsat_3F2_data_size) L_3F2_slew_preheat {= last_a_time = current_a_time, current_a_time = (L_Band_Inmarsat_3F2_data[L_3F2_i] - L_slew_preheat), job_clk = 0, L_3F2_i += 1 =};
            invariant(false) update_L_Band_Inmarsat_3F2 {= load += Slew_Preheat_Power =};

            invariant(job_clk <= L_slew_preheat) when (job_clk >= L_slew_preheat) L_3F2_start {= last_a_time = current_a_time, current_a_time += L_slew_preheat, job_clk = 0, is_aligned = true =};
            invariant(false) update_L_Band_Inmarsat_3F2 {= load += (L_Power - Slew_Preheat_Power) =};

            invariant(clk <= L_Band_Inmarsat_3F2_data[L_3F2_i]) when (clk >= L_Band_Inmarsat_3F2_data[L_3F2_i]) L_3F2_slewback {= last_a_time = current_a_time, current_a_time = L_Band_Inmarsat_3F2_data[L_3F2_i], job_clk = 0, L_3F2_i += 1 =};
            invariant(false) update_L_Band_Inmarsat_3F2 {= load -= (L_Power - Slew_Preheat_Power) =};

            invariant(job_clk <= slewing) when (job_clk >= slewing) L_3F2_end {= last_a_time = current_a_time, current_a_time += slewing, is_aligned = false =}; //; L_Band_Inmarsat_3F2_job()
            invariant(false) update_L_Band_Inmarsat_3F2 {= load -= Slew_Preheat_Power =}

        :: when (L_3F2_i > L_Band_Inmarsat_3F2_data_size) break
    }
}

/*****************************************************************************************************************************************************
    L-band 3F3 job process

    Job characteristics:
    - Preheat time:         30 minutes
    - Power consumption:    3863 * 60 (231780)
    
    Process description:
    Carry out a L_Band job in the Inmarsat3F3 area.
    Stages:
    1 - Slew and preheat combined
    2 - Start actual job as defined in time window
    3 - Slew back
    4 - End job after slewing back
    The automaton breaks when the iterator points to the artificial "0" element in the array.
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process L_Band_Inmarsat_3F3_job()
{
    invariant(clk <= (L_Band_Inmarsat_3F3_data[L_3F3_i] - L_slew_preheat)) alt
    {
        ::when (clk >= (L_Band_Inmarsat_3F3_data[L_3F3_i] - L_slew_preheat) && L_3F3_i <= L_Band_Inmarsat_3F3_data_size) L_3F3_slew_preheat {= last_a_time = current_a_time, current_a_time = (L_Band_Inmarsat_3F3_data[L_3F3_i] - L_slew_preheat), job_clk = 0, L_3F3_i += 1 =};
            invariant(false) update_L_Band_Inmarsat_3F3 {= load += Slew_Preheat_Power =};

            invariant(job_clk <= L_slew_preheat) when (job_clk >= L_slew_preheat) L_3F3_start {= last_a_time = current_a_time, current_a_time += L_slew_preheat, job_clk = 0, is_aligned = true =};
            invariant(false) update_L_Band_Inmarsat_3F3 {= load += (L_Power - Slew_Preheat_Power) =};

            invariant(clk <= L_Band_Inmarsat_3F3_data[L_3F3_i]) when (clk >= L_Band_Inmarsat_3F3_data[L_3F3_i]) L_3F3_slewback {= last_a_time = current_a_time, current_a_time = L_Band_Inmarsat_3F3_data[L_3F3_i], job_clk = 0, L_3F3_i += 1 =};
            invariant(false) update_L_Band_Inmarsat_3F3 {= load -= (L_Power - Slew_Preheat_Power) =};

            invariant(job_clk <= slewing) when (job_clk >= slewing) L_3F3_end {= last_a_time = current_a_time, current_a_time += slewing, is_aligned = false =}; //; L_Band_Inmarsat_3F3_job()
            invariant(false) update_L_Band_Inmarsat_3F3 {= load -= Slew_Preheat_Power =}

        ::when (L_3F3_i > L_Band_Inmarsat_3F3_data_size) break
    }
}

/*****************************************************************************************************************************************************
    Photovoltaic job process

    Job characteristics:
    - Power generation: 
        - Independent(UHF) and X-band job:  5700 * 60 (342000)
        - L-band job:                       6100 * 60 (366000)

    Model description:
    Every time the satellite gets in the sun, the battery starts charging and it stops the moment the satellite is out of the sun.
    When the satellite is in the sun the power generation depends on the satellite's attitude, which is either aligned (L-band) or not aligned (X-band).
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process PV_job()
{
    do
    {
        invariant(clk <= Sun_data[Sun_i]) alt
        {
            ::when (clk >= Sun_data[Sun_i] && Sun_i <= Sun_data_size && is_aligned) PV_aligned_start {= Sun_i += 1, last_a_time = current_a_time, current_a_time = Sun_data[Sun_i] =};
                invariant(false) update_PV {= load -= L_PV_Power =};

                invariant(clk <= Sun_data[Sun_i]) when (clk >= Sun_data[Sun_i]) PV_aligned_end {= Sun_i += 1, last_a_time = current_a_time, current_a_time = Sun_data[Sun_i] =};
                invariant(false) update_PV {= load += L_PV_Power =}

            ::when (clk >= Sun_data[Sun_i] && Sun_i <= Sun_data_size && !is_aligned) PV_notaligned_start {= Sun_i += 1, last_a_time = current_a_time, current_a_time = Sun_data[Sun_i] =};
                invariant(false) update_PV {= load -= X_PV_Power =};

                invariant(clk <= Sun_data[Sun_i]) when (clk >= Sun_data[Sun_i]) PV_notaligned_end {= Sun_i += 1, last_a_time = current_a_time, current_a_time = Sun_data[Sun_i] =}; 
                invariant(false) update_PV {= load += X_PV_Power =}

            ::when (Sun_i > Sun_data_size) break
        }
    }
}

/*****************************************************************************************************************************************************
    UHF job process

    Job characteristics:
    - Power consumption: 2630 * 60 (157800)

    Model description:
    A UHF job process downlinks collected data to, and uplinks new instructions from the GomSpace base station in Aalborg, Denmark.
    The UHF job process should be scheduled whenever possible (as much as it is available).
    This job is executed concurrently with other processes, hence can be executed in a do cycle. Breaks out of the cycle when the max array index is reached.
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process UHF_job()
{
    do
    {
        invariant(clk <= UHF_data[UHF_i]) alt
        {
            ::when (clk >= UHF_data[UHF_i] && UHF_i <= UHF_data_size) UHF_start {= UHF_i += 1, last_a_time = current_a_time, current_a_time = UHF_data[UHF_i] =};
                invariant(false) update_UHF {= load += UHF_Power =};

                invariant(clk <= UHF_data[UHF_i]) when (clk >= UHF_data[UHF_i]) UHF_end {= UHF_i += 1, last_a_time = current_a_time, current_a_time = UHF_data[UHF_i] =};
                invariant(false) update_UHF {= load -= UHF_Power =}

            ::when (clk >= UHF_data[UHF_i] && UHF_i <= UHF_data_size) UHF_skip {= UHF_i += 2, cost = maxReward =} //UHF skipped! Unwanted behaviour so maximum reward.

            ::when (UHF_i > UHF_data_size) break
        }
    }
}

/*****************************************************************************************************************************************************
    X-band Kourou job process

    Job characteristics:
    - Preheat time:         10 minutes
    - Power consumption:    11945 * 60 (716700)
    
    Model description: 
    Carry out a X_Band job in the Kourou area. 
    Stages:
    1 - Slew and preheat combined
    2 - Start actual job as defined in time window
    3 - Slew back
    4 - End job after slewing back
    The automaton breaks when the iterator points to the artificial "0" element in the array.
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process X_Band_Kourou_job()
{
    invariant(clk <= (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat)) alt
    {
        ::when (clk >= (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat) && X_Kourou_i <= X_Band_Kourou_data_size) X_Kourou_slew_preheat {= last_a_time = current_a_time, current_a_time = (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat), job_clk = 0, X_Kourou_i += 1 =};
            invariant(false) update_X_Band_Kourou {= load += Slew_Preheat_Power =};

            invariant(job_clk <= X_slew_preheat) when (job_clk >= X_slew_preheat) X_Kourou_start {= last_a_time = current_a_time, current_a_time += X_slew_preheat, job_clk = 0 =};
            invariant(false) update_X_Band_Kourou {= load += (X_Power - Slew_Preheat_Power) =};

            invariant(clk <= X_Band_Kourou_data[X_Kourou_i]) when (clk >= X_Band_Kourou_data[X_Kourou_i]) X_Kourou_slewback {= last_a_time = current_a_time, current_a_time = X_Band_Kourou_data[X_Kourou_i], job_clk = 0, X_Kourou_i += 1 =};
            invariant(false) update_X_Band_Kourou {= load -= (X_Power - Slew_Preheat_Power) =};

            invariant(job_clk <= slewing) when (job_clk >= slewing) X_Kourou_end {= last_a_time = current_a_time, current_a_time += slewing =};//; X_Band_Kourou_job()
            invariant(false) update_X_Band_Kourou {= load -= Slew_Preheat_Power =}

        ::when (X_Kourou_i > X_Band_Kourou_data_size) break
    }
}

/*****************************************************************************************************************************************************
    X-band Toulouse job process

    Job characteristics:
    - Preheat time:         10 minutes
    - Power consumption:    11945 * 60 (716700)
    
    Model description:
    Carry out a X_Band job in the Toulouse area.  
    Stages:
    1 - Slew and preheat combined
    2 - Start actual job as defined in time window
    3 - Slew back
    4 - End job after slewing back
    The automaton breaks when the iterator points to the artificial "0" element in the array.
*/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process X_Band_Toulouse_job()
{
    invariant(clk <= (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat)) alt
    {
        ::when (clk >= (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat) && X_Toulouse_i <= X_Band_Toulouse_data_size) X_Toulouse_slew_preheat {= last_a_time = current_a_time, current_a_time = (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat), job_clk = 0, X_Toulouse_i += 1 =};
            invariant(false) update_X_Band_Toulouse {= load += Slew_Preheat_Power =};

            invariant(job_clk <= X_slew_preheat) when (job_clk >= X_slew_preheat) X_Toulouse_start {= last_a_time = current_a_time, current_a_time += X_slew_preheat, job_clk = 0 =};
            invariant(false) update_X_Band_Toulouse {= load += (X_Power - Slew_Preheat_Power) =};

            invariant(clk <= X_Band_Toulouse_data[X_Toulouse_i]) when (clk >= X_Band_Toulouse_data[X_Toulouse_i]) X_Toulouse_slewback {= last_a_time = current_a_time, current_a_time = X_Band_Toulouse_data[X_Toulouse_i], job_clk = 0, X_Toulouse_i += 1 =};
            invariant(false) update_X_Band_Toulouse {= load -= (X_Power - Slew_Preheat_Power) =};

            invariant(job_clk <= slewing) when (job_clk >= slewing) X_Toulouse_end {= last_a_time = current_a_time, current_a_time += slewing =}; //; X_Band_Toulouse_job()
            invariant(false) update_X_Band_Toulouse {= load -= Slew_Preheat_Power =}
            
        ::when(X_Toulouse_i > X_Band_Toulouse_data_size) break
    }
}

/*****************************************************************************************************************************************************
    Skip jobs
    
    Model description:
    Check for every job if this job was active in the time window of the finished job in L_X_Scheduler(). 
    The do cycle is used to check all X- and L-Band jobs for possible skips in L_X_Skip(). 
    If a job is skipped, the array index might be incremented by two, hence going to the next "start" time of a job window.
*/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process L_X_Skip()
{
    do
    {
        invariant(false) alt
        {
            ::when (clk >= (L_Band_Inmarsat_3F2_data[L_3F2_i] - L_slew_preheat) && L_3F2_i <= L_Band_Inmarsat_3F2_data_size) Skip_3F2 {= L_3F2_i += 2 =}
            ::when (clk <= (L_Band_Inmarsat_3F2_data[L_3F2_i] - L_slew_preheat) && L_3F2_i <= L_Band_Inmarsat_3F2_data_size) break
        }
    };
    do
    {
        invariant(false) alt
        {
            ::when (clk >= (L_Band_Inmarsat_3F3_data[L_3F3_i] - L_slew_preheat) && L_3F3_i <= L_Band_Inmarsat_3F3_data_size) Skip_3F3 {= L_3F3_i += 2 =}
            ::when (clk <= (L_Band_Inmarsat_3F3_data[L_3F3_i] - L_slew_preheat) && L_3F3_i <= L_Band_Inmarsat_3F3_data_size) break
        }
    };
    do
    {
        invariant(false) alt
        {
            ::when (clk >= (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat) && X_Kourou_i <= X_Band_Kourou_data_size) Skip_Kourou {= X_Kourou_i += 2 =}
            ::when (clk <= (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat) && X_Kourou_i <= X_Band_Kourou_data_size) break
        }
    };
    do
    {
        invariant(false) alt
        {
            ::when (clk >= (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat) && X_Toulouse_i <= X_Band_Toulouse_data_size) Skip_Toulouse {= X_Toulouse_i += 2 =}
            ::when (clk <= (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat) && X_Toulouse_i <= X_Band_Toulouse_data_size) break
        }
    }
}

/*****************************************************************************************************************************************************
    L_Band_Inmarsat_*_job() or X_band_*_job() scheduler
    
    Model description:
    Process that schedules L_Band_Inmarsat_*_job() or X_band_*_job() jobs at runtime.
    Based on the fact that it is unwanted behaviour to do more L-Band jobs when less than two X-Band jobs are executed to downlink the data as this overflows the memory of GomX-3.
    It is also unwanted behaviour to execute more than two X-Band jobs sequantially without a L-band job in between because all data can be downlinked in at most two X-Band job executions.
    The skip process is called after every scheduling choice/job execution. This is done to make sure that after the job process has finished \
    the jobs that were active during the executed job window are skipped (index += 2) so the next job execution doesn't start in the wrong time window (too early).
    With sched_interval there is compensation for the schedule interval to prevent that the scheduled jobs are lagging behind.
*/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
process L_X_Scheduler() 
{
    clock sched_clk;

    do
    {   
        invariant(false) alt
        {
            //Scheduling L-Band jobs
            :: when (clk >= (L_Band_Inmarsat_3F2_data[L_3F2_i] - L_slew_preheat - sched_interval) && L_3F2_i <= L_Band_Inmarsat_3F2_data_size && L_X_counter[5] >= 2 && L_X_counter[4] < 1) Sched_3F2 {= L_X_counter[5] = 0, L_X_counter[4] += 1, L_X_counter[0] += 1, cost = L_X_counter[0] =};
                L_Band_Inmarsat_3F2_job(); L_X_Skip()

            :: when (clk >= (L_Band_Inmarsat_3F2_data[L_3F2_i] - L_slew_preheat - sched_interval) && L_3F2_i <= L_Band_Inmarsat_3F2_data_size && L_X_counter[5] < 2 && L_X_counter[4] < 1) Sched_3F2 {= L_X_counter[5] = 0, L_X_counter[4] += 1, L_X_counter[0] += 1, cost = maxReward + L_X_counter[0] =};          //Should not happen
                L_Band_Inmarsat_3F2_job(); L_X_Skip()

            :: when (clk >= (L_Band_Inmarsat_3F3_data[L_3F3_i] - L_slew_preheat - sched_interval) && L_3F3_i <= L_Band_Inmarsat_3F3_data_size && L_X_counter[5] >= 2 && L_X_counter[4] < 1) Sched_3F3 {= L_X_counter[5] = 0, L_X_counter[4] += 1, L_X_counter[1] += 1, cost = L_X_counter[1] =};
                L_Band_Inmarsat_3F3_job(); L_X_Skip()

            :: when (clk >= (L_Band_Inmarsat_3F3_data[L_3F3_i] - L_slew_preheat - sched_interval) && L_3F3_i <= L_Band_Inmarsat_3F3_data_size && L_X_counter[5] < 2 && L_X_counter[4] < 1) Sched_3F3 {= L_X_counter[5] = 0, L_X_counter[4] += 1, L_X_counter[1] += 1, cost = maxReward + L_X_counter[1] =};          //Should not happen
                L_Band_Inmarsat_3F3_job(); L_X_Skip()

            //Scheduling X-Band jobs
            :: when (clk >= (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat - sched_interval) && X_Kourou_i <= X_Band_Kourou_data_size && L_X_counter[5] < 1 && L_X_counter[4] > 0) Sched_Kourou {= L_X_counter[5] += 1, L_X_counter[2] += 1, cost = L_X_counter[2] =};
                X_Band_Kourou_job(); L_X_Skip()

            :: when (clk >= (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat - sched_interval) && X_Kourou_i <= X_Band_Kourou_data_size && L_X_counter[5] >= 1 && L_X_counter[4] > 0) Sched_Kourou {= L_X_counter[5] += 1, L_X_counter[4] = 0, L_X_counter[2] += 1, cost = L_X_counter[2] =};
                X_Band_Kourou_job(); L_X_Skip()

            :: when (clk >= (X_Band_Kourou_data[X_Kourou_i] - X_slew_preheat - sched_interval) && X_Kourou_i <= X_Band_Kourou_data_size && L_X_counter[5] >= 2 && L_X_counter[4] > 0) Sched_Kourou {= L_X_counter[5] += 1, L_X_counter[4] = 0, L_X_counter[2] += 1, cost = maxReward + L_X_counter[2] =};            //Should not happen
                X_Band_Kourou_job(); L_X_Skip()

            :: when (clk >= (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat - sched_interval) && X_Toulouse_i <= X_Band_Toulouse_data_size  && L_X_counter[5] < 1 && L_X_counter[4] > 0) Sched_Toulouse {= L_X_counter[5] += 1, L_X_counter[3] += 1, cost = L_X_counter[3] =};
                X_Band_Toulouse_job(); L_X_Skip()

            :: when (clk >= (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat - sched_interval) && X_Toulouse_i <= X_Band_Toulouse_data_size  && L_X_counter[5] >= 1 && L_X_counter[4] > 0) Sched_Toulouse {= L_X_counter[5] += 1, L_X_counter[4] = 0, L_X_counter[3] += 1, cost = L_X_counter[3] =};
                X_Band_Toulouse_job(); L_X_Skip()

            :: when (clk >= (X_Band_Toulouse_data[X_Toulouse_i] - X_slew_preheat - sched_interval) && X_Toulouse_i <= X_Band_Toulouse_data_size  && L_X_counter[5] >= 2 && L_X_counter[4] > 0) Sched_Toulouse {= L_X_counter[5] += 1, L_X_counter[4] = 0, L_X_counter[3] += 1, cost = maxReward + L_X_counter[3] =}; //Should not happen
                X_Band_Toulouse_job(); L_X_Skip()

            //Scheduling no jobs
            :: when (L_3F2_i <= L_Band_Inmarsat_3F2_data_size || L_3F3_i <= L_Band_Inmarsat_3F3_data_size || X_Kourou_i <= X_Band_Kourou_data_size || X_Toulouse_i <= X_Band_Toulouse_data_size) Sched_Nothing {= cost = maxReward, sched_clk = 0 =}; //Should always try to schedule a job
                invariant(sched_clk <= sched_interval) when (sched_clk >= sched_interval) tick_sched
        }
    }
}

/*****************************************************************************************************************************************************
    Combine all processes
    
    Description:
    The satellite model consists of four concurrent job classes:
    - Battery job
    - Photovoltaics job 
    - UHF job 
    - L-Band or X-Band job
*//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
par
{
    //Test processes
    //::L_Band_Inmarsat_3F2_job()
    //::L_Band_Inmarsat_3F3_job()
    //::X_Band_Kourou_job()
    //::X_Band_Toulouse_job()

    ::Battery_job()
    ::PV_job()
    ::UHF_job()
    ::L_X_Scheduler()
}