建模模拟工程
研究文章

通向智能空中交通控制系统使用形式法

框16

inv5:Abjects_in_runway⊆aircrafts_in_airport
inv6:Abjects_in_runway≠∅⇒urr_RW_status≔不可用