Schedulability Analysis with 3 Viewpoints

%matplotlib widget

from pacti.contracts import PolyhedralIoContract
from pacti.utils import read_contracts_from_file
from contract_utils import *

Scenario design analysis across viewpoints

Operating a space mission system requires allocating resources among tasks in order to satisfy operational requirements across multiple domain-specific viewpoints. For this case study, we developed scenarios in 4 viewpoints as summarized qualitative in the table below:

Viewpoint	State	CHARGING	DSN	SBO	TCM
Power	soc	+	-	-	-
Science	d	0	-	+	0
	c	0	0	+	0
Navigation	u	+	+	-	+
	r	0	0	0	+
Thermal	temp	-	-	-	+

The specification of the thermal scenario helped us realize that there are no significant thermal interactions among the scenario tasks that would constraint possible schedules. Therefore, it makes sense to omit the thermal viewpoint for the scenario analysis, leaving power, science & communication, and navigation as the significant viewpoints to use for optimizing the scenario design.

Now, we need to gather operational requirements for each of the three viewpoints.

Operational requirements by viewpoint

Here, we adopt a simple methodology for exploring admissible scenario schedules as sets of possible solutions to the duration of each task. The idea is to elicit operational requirements as constraints on the entry/exit scenario state variables. We use a forcing technique to ensure that admissible solutions correspond to schedules where each task has a positive scheduled duration.

Power

The following specification defines a conservative operational regime that requires the battery state of charge to be at minimum 40% based on an initial state of charge of 80%; we force a non-trivial schedule by requiring that the duration of each task be no less than 10 units.

op_req_pwr1=PolyhedralIoContract.from_strings(
    input_vars=[
        "soc1_entry",
        "duration_dsn1",
        "duration_charging2",
        "duration_sbo3",
        "duration_tcm_heating4",
        "duration_tcm_deltav5",
    ],
    output_vars=[
        "output_soc1",
        "output_soc2",
        "output_soc3",
        "output_soc4",
        "output_soc5"
    ],
    assumptions=[
        "soc1_entry=80",
        "duration_dsn1 >= 10",
        "duration_charging2 >= 10",
        "duration_sbo3 >= 10",
        "duration_tcm_heating4 >= 10",
        "duration_tcm_deltav5 >= 10",
    ],
    guarantees=[
        "output_soc1 >= 40",
        "output_soc2 >= 40",
        "output_soc3 >= 40",
        "output_soc4 >= 40",
        "output_soc5 >= 40",
    ])

The following specification defines a aggressive operational regime that requires the battery state of charge to be at minimum 10% based on an initial state of charge of 80%; we force a non-trivial schedule by requiring that the duration of each task be no less than 10 units.

op_req_pwr2=PolyhedralIoContract.from_strings(
    input_vars=[
        "soc1_entry",
        "duration_dsn1",
        "duration_charging2",
        "duration_sbo3",
        "duration_tcm_heating4",
        "duration_tcm_deltav5",
    ],
    output_vars=[
        "output_soc1",
        "output_soc2",
        "output_soc3",
        "output_soc4",
        "output_soc5"
    ],
    assumptions=[
        "soc1_entry=80",
        "duration_dsn1 >= 10",
        "duration_charging2 >= 10",
        "duration_sbo3 >= 10",
        "duration_tcm_heating4 >= 10",
        "duration_tcm_deltav5 >= 10",
    ],
    guarantees=[
        "output_soc1 >= 10",
        "output_soc2 >= 10",
        "output_soc3 >= 10",
        "output_soc4 >= 10",
        "output_soc5 >= 10",
    ]
)

Science & Communication

It is useful to calculate how much science the avionics capability can deliver. For this, the following operational requirement specifies the initial conditions only. As before, we force a non-trivial schedule by requiring that the duration of each task be no less than 10 units.

op_req_sci0=PolyhedralIoContract.from_strings(
    input_vars=[
        "c1_entry",
        "d1_entry",
        "duration_dsn1",
        "duration_charging2",
        "duration_sbo3",
        "duration_tcm_heating4",
        "duration_tcm_deltav5",
    ],
    output_vars=[
        "output_c5",
        "output_d5",
    ],
    assumptions=[
        # "c1_entry = 0",
        # "d1_entry >= 70",
        "duration_dsn1 >= 10",
        "duration_charging2 >= 10",
        "duration_sbo3 >= 10",
        "duration_tcm_heating4 >= 10",
        "duration_tcm_deltav5 >= 10",
    ],
    guarantees=[
    ]
)

