Event-B建模实际操作：控制桥上的汽车（三）

接上节；在现在的形式中，桥的模型看起来有些奇妙。按照我们的观察，好像汽车司机能统计汽车的数量，并据此决定能不能从大陆上桥或者从岛上桥。这也意味着我们能看到系统的状态。显然，这是根本不可能的。为此，我们进一步做精化。 Second Refinement: Introducing the Traffic Lights In its present form, the model of the brid

>>阅读原文<<