MIU 系统简介

MIU 系统是一个无限的字符串转移系统(Transaction System)。MIU 系统仅包括三种字母，即 Alphabet = {M,I,U};以及四种转移规则，T1、T2、 T3、T4。一条由“MIU”组成的字符串即为系统的一种状态。MIU 系统需要指定初始状态 S0 与目标的终点状态 Sfinal。四条转移规则具体如下:

T1“appendU”规则，若当前的合法字符串以“I”结尾，则可以在其尾部追加一个字母“U”。例如串“MUI” 可以利用 T1 规则转化为“MUIU”。
T2“appendDouble”规则，若当前的合法字符串的首字母是“M”，则可以在其尾部追加当前字符串除了首字母的子串。例如串“MUI”可以利用 T2 规则转化为“MUIUI”。
T3“deleteI”规则，若当前的合法字符串中包含连续的三个“I”，则去除此连续的三个“I”，余下的字符
串首尾相接合成新串。例如串“MIIIU” 可以利用 T3 规则转化为“MU”。
T4“deleteU”规则，若当前的合法字符串中包含连续的两个“U”，则去除此连续的两个“U”，余下的字符串首尾相接合成新串。例如串“MUUI” 可以利用 T4 规则转化为“MI”。
系统要验证的需求是，在给定的初始状态 S0，利用以上四个转移规则，是否能生成目标终点状态 Sfinal。

MIU 在 Maude 中的建模

对于类别设计，MIU 系统仅仅涉及字母表和字符串(系统状态)，所以设计 miu 与 State 两类。

sort miu .
sort State .

对于操作符设计，指定字母表含有上述字母{M,I,U}，并且字符串(字母)可以链接成新字符串，指定系统状态操作符。代码如下所示。

ops  M I U : -> miu .
op _ _ : miu miu -> miu [assoc].
op state : miu -> State .

MIU 系统的转化规则代码如下所示:

vars s1 s2 : miu .
rl [appendU] : state(s1 I) => state(s1 I U) .
rl [appendDouble] : state(M s1) => state(M s1 s1) .
rl [deleteI] : state(s1 I I I s2) => state(s1 s2) .
rl [deleteU] : state(s1 U U s2) => state(s1 s2) .

MIU 系统实验效果

对于此系统，我进行了两组实验。

实验 A

S0=“MIIIU”，能否达到 Sfinal=“MUUUU”。操作语句:

load miu.maude .
search [1] state(M I I I U) =>* state(M U U U U) .
show search graph .

实验效果：

实验B

S0=“MI”，能否达到Sfinal=“MU”。
操作语句：

load miu.maude .
search [1] state(M I) =>* state(M U) .
show search graph .

由于这是一个无限系统，如果去搜索一个不可能存在的状态，则需要对推理步长进行限制，否则maude将无限运行。然而限制了推理步长则无法严格证明。所以需要用另一种思路来证明MIU系统之中不可能出现的状态。

系统规约的其他解法

MIU问题规约到310问题。
将M映射到整数“3”，I映射到整数“1”，U映射到整数“0”。已知自然数N能被三整除，则N的各个位上的数字之和，也能被三整除；若N各个位上的数字不能被三整除，则N不能被三整除。
MIU的规则到310的规则映射：
T1“appendU”规则，若当前的合法整数以“1”结尾，则可以在其尾部追加“3”。例如串“3111”可以利用T1规则转化为“31113”。
T2“appendDouble”规则，若当前的合法整数的最高位是“3”，则可以在其尾部追加当前整数除了最高位的剩余整数。例如串“310”可以利用T2规则转化为“31010”。
T3“deleteI”规则，若当前的合法整数中包含连续的三个“1”，则去除此连续的三个“1”，余下的整数首尾相接合成新整数。例如串“31110”可以利用T3规则转化为“30”。
T4“deleteU”规则，若当前的合法整数中包含连续的两个“0”，则去除此连续的两个“0”，余下的整数首尾相接合成新整数。例如串“3001”可以利用T4规则转化为“31”。
可以发现当S0是可以被3整除时，无论如何操作四条规则，状态Sx都是能被3整除；反之当S0是不可以被3整除时，无论如何操作四条规则，状态Sx都是不能被3整除。

所以当原MIU系统输入MI，即310系统的31时，是无法到达MIU系统的MU，即310系统的30的。

完整代码

用Maude对MIU系统建模相关推荐

第一章：1.2.1系统建模
系统建模是研究系统的基础,本节主要内容如下: 系统方程与框图系统建模的主要思路如下: 下面我们分别展示一下这两种方法微分方程与差分方程对于连续的系统,我们往往使用微分方程,而对于离散的系统,我们 ...
matlab and操作,系统建模 | Control Tutorials for Matlab and Simulink
介绍:系统建模设计控制体统的第一步是通过自然规律或者实验数据建立适当的数学模型.我们会引进状态空间和传递函数来代表系统.然后我们回顾一些基本的机械或者电力系统模型,并且会在MATLAB中展示怎么近一 ...
无穷大功率电源matlab仿真,MATLAB-Simulink系统建模与仿真-实验报告
MATLAB/Simulink 电力系统建模与仿真实验报告姓名: ****** 专业:电气工程及其自动化班级: ******************* 学号:****************** ...
matlab设置非平坦结构元,详解MATLAB/Simulink通信系统建模与仿真图书信息
第1章 Simulink基础 1.1 Simulink简介 1.2 运行Simulink演示程序 1.2.1 运行房屋热力学系统演示模型 1.2.2 房屋热力学系统模型说明 1.2.3 其他Simul ...
matlab库存点仿真教程,基于MATLABSimulink库存系统建模与仿真.doc
基于MATLABSimulink库存系统建模与仿真基于MATLABSimulink库存系统建模与仿真摘要:库存系统是管理系统中最普遍的一种,在库存系统中要通过不同的需求情况,确定何时订货和定多少货 ...
迪捷软件团队研发的国产替代MBSE系统建模仿真软件
近年来,系统工程的概念越来越火热.其中MBSE(基于模型的系统工程)是最受大家推崇的.在复杂系统和安全关键的开发领域,如果你不能说出一些跟MBSE有关的一些词儿,那么你是无法号称自己站在时代前沿的. ...
系统建模、分析、仿真和验证软件工具ModelCodoer
在安全关键领域,基于模型的软件工程已逐渐进入了我国的装备研制过程中.使用SimuLink或者SCADE等嵌入式软件建模工具进行可视化建模,然后生成高可靠的二进制代码逐渐成为了安全关键领域的主流软件开发 ...
作者：司光亚（1967-），男，国防大学信息作战与指挥训练教研部教授，主要研究方向为战争复杂系统建模仿真。...
司光亚(1967-),男,国防大学信息作战与指挥训练教研部教授.总工程师,主要研究方向为战争复杂系统建模仿真.
作者：吴琳（1974-），男，博士，国防大学信息作战与指挥训练教研部教授，主要研究方向为复杂系统与网络、战争复杂系统建模。...
吴琳(1974-),男,博士,国防大学信息作战与指挥训练教研部教授.博士生导师,主要研究方向为复杂系统与网络.战争复杂系统建模.

用Maude对MIU系统建模