The following specification defines a conservative operational regime that requires the spacecraft to downlink at least 50% of its onboard science data storage while acquiring at least 60 units of science data from the initial conditions defined above.

op_req_sci1=op_req_sci0.merge(PolyhedralIoContract.from_strings(
    input_vars=[
        # "d1_entry",
    ],
    output_vars=[
        "output_c5",
        "output_d5",
    ],
    assumptions=[
        # "d1_entry >= 70",
    ],
    guarantees=[
        # "output_c5 >= 10",
        "output_d5 >= 10",
    ]
))

The following specification defines an aggressive operational regime that requires the spacecraft to downlink at least 90% of its onboard science data storage while acquiring at least 80 units of science data from the initial conditions defined above.

op_req_sci2=op_req_sci0.merge(PolyhedralIoContract.from_strings(
    input_vars=[],
    output_vars=[
        "output_c5",
        "output_d5",
    ],
    assumptions=[],
    guarantees=[
        # "output_c5 >= 80",
        "output_d5 >= 90",
    ]
))

Navigation

The following specification defines a conservative operational regime that requires the spacecraft to reduce navigation uncertainty to below 40% from an initial level of 70% and to reduce trajectory relative distance to below 80% starting from an inital level of 100%. As before, we force a non-trivial schedule by requiring that the duration of each task be no less than 10 units.

op_req_nav1=PolyhedralIoContract.from_strings(
    input_vars=[
        "u1_entry",
        "r1_entry",
        "duration_dsn1",
        "duration_charging2",
        "duration_sbo3",
        "duration_tcm_heating4",
        "duration_tcm_deltav5",
    ],
    output_vars=[
        "output_u5",
        "output_r5",
    ],
    assumptions=[
        "u1_entry = 30",
        "r1_entry = 100",
        "duration_dsn1 >= 10",
        "duration_charging2 >= 10",
        "duration_sbo3 >= 10",
        "duration_tcm_heating4 >= 10",
        "duration_tcm_deltav5 >= 10",
    ],
    guarantees=[
        "output_u5 <= 80",
        "output_r5 <= 80",
    ]
)

The following specification defines an aggressive operational regime that requires the spacecraft to reduce navigation uncertainty to below 20% from an initial level of 70% and to reduce trajectory relative distance to below 70% starting from an inital level of 100%. As before, we force a non-trivial schedule by requiring that the duration of each task be no less than 10 units.

op_req_nav2=PolyhedralIoContract.from_strings(
    input_vars=[
        "u1_entry",
        "r1_entry",
        "duration_dsn1",
        "duration_charging2",
        "duration_sbo3",
        "duration_tcm_heating4",
        "duration_tcm_deltav5",
    ],
    output_vars=[
        "output_u5",
        "output_r5",
    ],
    assumptions=[
        "u1_entry = 30",
        "r1_entry = 80",
        "duration_dsn1 >= 10",
        "duration_charging2 >= 10",
        "duration_sbo3 >= 10",
        "duration_tcm_heating4 >= 10",
        "duration_tcm_deltav5 >= 10",
    ],
    guarantees=[
        "output_u5 <= 80",
        "output_r5 <= 70",
    ]
)

Exploring combinations of operational scenario requirements

So far, we have defined conservative and aggressive operational requirements for each viewpoint. We can exploit the commutativity property of Pacti's contract merge operation to explore combinations of these requirements.

The first step involves reading the viewpoint-specific scenarios from their respective viewpoint-specific scenario case studies as shown below:

scenario_pwr = read_contracts_from_file(file_name="json/scenario_power.json")[0][1]
scenario_sci = read_contracts_from_file(file_name="json/scenario_science.json")[0][1]
scenario_nav = read_contracts_from_file(file_name="json/scenario_nav.json")[0][1]

Next, we explore algebraic combinations of scenarios and operational requirements with the confidence that the order in which we merge the requirements and scenarios is irrelevant. This flexibility gives an opportunity for collaborative design exploration where different teams could explore merging different combinations of viewpoints and requirement variants (e.g., conservative vs. aggressive).

all_scenarios = scenario_pwr.merge(scenario_sci).merge(scenario_nav)
print(f"all_scenarios:\n{all_scenarios}")
print('\n'.join(bounds(all_scenarios)))

