Event-B建模（六）——控制桥上汽车，精化
目录
- 第一次精化
- 状态的精化
- 事件的精化
- 第二次精化
- 状态的精化
- 事件的精化
- 第三次精化
- 状态的精化
- 事件的精化
这篇的上一篇在这个地方Event-B建模（三）——控制桥上汽车，初始模型，环境配置和小问题的解决都在上一篇中有写，这里就不重复了
第一次精化
在第一次精化时，我们要考虑的不再是桥岛组合体，而是要引入“桥”的概念，现在要考虑的模型如下图所示：
因为多了“桥”这个概念，所以我们要考虑更多的事件，例如汽车进入或者离开小岛，称为IL_in和IL_out，而ML_out和ML_in在这次精化中依然存在，分别对应于汽车离开大陆上桥和离开桥进入大陆
状态的精化
在第一次精化时，我们让常量d保持原样，而变量使用三个变量取代，因为现在多了桥这个概念，单纯的n已经无法表示汽车行驶的方向
我们现在使用三个变量a，b，c来表示，a表示在桥上并驶向小岛的车辆数，变量b表示在岛上的车辆数，而变量c表示在桥上并驶向大陆的车辆数
画个表格
| 变量 | 含义 |
|---|---|
| a | 在桥上并驶向小岛的车辆数 |
| b | 在岛上的车辆数 |
| c | 在桥上并驶向大陆的车辆数 |
首先a，b，c必须是自然数，a,b,c∈Na,b,c\in Na,b,c∈N，然后a，b，c的总和是n，即a+b+c=n，并且因为桥是个单行道，所以a和c不能同时大于0，可以写成a=0∨c=0a=0\vee c=0a=0∨c=0
这里新添加上新的变量a，b，c顺便可以把原来的变量n删除
事件的精化
接下来我们对事件进行精化
汽车离开大陆上桥事件
在精化中，我们新版本的ML_out称为具体版本，而原来的ML_out被称为抽象版本，在这里我们看到这个具体的版本和抽象版本的卫guard完全不同，但是我们却可以发现它和抽象版本并没有什么矛盾，也就是说，当具体卫条件成立的时候，抽象版本的卫肯定也是成立，因为a+b<d以及c=0就相当于a+b+c<d也就相当于n<d
下面的ML_in事件仍然符合这个条件
我们认为，正确的精化时，需要保证具体的卫比抽象的卫更强，什么叫更强？这就意味着具体的卫蕴含着抽象的卫，也可以说不可能出现一种情况，使得具体的卫成立，但抽象的卫不成立。正确精化的证明义务用GRD表示，可以看到左边证明义务一栏里面已经有了GRD这个义务
汽车离开桥进入大陆事件
汽车进入小岛事件
a必须大于0，在岛上的汽车数量b++，而a–
汽车离开小岛
在岛上的汽车数量必须大于0，a必须等于0，因为这是个单行桥，action就是b–以及c++
来看一下左边新的证明义务，可能会出现某一个证明义务没通过，就是ML_in/grd1/GRD这个
（下面两张图不是我的，来自于某位同学，该同学已同意我使用）
双击一下，切换到proving视图，点一下这个绳索一下按钮，记得保存，记得保存，记得保存，然后这个证明义务就通过了
证明义务通过是通过了，不过这样就结束了嘛？就像代码编译完了没有报错，语法是正确了，但是不能保证你的逻辑没问题呀
当引进了一些新事件时，我们还必须证明另外一些东西，就是说它们不会发散，也就是说，这些新事件不会永无止境地执行。为了证明这一性质，我们必须给出一个自然数值的表达式，称为变动式(variant)，而后证明所有的新事件都会减少它的值。这就带来了两个证明义务：第一个是说我们提出的这个变动式是一个自然数，第二个是说每个新事件都会减小该变动式的值
其实提出的这个变动式相当于while循环中的那个条件，我们如何确认while循环会终止呢？假设while循环长成while(n>0)这个样子，我们要确保n每次都会减小就行了，而我们提出的变动式需要在新的事件执行后，这个变动式会确实的减少，从而表明新的事件不会永无止境的运行下去
如何在rodin里完成这一过程呢？来看一看吧，新的事件是IL_in，和IL_out
点一下这个ordinary，然后跳出一个框，选择convergent（收敛的），按F5刷新一下
这时候我们的证明义务又跳出四个新的证明义务了，分别是IL_in和IL_out的VAR和NAT证明义务
然后我们提出一个变动式，注意变动式variant这个单词和变量(variables)这个单词有点像，别搞混了哟~
试试看吧，如果变动式是a+b怎么样呢？我们看到执行IL_in的时候b加了1，a减少了1，IL_out的时候b减少了1，执行IL_out的时候的确没啥大问题，因为确实地减少了，不过执行IL_in又加了b，好像执行了对于变动式也没啥变化，所以我们可以让a减少得比b快就可以了，所以我们的变动式只要是形如n*a+b的形式就可以了，这里就用2*a+b好了
保存一下，再次发现证明义务都证明完成了
最后的最后，我们还要保证所有的具体的时间（无论新的还是老的）都不会出现比抽象事件更多的死锁，也像第一次模型那样，我们加入一个无死锁的定理
这个条件说变了就是把所有的gurad条件析取
这样一来，第一次精化总算是全部完成了
第二次精化
在第二次精化中，我们将加入红绿灯，汽车可以根据交通灯的指示来决定是否上桥
在这一次精化中，我们首先必须引入两个交通灯，分别取名为ml_tl和il_tl，分别代表在大陆一端的红绿灯以及在小岛一端的红绿灯，然后引入相应的不变式，最后引入一些新的事件，用新的事件改变交通灯的颜色
状态的精化
第二次精化同样继承一个context，精化原来的machine
首先红绿灯的颜色定义为常量，所以我们引入COLOR集合，并且定义其中的red,green这两个常量，这个操作和之前的银行小系统差不多
然后把变量ml_tl和il_tl加上
只有inv3和inv4需要解释一下，其他地方都挺好理解的，inv3和inv4是带条件的不变式，⇒\Rightarrow⇒这个符号其实就是蕴含符→\rightarrow→，只不过写成这样子罢了
inv3代表大陆侧的灯为绿色时，只能由大陆侧的汽车上桥，而不能出现小岛侧的汽车驶向大陆的情况，因为绿灯代表某侧的汽车可以上桥且桥为单行道，并且a+b<d在桥上的车数量不能超过d
事件的精化
ML_out和IL_out需要进行精化，只有当红绿灯为绿色时，才能执行这两个事件，这一步需要修改一下guard条件，使得我们这次精化的事件卫更强，结合inv3和inv4不变式，精化后的事件为：
接下来引入两个新的事件，使得在适当的条件下，红绿灯的颜色由红转绿，这俩事件的gurad条件其实和ML_out和IL_out差不多，不过多了红绿灯为红这个guard
保存一下，发现左边红色还有些INV没有证明出来，说明我们现在的模型还存在一些问题，需要再仔细检查并且修改一下
我们考虑到当a+1+b=d的时候，也就说进入的这辆汽车是允许进入的最后一辆汽车，这个时候就不能再进入汽车了，不然会违背需求FUN-2，event-b里面可没有变成语言的if条件语句，碰到这种情况我们再添加一个事件，然后事件的guard不同就可以了
把原来的ML_out改名为ML_out_1，并且处理a+b+1≠da+b+1\neq da+b+1=d的时候的情况，然后ML_out_2用来处理a+b+1=da+b+1=da+b+1=d的情况，这个时候要让等变红
同理，IL_out这边也要考虑b=0的情况，b=0就代表没有汽车了，不可以再执行离岛操作了，灯也要变成红色
改完了之后再看看证明义务
到了这一步，目前的证明义务都是证明通过的，还有人记得还需要做什么吗？就像第一次精化一样，这次新的模型仍然要检查收敛
现在有可能出现这样一种情况，两个红色灯一直在变，导致其他的事件无法执行，这样子肯定是不行的，所以要把这种灯疯狂改变的情况排除掉。我们的解决方案是，提供一种限定，当红绿灯的一边变成绿色之后，只有在有汽车从这个方向上通过的时候才能使得红绿灯再次改变，下面的实现方案有些繁琐，不过实现了我们刚刚说的限定
添加两个值为0,1的变量il_pass和ml_pass，初始化为1
这里再添加上inv8和9这两个不变式，其实这两个条件是在我们设计的模型下必然成立的，不过为了系统推导出证明义务，还是要手动加上去
下面的意思是，如果执行了ML_tl_green红绿灯变绿的事件，那么该端的_pass变量变成0，这样可以阻止另一端的红绿灯发生变化，直到有车通过为止
ML_out和IL_out也添加相应的改变
写上变动式
最后我们再上一个证明无死锁
inv10: (ml_tl=red ∧ a+b<d ∧ c=0 ∧ ml_pass=1 ∧ il_pass=1) ∨ (il_tl=red ∧ a=0 ∧ b>0 ∧ ml_pass=1 ∧ il_pass=1) ∨ ml_tl=green ∨ il_tl=green ∨ a>0 ∨ c>0
这样一来，我们的第二次精化也完成了
第三次精化
终于到了最后一次的精化，在最后一次精化中，我们将引入传感器
一共四个传感器，分别是ML_OUT_SR,ML_IN_SR,IL_OUT_SR,IL_IN_SR，对应着进出大陆和进出小岛
因为这里出现了传感器，所以我们将在这个系统中明确地区分软件控制环境和物理环境，下图描绘了这个情况
控制变量：
变量a，b，c以及il_pass和ml_pass，在这里我们要明确，这里的变量a,b,c未必恰好对应于桥上和岛上物理汽车数目，只是代表控制软件中的计数
环境变量：
四个代表传感器状态的变量，ML_OUT_SR,ML_IN_SR,IL_OUT_SR,IL_IN_SR，然后我们还要引入三个变量A、B、C，分别代表桥上驶向小岛的汽车（A）、在岛上的汽车（B）、和桥上驶向大陆的汽车（C）的物理数量
输出通道
代表从控制器到环境的输出通道，有变量ml_tl，il_tl，
输入通道
代表从环境获取的信号传输到控制器，一个传感器有两种不同的状态，“开”或者“关”，当一辆汽车抵达时，传感器由“关”状态改为“开”状态，此时传感器不向控制器发送任何消息，而当一辆汽车通过传感器时，传感器的状态由“开”变成了“关”，此时的传感器会向控制器发送一个信号，为此引入4个输入通道变量，每个变量对应于一个传感器，ml_out_10、ml_in_10、il_out_10和il_in_10
整个系统的控制流程如下图所示：
状态的精化
各个变量的意义弄清楚了，之后开始在rodin里面编写
先继承一个context
主要是定义传感器
（senor2n这个是之后建立变动式要用到的东西，就是把on和off这两个状态赋予一个值）
建立一个mac4精化mac3
加上不变式（因为实在太长了，分开来截图）
这部分是变量值域的定义
当传感器状态为on时，说明有车辆通过，所以对物理变量A，B，C有所要求
当输入通道ml_out_10为1时，说明刚刚有一辆汽车离开了传感器，此时该方向的红绿灯必须是绿色的，同理，il_out_10也是类似
当一辆车位于某个传感器上时，对应输入通道上没有消息
这里应该添加上一条假设，控制器必须足够快速，能够处理来自环境的所有信息
另外的不变式是关于汽车的物理数量（A，B，C）以及与之对应的控制器处理的汽车数量(a，b，c)之间的关系，例如：
看第一条，当il_in_10=1时，代表有一辆汽车已经离开桥进入小岛，但控制器还不知道这个情况，这样A已经减小而B已经增大，但控制器变量a和b并没有改变，类似地，ml_out_10=1，代表有一辆车从大陆上桥，但控制器当时还不知道这个情况，因此A已经增大，但是a没有变化
还有类似的不变式处理B和b以及C和c：
最后，物理变量A，B，C同样有如同abc那样的限制条件
定义完了不变式需要进行初始化
事件的精化
事件的精化我们直接写出
下面是4个新增的新事件，分别对应于有车到达各个传感器
最后的四个事件对应于汽车离开对应的传感器
做到了这里，保存一下，有问题也可以用之前的方案解决，不过我们仍然要证明新的事件是收敛的
提出一个变动式
12−(sensor2n(ML_OUT_SR)+sensor2n(ML_IN_SR)+sensor2n(IL_OUT_SR)+sensor2n(IL_IN_SR)+2∗(ml_out_10+ml_in_10+il_out_10+il_in_10))12-(sensor2n(ML\_OUT\_SR)+sensor2n(ML\_IN\_SR)+sensor2n(IL\_OUT\_SR)+sensor2n(IL\_IN\_SR)+2∗(ml\_out\_10+ml\_in\_10+il\_out\_10+il\_in\_10))12−(sensor2n(ML_OUT_SR)+sensor2n(ML_IN_SR)+sensor2n(IL_OUT_SR)+sensor2n(IL_IN_SR)+2∗(ml_out_10+ml_in_10+il_out_10+il_in_10))
其实前面的12可以换成一个任意大于12的自然数，当然也有其他不同的变动式，譬如说想想利用A，B，C这三个变量来写，而且我给on赋值为1，off赋值为0，其实换种赋值方式就可以改成不同的变动式了
最后再证明无死锁（应该可以化简的，不过我没有化简）
(ml_out_10=1 ∧ a+b+1≠d) ∨ (ml_out_10=1 ∧ a+b+1=d) ∨ (0<c ∧ ml_in_10=1) ∨ (0<a ∨ il_in_10=1) ∨ (il_out_10=1 ∧ b≠1) ∨ (il_out_10=1 ∧ b=1) ∨ (ml_tl=red ∧ a+b<d ∧ c=0 ∧ il_pass=1 ∧ il_out_10=0) ∨ (il_tl=red ∧ 0<b ∧ a=0 ∧ ml_pass=1 ∧ ml_out_10=0) ∨ (ML_OUT_SR=off ∧ ml_out_10=0) ∨ (ML_IN_SR=off ∧ ml_in_10=0 ∧ c>0) ∨ (IL_IN_SR=off ∧ il_in_10=0 ∧ A>0) ∨ (IL_OUT_SR=off ∧ il_out_10=0 ∧ B>0) ∨ (ML_OUT_SR=on ∧ ml_tl=green) ∨ ML_IN_SR=on ∨ IL_IN_SR=on ∨ (IL_OUT_SR=on ∧ il_tl=green)
到此为止，控制桥上的汽车这个模型全部结束啦~
第三次精化的证明义务有169个，还好有工具，要是手动证明的话肯定是要累死
说起来Event-B其实也挺久了，学习的时候竟然很少有中文资料，既然网上没有又要学习，所以只好干脆自己写一份了，希望以后学习的人看到能够少走弯路，节约时间。
Event-B建模（六）——控制桥上汽车，精化相关推荐
- Event-B建模（三）——控制桥上汽车，初始模型
目录 需求文档 分析 前置准备 新建工程 状态的形式化 模型状态的静态部分 模型状态的动态部分 事件的形式化 证明义务 无死锁证明 解决出现的问题 安装完了Rodin,现在让我们开始动手验证吧~ 以一 ...
- 线性系统大作业——2.二阶倒立摆建模与控制系统设计（上）
文章目录 0.简介 1.建立数学模型 1.1.牛顿运动定律分析 欧拉-拉格朗日方程分析 2.Simulink仿真 3.使用SimMechancis仿真 4.在平衡点附近模型线性化 5.系统能控性.能观 ...
- MATLAB优化转向器,汽车电动转向器动力学建模与控制仿真研究(MATLAB仿真)
汽车电动转向器动力学建模与控制仿真研究(MATLAB仿真)(任务书,开题报告,外文翻译,计划进度表,毕业论文12000字,相关框图和参数) 摘 要 汽车电动转向器是一种新型的汽车转向助力系统. 文章 ...
- 超牛！用WIFI控制的摇控汽车
(今天在PCClub上看到一牛人的帖子,拿来和大家分享下.) 超牛!用WIFI控制的摇控汽车 一.前言 Wifi机器人(Wifi Robot):其实是一辆能通过互联网,或500米以外的笔记本无线设施来 ...
- 《机器人与数字人：基于MATLAB的建模与控制》——2.3节指数映射和k过程
本节书摘来自华章社区<机器人与数字人:基于MATLAB的建模与控制>一书中的第2章,第2.3节指数映射和k过程,作者［美］顾友谅(Edward Y.L.Gu),更多章节内容可以访问云栖社区 ...
- 《机器人与数字人：基于MATLAB的建模与控制》——2.2节李群和李代数
本节书摘来自华章社区<机器人与数字人:基于MATLAB的建模与控制>一书中的第2章,第2.2节李群和李代数,作者［美］顾友谅(Edward Y.L.Gu),更多章节内容可以访问云栖社区&q ...
- jsp文件通常用common_29.jsp-动态生活之用Commons-FileUpload组件控制文件上传
sizeMax):设置请求信息实体内容的最大允许的字节数 ★ public List parseRequest(HttpServletRequest req): 解析form表单中的每个字符的数据,返 ...
- 19个神经元控制自动驾驶汽车，MIT等虫脑启发新研究登Nature子刊
本文经机器之心(almosthuman2014)授权转载,禁止二次转载. 选自Medium 作者:Louis Bouchard 机器之心编译 编辑:魔王.泽南 这种新型智能系统模仿线虫的神经系统来高效 ...
- Java实验8 T5.使用键盘控制界面上图片的移动
编写程序,实现使用键盘上的上下左右箭头控制界面上图片的移动.移动到边界时从界面另一侧出现.移动过程中显示另一个图片,停止时恢复原来的图片. package text8;//MyFrame.java i ...
最新文章
- HDU_5249(百度之星D题)
- 直博5年！叹我年少轻狂！头4年一篇1作SCI也没有...
- 《那些年啊，那些事——一个程序员的奋斗史》——86
- 今日恐慌与贪婪指数为40 恐慌程度有所上升
- java原生开发项目-快递e栈
- OpenCV2 图像叠加 给照片加水印
- Simple-RNN with Keras
- Windows 相关镜像及补丁下载地址
- 黑马程序员--Mysql中文乱码解决办法
- Fiddler手机APP抓包及无法连接网络问题处理
- 淘特，阿里在下沉市场的一把好刀
- ubuntu 14.04全攻略
- 多角度了解ABeam（德硕）技术架构
- js闭包的理解及应用场景
- Linux内存卡槽故障判断,内存插槽损坏的三种常见故障
- SprinBoot实现接管SpringMVC自定义配置
- 微信小程序获取头像昵称，限制头像大小
- java中Map遍历的四种方式
- 品铂平板电脑刷linux,教你如何把品铂PIPO W8平板电脑升级到win10系统_硬件教程
- C语言-密码2,输入一行电报文字，将字母变成其下一字母（如’a’变成’b’……’z’变成’ａ’其它字符不变）。