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

紧接上节。现在我们要继续工作，做出初始模型的第一个精化。一个精化就是一个比初始模型更精确的模型。虽然它更精确，但也不应该与初始模型矛盾。这样，我们就必须证明这个精化与初始模型的一致性。 First Refinement: Introducing the One-Way Bridge We are now going to proceed with a refinement of our initi

>>阅读原文<<