BoyerMoore算法Pluscal代码语法错误排查与执行方法咨询

一、字符到ASCII转换的语法错误修复 #

TLA+不会自动完成字符与ASCII值的映射，需显式处理才能避免“函数参数不在定义域内”的报错，具体修复方式如下：

1. 导入标准库模块
   在TLA+文件开头添加EXTENDS Ascii，该模块提供的CharToOrd函数可直接将标准ASCII字符转换为对应数值。

2. 替换字符引用方式
   所有需要用ASCII值作为函数/数组参数的字符，都要通过CharToOrd(c)显式转换。比如原代码中直接用字符作为badCharTable的索引，需改为：

badCharTable[CharToOrd(SubSeq(pattern, i+1, i+1))] := i;

3. 自定义字符映射（可选）
   若需处理非ASCII字符，可手动定义字符到数值的映射函数：

CustomCharToASCII == [c ∈ {'你', '好', ...} |-> 对应的Unicode或自定义数值]

之后在代码中调用该函数完成转换即可。

二、无需模型检查器的单次执行测试方式 #

TLA+提供两种直接运行代码的方式，无需启动模型检查器：

1. 命令行单次模拟 #

• 先将Pluscal代码编译为TLA+：在Toolbox中点击「Translate Pluscal to TLA+」，或用命令行工具pcal编译。
• 执行模拟命令：

tlc -simulate -depth 1000 YourSpec.tla

-depth指定模拟的最大步数，可根据算法执行需求调整数值。

2. Toolbox内置表达式求值功能 #

• 打开TLA+文件，点击顶部菜单栏「Tools」→「Evaluate Expression」。
• 输入要测试的表达式（如CharToOrd('a')或Boyer-Moore匹配函数的调用语句），点击「Evaluate」即可得到单次执行结果。

代码示例参考 #

修正后的Pluscal代码片段（字符转ASCII部分） #

EXTENDS Ascii, Integers

(*--algorithm BoyerMoore
variables
    text = "abcabcabc",
    pattern = "abc",
    badCharTable = [i ∈ 0..127 |-> -1],  // 覆盖标准ASCII范围
    m = Len(pattern),
    n = Len(text);

begin
    BuildBadChar:
        for i = 0 to m-1 do
            badCharTable[CharToOrd(SubSeq(pattern, i+1, i+1))] := i;
        end for;
    
    // 后续匹配逻辑...
end algorithm;*)

对照用Java参考代码 #

public class BoyerMoore {
    public static int search(String text, String pattern) {
        int n = text.length();
        int m = pattern.length();
        int[] badCharTable = new int[127];
        
        // 初始化坏字符表
        for (int i = 0; i < 127; i++) {
            badCharTable[i] = -1;
        }
        // 填充坏字符表
        for (int i = 0; i < m; i++) {
            badCharTable[(int) pattern.charAt(i)] = i;
        }
        
        int s = 0;
        while (s <= n - m) {
            int j = m - 1;
            while (j >= 0 && pattern.charAt(j) == text.charAt(s + j)) {
                j--;
            }
            if (j < 0) {
                return s; // 匹配成功，返回起始索引
            } else {
                s += Math.max(1, j - badCharTable[(int) text.charAt(s + j)]);
            }
        }
        return -1; // 无匹配
    }

    public static void main(String[] args) {
        System.out.println(search("abcabcabc", "abc")); // 输出0
    }
}

内容的提问来源于stack exchange，提问作者Mohan Radhakrishnan