用Maude对MIU系统建模

MIU 系统简介

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

1. T1“appendU”规则，若当前的 合法字符串以“I”结尾，则可以在其 尾部追加一个字母“U”。例如串“MUI” 可以利用 T1 规则转化为“MUIU”。
2. T2“appendDouble”规则，若当 前的合法字符串的首字母是“M”，则 可以在其尾部追加当前字符串除了首 字母的子串。例如串“MUI”可以利用 T2 规则转化为“MUIUI”。
3. T3“deleteI”规则，若当前的合 法字符串中包含连续的三个“I”，则 去除此连续的三个“I”，余下的字符
   串首尾相接合成新串。例如串“MIIIU” 可以利用 T3 规则转化为“MU”。
4. 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的。

完整代码

完整代码