Event-B建模實際操作：控制橋上的汽車（三）

接上節；在現在的形式中，橋的模型看起來有些奇妙。按照我們的觀察，好像汽車司機能統計汽車的數量，並據此決定能不能從大陸上橋或者從島上橋。這也意味着我們能看到系統的狀態。顯然，這是根本不可能的。爲此，我們進一步做精化。 Second Refinement: Introducing the Traffic Lights In its present form, the model of the brid

>>阅读原文<<