all_scenarios:
InVars: [soc1_entry, duration_dsn1, duration_charging2, duration_sbo3, duration_tcm_heating4, duration_tcm_deltav5, d1_entry, c1_entry, u1_entry, r1_entry]
OutVars:[output_soc4, output_soc3, output_soc2, output_soc1, output_soc5, output_d4, output_c4, output_d3, output_c3, output_d2, output_c2, output_d1, output_c1, output_d5, output_c5, output_u4, output_r4, output_u3, output_r3, output_u2, output_r2, output_u1, output_r1, output_u5, output_r5]
A: [
  -duration_tcm_deltav5 <= -0
  -4 duration_charging2 + 2.2 duration_dsn1 + 0.2 duration_sbo3 + 0.3 duration_tcm_deltav5 + 0.8 duration_tcm_heating4 - soc1_entry <= -0
  -duration_tcm_heating4 <= -0
  -duration_sbo3 <= -0
  -duration_charging2 <= -0
  5 duration_charging2 - 2 duration_dsn1 + soc1_entry <= 100
  -duration_dsn1 <= -0
  soc1_entry <= 100
  2.2 duration_dsn1 - soc1_entry <= -0
  d1_entry - 0.3 duration_dsn1 + 4 duration_sbo3 <= 100
  -d1_entry <= -0
  d1_entry <= 100
  -c1_entry <= -0
  -u1_entry <= -0
  u1_entry <= 100
  -r1_entry <= -0
  r1_entry <= 100
]
G: [
  2 duration_dsn1 + output_soc1 - soc1_entry <= 0
  -2.2 duration_dsn1 - output_soc1 + soc1_entry <= 0
  4 duration_charging2 + output_soc1 - output_soc2 <= 0
  -5 duration_charging2 - output_soc1 + output_soc2 <= 0
  0.1 duration_sbo3 - output_soc2 + output_soc3 <= 0
  -0.2 duration_sbo3 + output_soc2 - output_soc3 <= 0
  0.7 duration_tcm_heating4 - output_soc3 + output_soc4 <= 0
  -0.8 duration_tcm_heating4 + output_soc3 - output_soc4 <= 0
  0.2 duration_tcm_deltav5 - output_soc4 + output_soc5 <= 0
  -0.3 duration_tcm_deltav5 + output_soc4 - output_soc5 <= 0
  -d1_entry + 0.3 duration_dsn1 + output_d1 <= 0
  d1_entry - 0.5 duration_dsn1 - output_d1 <= 0
  -output_d1 <= 0
  -c1_entry + output_c1 = 0
  -output_d1 + output_d2 = 0
  -output_c1 + output_c2 = 0
  3 duration_sbo3 + output_d2 - output_d3 <= 0
  -4 duration_sbo3 - output_d2 + output_d3 <= 0
  3 duration_sbo3 + output_c2 - output_c3 <= 0
  -4 duration_sbo3 - output_c2 + output_c3 <= 0
  -output_d3 + output_d4 = 0
  -output_c3 + output_c4 = 0
  -output_d4 + output_d5 = 0
  -output_c4 + output_c5 = 0
  output_u1 - u1_entry <= 1.2
  -output_u1 + u1_entry <= -1.1
  output_r1 - r1_entry = 0
  output_u2 <= 100
  -output_u1 + output_u2 <= 1.1
  output_u1 - output_u2 <= -1
  -output_r1 + output_r2 = 0
  -0.6 duration_sbo3 + output_u2 - output_u3 <= 0
  0.5 duration_sbo3 - output_u2 + output_u3 <= 0
  -output_u3 <= 0
  -output_r2 + output_r3 = 0
  -output_u3 + output_u4 = 0
  -output_r3 + output_r4 = 0
  output_u5 <= 100
  -1.6 duration_tcm_deltav5 - output_u4 + output_u5 <= 0
  1.5 duration_tcm_deltav5 + output_u4 - output_u5 <= 0
  -0.5 duration_tcm_deltav5 + output_r4 - output_r5 <= 0
  0.4 duration_tcm_deltav5 - output_r4 + output_r5 <= 0
  -output_r5 <= 0
]
 input c1_entry in [0.00,None]
 input d1_entry in [0.00,100.00]
 input duration_charging2 in [0.00,20.00]
 input duration_dsn1 in [0.00,45.45]
 input duration_sbo3 in [0.00,25.00]
 input duration_tcm_deltav5 in [0.00,66.67]
 input duration_tcm_heating4 in [0.00,125.00]
 input r1_entry in [0.00,100.00]
 input soc1_entry in [0.00,100.00]
 input u1_entry in [0.00,97.90]
