Display_Model_Goal
	• Tells pilot desired rate of altitude change • Checking for consistency gave a counterexample – Other_Aircraft reverse from an Increase- Climb to an Increase-Descend advisory – After study, this is only permitted in our non- deterministic modeling of Other_Aircraft – Modeling a piece of Other_Aircraft’s logic precludes this counterexample