<jupyter_start><jupyter_text>F16 Air Collision Property FalsificationWe will be analyzing an air collision avoidance autopilot, attempting to find instances where the autopilot fails to avoid a collision. For this activity, we have described the F16 system, intruder scenario, properties, and solver configuration using CSAF abstractions. Namely,* **Systems** The ownship and intruder F-16 systems are described as systems composed of components. The ACAS autopilot collects messages of both aircrafts' states and determines a corrective course for the ownship.* **Scenarios** The systems are dozens of states and parameters, and so exploring this space fully would be intensive. Scenarios allow one to define an interface that reduces the parameters to search by fixing some value or appealing to symmetry present in the system. For instance, rather than varying both aircrafts' position, airspeed, and heading, relative values are searched. We fix the ownship speed, heading, and position, while varying the intruder.* **Goals** Goals encode properties associated with systems or scenarios and an analysis that can verify or falsify them. In this case, we attempt to falsify a collision property using bayesian optimization. Note that failing to falsify the collision doesn't mean that the ownship is verfied to avoid a collision in the scenario's configuration space.<jupyter_code># imports
import numpy as np
import matplotlib.pyplot as plt
%matplotlib inline
%config InlineBackend.figure_format='retina'

import sys
sys.path.append("..")

import csaf
from csaf_f16.goals import AcasSimpleFalsifyGoal, AcasNoBalloonAirspeedFalsifyGoal<jupyter_output><empty_output><jupyter_text>Construct the F16 Scenario`csaf_f16` has a collection goals in `csaf_f16.goals`. One goal is `AcasSimpleFalsifyGoal` and contains an intruder and ownship F-16 whose relative lateral position, heading, and airspeed can be searched.<jupyter_code># Create falsification goal
g = AcasSimpleFalsifyGoal()<jupyter_output><empty_output><jupyter_text>Solve the Optimization ProblemThe goal object already has its falsification strategy set--constrained bayesian optimization (using `GPyOpt`). As the falsifier will run indefinitely if there are no counterexamples, we set a maximum time and maximum number of solver iterations.<jupyter_code># Run optimization with default values
g.test(max_time=300.0, max_iter=1000)<jupyter_output><empty_output><jupyter_text>Visualize the Optimal Configuration<jupyter_code># plot GPyOpt's Convergence Information
g.optimizer.plot_convergence()
# print optimal configuration and objective value
print(g.optimizer.x_opt)
print(g.optimizer.fx_opt)
# run the best example and plot the results (using AcasScenarioViewer)
from csaf_f16.acas import AcasScenarioViewer

x0 = g.optimizer.x_opt
scen = g.scenario_type()
trajs, p = g.run_sim(x0)

viewer = AcasScenarioViewer(trajs, scen)
fig, ax = viewer.summary_plot()
ax.set_xlim(-10000, 10000)
ax.set_ylim(0, 25000)
plt.show()
# uncomment this to see a video
"""
from IPython.display import HTML
from matplotlib import animation
anim = viewer.summary_video(bounds=((-15000, 15000), (-5000, 25000)), msize=0.0005)
HTML(anim.to_jshtml())
"""<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.06672873991309745, 'fraction_numerical': 0.02110490378646803, 'mean_word_length': 6.3752860411899315, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 17, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '4', 'dir': 'jupyter-structured-clean-dedup', 'id': '381488', 'license': 'BSD-3-Clause', 'n_tokens_mistral': 980, 'n_tokens_neox': 903, 'n_words': 371, 'path': 'notebooks/f16-acas-constrained-bopt.ipynb', 'repo_name': 'GaloisInc/csaf', 'size': '3222'}