output output_c1 in [0.00,None]
output output_c2 in [0.00,None]
output output_c3 in [0.00,None]
output output_c4 in [0.00,None]
output output_c5 in [0.00,None]
output output_d1 in [0.00,100.00]
output output_d2 in [0.00,100.00]
output output_d3 in [0.00,100.00]
output output_d4 in [0.00,100.00]
output output_d5 in [0.00,100.00]
output output_r1 in [0.00,100.00]
output output_r2 in [0.00,100.00]
output output_r3 in [0.00,100.00]
output output_r4 in [0.00,100.00]
output output_r5 in [0.00,100.00]
output output_soc1 in [0.00,100.00]
output output_soc2 in [0.00,100.00]
output output_soc3 in [0.00,100.00]
output output_soc4 in [0.00,100.00]
output output_soc5 in [0.00,100.00]
output output_u1 in [1.10,99.00]
output output_u2 in [2.10,100.00]
output output_u3 in [0.00,100.00]
output output_u4 in [0.00,100.00]
output output_u5 in [0.00,100.00]

a1_p = all_scenarios.merge(op_req_pwr1)
a1_n = all_scenarios.merge(op_req_nav1)
a1_s = all_scenarios.merge(op_req_sci1)
a1_pn = a1_p.merge(op_req_nav1)
print(f"op_req_sci1\n{op_req_sci1}")
a1_ps = a1_p.merge(op_req_sci1)
a1_sn = a1_s.merge(op_req_nav1)
print("ok")
print(f"op_req_sci1:\n{op_req_sci1}")
print("a1_s"+'\n'.join(bounds(a1_s)))

req_d1=PolyhedralIoContract.from_strings(
    input_vars=[
        "d1_entry",
    ],
    output_vars=[
    ],
    assumptions=[
        "d1_entry >= 70",
    ],
    guarantees=[
    ]
)
a1_sd1 = all_scenarios.merge(op_req_sci1).merge(req_d1)
print("a1_sd1"+'\n'.join(bounds(a1_sd1)))
req_sci1_d1=op_req_sci1.merge(req_d1)
print(f"req_sci1_d1\n{req_sci1_d1}")
a2_sd1 = all_scenarios.merge(req_sci1_d1)
print("a2_sd1"+'\n'.join(bounds(a2_sd1)))

op_req_sci1
InVars: [c1_entry, d1_entry, duration_dsn1, duration_charging2, duration_sbo3, duration_tcm_heating4, duration_tcm_deltav5]
OutVars:[output_c5, output_d5]
A: [
  -duration_dsn1 <= -10
  -duration_charging2 <= -10
  -duration_sbo3 <= -10
  -duration_tcm_heating4 <= -10
  -duration_tcm_deltav5 <= -10
]
G: [
  -output_d5 <= -10
]
ok
op_req_sci1:
InVars: [c1_entry, d1_entry, duration_dsn1, duration_charging2, duration_sbo3, duration_tcm_heating4, duration_tcm_deltav5]
OutVars:[output_c5, output_d5]
A: [
  -duration_dsn1 <= -10
  -duration_charging2 <= -10
  -duration_sbo3 <= -10
  -duration_tcm_heating4 <= -10
  -duration_tcm_deltav5 <= -10
]
G: [
  -output_d5 <= -10
]
a1_s input c1_entry in [0.00,None]
 input d1_entry in [3.00,73.64]
 input duration_charging2 in [10.00,19.60]
 input duration_dsn1 in [10.00,45.45]
 input duration_sbo3 in [10.00,25.00]
 input duration_tcm_deltav5 in [10.00,66.67]
 input duration_tcm_heating4 in [10.00,103.75]
 input r1_entry in [4.00,100.00]
 input soc1_entry in [22.00,100.00]
 input u1_entry in [2.70,97.90]
