Space_mission case study

[iincer]

Hi @NicolasRouquette,
I made this change to polyhedral-contract-example3.py in the space_mission branch (I also deleted the plotting branch because all functionality is in space_mission):

https://github.com/FormalSystems/pacti/blob/2f68b407362c62da5e391b8ba92f67edc9dbe034/case_studies/polyhedra_contracts/polyhedral-contract-example3.py#L28

The composition works on my end. Can you try and let me know if we still have issues with composition? Also, do we still need the polyhedra-contracts branch?

[NicolasRouquette]

Thanks for the fix!

The polyhedra-contracts branch is about the syntactic support for polyhedral contracts.

I believe that we've reached a point where this work is completed. Before merging this into main, I suggest adding some documentation to explain the API so as to facilitate migration for others on the project.

The space_mission branch is about 2 case studies, both of which are ongoing:

• the spacecraft / small-body approach scenario in (the space_mission subfolder)
• the Mars 2020 EDL scenario (in the mars_entry_descent_landing subfolder)

It will make sense to merge this branch when these case studies have reached a point where we can explain interesting results obtained with Pacti. Meanwhile, we can merge updates of the polyhedral-contracts branch as needed.

[NicolasRouquette]

There is something strange w/ the atmospheric_entry contract:

https://github.com/FormalSystems/pacti/blob/ffd49aac00f00c119c2c161bacb660c3ea02c185/case_studies/mars_entry_descent_landing/mars_edl.ipynb

I was puzzled why v1 can be negative:

So I tried to add a guarantee (commented out): -v1 <= 0.
With this constraint, the plot becomes empty.

Is there something wrong?

[NicolasRouquette]

With this update: https://github.com/FormalSystems/pacti/blob/06a7daaf39f7e202758c1ad4b9779cd12e75e8a4/case_studies/mars_entry_descent_landing/mars_edl.ipynb

I get this:

It seems that we have to specify constraints about the range of possible exit time and velocity.

Something like:

t1 - t0 \in [ delta_t1_min, delta_t1_max ]
v1 -v0 \in [ delta_v1_min, delta_v1_max ]

[iincer]

Thanks, @NicolasRouquette, for providing means to reproduce this. The problem was with empty interiors again. I made another update that should robustly allow plots of equalities (in the space_mission branch).

[iincer]

I made a couple of modifications to polyhedral-contract-example3.py, and composition works correctly now.

https://github.com/FormalSystems/pacti/blob/8b71ca78c01fd2218cbec47d897cfe8d25b79736/case_studies/polyhedra_contracts/polyhedral-contract-example3.py#L14-L42

[iincer]

The additional constraint v1 <= 1500 may not make much sense. Instead of bounding v1, we may try bounding t1 from above, which will implicitly impose a bound on v1.