output output_c1 is unknown
output output_c2 is unknown
output output_c3 in [30.00,None]
output output_c4 in [30.00,None]
output output_c5 in [30.00,None]
output output_d1 in [0.00,60.00]
output output_d2 in [0.00,60.00]
output output_d3 in [30.00,100.00]
output output_d4 in [30.00,100.00]
output output_d5 in [30.00,100.00]
output output_r1 in [4.00,100.00]
output output_r2 in [4.00,100.00]
output output_r3 in [4.00,100.00]
output output_r4 in [4.00,100.00]
output output_r5 in [0.00,96.00]
output output_soc1 in [0.00,50.00]
output output_soc2 in [40.00,100.00]
output output_soc3 in [35.00,99.00]
output output_soc4 in [3.00,92.00]
output output_soc5 in [0.00,90.00]
output output_u1 in [3.90,99.00]
output output_u2 in [5.00,100.00]
output output_u3 in [0.00,85.00]
output output_u4 in [0.00,85.00]
output output_u5 in [15.00,100.00]
a1_sd1 input c1_entry in [0.00,None]
 input d1_entry in [70.00,73.64]
 input duration_charging2 in [10.00,18.67]
 input duration_dsn1 in [33.33,45.45]
 input duration_sbo3 in [10.00,10.91]
 input duration_tcm_deltav5 in [10.00,66.67]
 input duration_tcm_heating4 in [10.00,93.75]
 input r1_entry in [4.00,100.00]
 input soc1_entry in [73.33,100.00]
 input u1_entry in [2.70,89.45]
output output_c1 is unknown
output output_c2 is unknown
output output_c3 in [30.00,None]
output output_c4 in [30.00,None]
output output_c5 in [30.00,None]
output output_d1 in [47.27,60.00]
output output_d2 in [47.27,60.00]
output output_d3 in [77.27,100.00]
output output_d4 in [77.27,100.00]
output output_d5 in [77.27,100.00]
output output_r1 in [4.00,100.00]
output output_r2 in [4.00,100.00]
output output_r3 in [4.00,100.00]
output output_r4 in [4.00,100.00]
output output_r5 in [0.00,96.00]
output output_soc1 in [0.00,33.33]
output output_soc2 in [40.00,100.00]
output output_soc3 in [37.82,99.00]
output output_soc4 in [3.00,92.00]
output output_soc5 in [0.00,90.00]
output output_u1 in [3.90,90.55]
output output_u2 in [5.00,91.55]
output output_u3 in [0.00,85.00]
output output_u4 in [0.00,85.00]
output output_u5 in [15.00,100.00]
req_sci1_d1
InVars: [c1_entry, d1_entry, duration_dsn1, duration_charging2, duration_sbo3, duration_tcm_heating4, duration_tcm_deltav5]
OutVars:[output_c5, output_d5]
A: [
  -duration_dsn1 <= -10
  -duration_charging2 <= -10
  -duration_sbo3 <= -10
  -duration_tcm_heating4 <= -10
  -duration_tcm_deltav5 <= -10
  -d1_entry <= -70
]
G: [
  -output_d5 <= -10
]
a2_sd1 input c1_entry in [0.00,None]
 input d1_entry in [70.00,73.64]
 input duration_charging2 in [10.00,18.67]
 input duration_dsn1 in [33.33,45.45]
 input duration_sbo3 in [10.00,10.91]
 input duration_tcm_deltav5 in [10.00,66.67]
 input duration_tcm_heating4 in [10.00,93.75]
 input r1_entry in [4.00,100.00]
 input soc1_entry in [73.33,100.00]
 input u1_entry in [2.70,89.45]
output output_c1 is unknown
output output_c2 is unknown
output output_c3 in [30.00,None]
output output_c4 in [30.00,None]
output output_c5 in [30.00,None]
output output_d1 in [47.27,60.00]
output output_d2 in [47.27,60.00]
output output_d3 in [77.27,100.00]
output output_d4 in [77.27,100.00]
output output_d5 in [77.27,100.00]
output output_r1 in [4.00,100.00]
output output_r2 in [4.00,100.00]
output output_r3 in [4.00,100.00]
output output_r4 in [4.00,100.00]
output output_r5 in [0.00,96.00]
output output_soc1 in [0.00,33.33]
output output_soc2 in [40.00,100.00]
output output_soc3 in [37.82,99.00]
output output_soc4 in [3.00,92.00]
output output_soc5 in [0.00,90.00]
output output_u1 in [3.90,90.55]
output output_u2 in [5.00,91.55]
output output_u3 in [0.00,85.00]
output output_u4 in [0.00,85.00]
output output_u5 in [15.00,100.00]

Next, we check whether there exists an admissible set of scenario schedules for all conservative operational requirements.

all_conservative_op_reqs = all_scenarios.merge(op_req_pwr1).merge(op_req_sci1).merge(op_req_nav1)
print(f"all_conservative_op_reqs=\n{all_conservative_op_reqs}")
print('\n'.join(bounds(all_conservative_op_reqs)))

all_conservative_op_reqs=
InVars: [soc1_entry, duration_dsn1, duration_charging2, duration_sbo3, duration_tcm_heating4, duration_tcm_deltav5, d1_entry, c1_entry, u1_entry, r1_entry]
OutVars:[output_soc4, output_soc3, output_soc2, output_soc1, output_soc5, output_d4, output_c4, output_d3, output_c3, output_d2, output_c2, output_d1, output_c1, output_d5, output_c5, output_u4, output_r4, output_u3, output_r3, output_u2, output_r2, output_u1, output_r1, output_u5, output_r5]
A: [
  -duration_tcm_deltav5 <= -0
  -4 duration_charging2 + 2.2 duration_dsn1 + 0.2 duration_sbo3 + 0.3 duration_tcm_deltav5 + 0.8 duration_tcm_heating4 - soc1_entry <= -0
  -duration_tcm_heating4 <= -0
  -duration_sbo3 <= -0
  -duration_charging2 <= -0
  5 duration_charging2 - 2 duration_dsn1 + soc1_entry <= 100
  -duration_dsn1 <= -0
  soc1_entry <= 100
  2.2 duration_dsn1 - soc1_entry <= -0
  d1_entry - 0.3 duration_dsn1 + 4 duration_sbo3 <= 100
  -d1_entry <= -0
  d1_entry <= 100
  -c1_entry <= -0
  -u1_entry <= -0
  u1_entry <= 100
  -r1_entry <= -0
  r1_entry = 100
  soc1_entry = 80
  -duration_dsn1 <= -10
  -duration_charging2 <= -10
  -duration_sbo3 <= -10
  -duration_tcm_heating4 <= -10
  -duration_tcm_deltav5 <= -10
  u1_entry = 30
]
G: [
  2 duration_dsn1 + output_soc1 - soc1_entry <= 0
  -2.2 duration_dsn1 - output_soc1 + soc1_entry <= 0
  4 duration_charging2 + output_soc1 - output_soc2 <= 0
  -5 duration_charging2 - output_soc1 + output_soc2 <= 0
  0.1 duration_sbo3 - output_soc2 + output_soc3 <= 0
  -0.2 duration_sbo3 + output_soc2 - output_soc3 <= 0
  0.7 duration_tcm_heating4 - output_soc3 + output_soc4 <= 0
  -0.8 duration_tcm_heating4 + output_soc3 - output_soc4 <= 0
  0.2 duration_tcm_deltav5 - output_soc4 + output_soc5 <= 0
  -0.3 duration_tcm_deltav5 + output_soc4 - output_soc5 <= 0
  -d1_entry + 0.3 duration_dsn1 + output_d1 <= 0
  d1_entry - 0.5 duration_dsn1 - output_d1 <= 0
  -output_d1 <= 0
  -c1_entry + output_c1 = 0
  -output_d1 + output_d2 = 0
  -output_c1 + output_c2 = 0
  3 duration_sbo3 + output_d2 - output_d3 <= 0
  -4 duration_sbo3 - output_d2 + output_d3 <= 0
  3 duration_sbo3 + output_c2 - output_c3 <= 0
  -4 duration_sbo3 - output_c2 + output_c3 <= 0
  -output_d3 + output_d4 = 0
  -output_c3 + output_c4 = 0
  -output_d4 + output_d5 = 0
  -output_c4 + output_c5 = 0
  output_u1 - u1_entry <= 1.2
  -output_u1 + u1_entry <= -1.1
  output_r1 - r1_entry = 0
  -output_u1 + output_u2 <= 1.1
  output_u1 - output_u2 <= -1
  -output_r1 + output_r2 = 0
  -0.6 duration_sbo3 + output_u2 - output_u3 <= 0
  0.5 duration_sbo3 - output_u2 + output_u3 <= 0
  -output_r2 + output_r3 = 0
  -output_u3 + output_u4 = 0
  -output_r3 + output_r4 = 0
  1.5 duration_tcm_deltav5 + output_u4 - output_u5 <= 0
  -0.5 duration_tcm_deltav5 + output_r4 - output_r5 <= 0
  -output_soc1 <= -40
  -output_soc5 <= -40
  output_u5 <= 80
  output_r5 <= 80
]
 input c1_entry in [0.00,None]
 input d1_entry in [4.50,25.33]
 input duration_charging2 in [10.00,12.00]
 input duration_dsn1 in [15.00,20.00]
 input duration_sbo3 in [20.17,25.00]
 input duration_tcm_deltav5 in [40.00,41.93]
 input duration_tcm_heating4 in [10.00,71.40]
 input r1_entry in [100.00,100.00]
 input soc1_entry in [80.00,80.00]
 input u1_entry in [30.00,30.00]
output output_c1 in [0.00,None]
output output_c2 in [0.00,None]
output output_c3 in [60.50,None]
output output_c4 in [60.50,None]
output output_c5 in [60.50,None]
output output_d1 in [0.00,19.33]
output output_d2 in [0.00,19.33]
output output_d3 in [60.50,100.00]
output output_d4 in [60.50,100.00]
output output_d5 in [60.50,100.00]
output output_r1 in [100.00,100.00]
output output_r2 in [100.00,100.00]
output output_r3 in [100.00,100.00]
output output_r4 in [100.00,100.00]
output output_r5 in [79.03,80.00]
output output_soc1 in [40.00,50.00]
output output_soc2 in [80.00,100.00]
output output_soc3 in [75.00,97.98]
output output_soc4 in [48.00,90.98]
output output_soc5 in [40.00,82.98]
output output_u1 in [31.10,31.20]
output output_u2 in [32.10,32.30]
output output_u3 in [17.10,20.00]
output output_u4 in [17.10,20.00]
output output_u5 in [77.10,80.00]

all_aggressive_op_reqs = all_scenarios.merge(op_req_pwr2).merge(op_req_sci2).merge(op_req_nav2)
print(f"all_aggressive_op_reqs=\n{all_aggressive_op_reqs}")

all_aggressive_op_reqs=
InVars: [soc1_entry, duration_dsn1, duration_charging2, duration_sbo3, duration_tcm_heating4, duration_tcm_deltav5, d1_entry, c1_entry, u1_entry, r1_entry]
OutVars:[output_soc4, output_soc3, output_soc2, output_soc1, output_soc5, output_d4, output_c4, output_d3, output_c3, output_d2, output_c2, output_d1, output_c1, output_d5, output_c5, output_u4, output_r4, output_u3, output_r3, output_u2, output_r2, output_u1, output_r1, output_u5, output_r5]
A: [
  -duration_tcm_deltav5 <= -0
  -4 duration_charging2 + 2.2 duration_dsn1 + 0.2 duration_sbo3 + 0.3 duration_tcm_deltav5 + 0.8 duration_tcm_heating4 - soc1_entry <= -0
  -duration_tcm_heating4 <= -0
  -duration_sbo3 <= -0
  -duration_charging2 <= -0
  5 duration_charging2 - 2 duration_dsn1 + soc1_entry <= 100
  -duration_dsn1 <= -0
  soc1_entry <= 100
  2.2 duration_dsn1 - soc1_entry <= -0
  d1_entry - 0.3 duration_dsn1 + 4 duration_sbo3 <= 100
  -d1_entry <= -0
  d1_entry <= 100
  -c1_entry <= -0
  -u1_entry <= -0
  u1_entry <= 100
  -r1_entry <= -0
  r1_entry <= 100
  soc1_entry = 80
  -duration_dsn1 <= -10
  -duration_charging2 <= -10
  -duration_sbo3 <= -10
  -duration_tcm_heating4 <= -10
  -duration_tcm_deltav5 <= -10
  u1_entry = 30
  r1_entry = 80
]
G: [
  2 duration_dsn1 + output_soc1 - soc1_entry <= 0
  -2.2 duration_dsn1 - output_soc1 + soc1_entry <= 0
  4 duration_charging2 + output_soc1 - output_soc2 <= 0
  -5 duration_charging2 - output_soc1 + output_soc2 <= 0
  0.1 duration_sbo3 - output_soc2 + output_soc3 <= 0
  -0.2 duration_sbo3 + output_soc2 - output_soc3 <= 0
  0.7 duration_tcm_heating4 - output_soc3 + output_soc4 <= 0
  -0.8 duration_tcm_heating4 + output_soc3 - output_soc4 <= 0
  0.2 duration_tcm_deltav5 - output_soc4 + output_soc5 <= 0
  -0.3 duration_tcm_deltav5 + output_soc4 - output_soc5 <= 0
  -d1_entry + 0.3 duration_dsn1 + output_d1 <= 0
  d1_entry - 0.5 duration_dsn1 - output_d1 <= 0
  -output_d1 <= 0
  -c1_entry + output_c1 = 0
  -output_d1 + output_d2 = 0
  -output_c1 + output_c2 = 0
  -4 duration_sbo3 - output_d2 + output_d3 <= 0
  3 duration_sbo3 + output_c2 - output_c3 <= 0
  -4 duration_sbo3 - output_c2 + output_c3 <= 0
  -output_d3 + output_d4 = 0
  -output_c3 + output_c4 = 0
  -output_d4 + output_d5 = 0
  -output_c4 + output_c5 = 0
  output_u1 - u1_entry <= 1.2
  -output_u1 + u1_entry <= -1.1
  output_r1 - r1_entry = 0
  -output_u1 + output_u2 <= 1.1
  output_u1 - output_u2 <= -1
  -output_r1 + output_r2 = 0
  -0.6 duration_sbo3 + output_u2 - output_u3 <= 0
  0.5 duration_sbo3 - output_u2 + output_u3 <= 0
  -output_r2 + output_r3 = 0
  -output_u3 + output_u4 = 0
  -output_r3 + output_r4 = 0
  -1.6 duration_tcm_deltav5 - output_u4 + output_u5 <= 0
  1.5 duration_tcm_deltav5 + output_u4 - output_u5 <= 0
  -0.5 duration_tcm_deltav5 + output_r4 - output_r5 <= 0
  0.4 duration_tcm_deltav5 - output_r4 + output_r5 <= 0
  -output_soc1 <= -10
  -output_soc5 <= -10
  -output_d5 <= -90
  output_u5 <= 80
  output_r5 <= 70
]

def show_bounds(c: PolyhedralIoContract):
    print("Task duration bounds:")
    print(f"    step1_dsn: "+str(c.get_variable_bounds("duration_dsn1")))
    print(f"    step2_charging: "+str(c.get_variable_bounds("duration_charging2")))
    print(f"    step3_sbo: "+str(c.get_variable_bounds("duration_sbo3")))
    print(f"    step4_tcm_heating: "+str(c.get_variable_bounds("duration_tcm_heating4")))
    print(f"    step5_tcm_deltav: "+str(c.get_variable_bounds("duration_tcm_deltav5")))

    print("Power bounds:")
    print(f"    soc5: "+str(c.get_variable_bounds("output_soc5")))
    print("Science bounds:")
    print(f"    d5: "+str(c.get_variable_bounds("output_d5")))
    print(f"    c5: "+str(c.get_variable_bounds("output_c5")))
    print("Navigation bounds:")
    print(f"    u5: "+str(c.get_variable_bounds("output_u5")))
    print(f"    r5: "+str(c.get_variable_bounds("output_r5")))

    max_soc = c.optimize("0.2 output_soc1 + 0.2 output_soc2 + 0.2 output_soc3 + 0.2 output_soc4 + 0.2 output_soc5", maximize=True)
    min_soc = c.optimize("0.2 output_soc1 + 0.2 output_soc2 + 0.2 output_soc3 + 0.2 output_soc4 + 0.2 output_soc5", maximize=False)
    print(f"[min, max] average SOC=[{min_soc}, {max_soc}]")

show_bounds(all_conservative_op_reqs)

Task duration bounds:
    step1_dsn: (15.0, 20.0)
    step2_charging: (10.0, 12.0)
    step3_sbo: (20.16666666666667, 25.0)
    step4_tcm_heating: (10.0, 71.40476190476191)
    step5_tcm_deltav: (40.0, 41.93333333333333)
Power bounds:
    soc5: (40.0, 82.98333333333333)
Science bounds:
    d5: (60.500000000000014, 100.0)
    c5: (60.500000000000014, None)
Navigation bounds:
    u5: (77.1, 80.0)
    r5: (79.03333333333333, 80.0)
[min, max] average SOC=[56.6, 84.39]

show_bounds(all_aggressive_op_reqs)

Task duration bounds:
    step1_dsn: (15.0, 35.0)
    step2_charging: (10.0, 18.0)
    step3_sbo: (10.0, 25.0)
    step4_tcm_heating: (10.0, 98.75)
    step5_tcm_deltav: (20.0, 41.93333333333333)
Power bounds:
    soc5: (10.0, 88.0)
Science bounds:
    d5: (90.0, 100.0)
    c5: (30.0, None)
Navigation bounds:
    u5: (47.1, 80.0)
    r5: (59.03333333333333, 70.0)
[min, max] average SOC=[25.8, 85.80000000000001]