Alloy API调用TranslateAlloyToKodkod.execute_command抛出空指针异常

问题背景 #

使用Java版Alloy API实现Alloy模型编译、可视化展示、实例搜索范围缩小功能时，部分Alloy源码可正常执行，部分源码执行抛出NullPointerException，通过Eclipse调试API类内容无法定位问题。

异常表现 #

调用TranslateAlloyToKodkod.execute_command时触发java.lang.NullPointerException。

根因排查 #

官方文档标注该方法仅在选择"save to FILE"作为SAT求解器时返回null，你使用SAT4J求解器且Alloy原生分析器可正常求解两份测试代码，排除该场景。
实际触发原因有两个：

1. 代码未对execute_command的返回值做非空校验，一旦方法返回null，后续调用ans.satisfiable()直接触发空指针
2. 触发异常的Group模型包含高阶约束（使用set Element作为谓词参数），默认A4Options配置中skolemDepth参数为0，无法处理高阶约束，导致翻译阶段失败，execute_command直接返回null

修复方案 #

步骤1：修改A4Options配置，支持高阶约束 #

创建A4Options实例时，添加skolemDepth配置，自动处理高阶量词skolem化：

A4Options options = new A4Options();
options.solver = A4Options.SatSolver.SAT4J;
options.skolemDepth = -1; // 新增：自动适配高阶约束求解

步骤2：添加非空判断，兼容无满足解的场景 #

修改命令执行后的结果处理逻辑，增加返回值非空判断，避免空指针：

for (Command command: world.getAllCommands()) {
    System.out.println("=========== command : "+command+" ============");
    A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);
    // 新增：判断返回结果是否为空
    if (ans == null) {
        System.out.println("当前命令求解失败，跳过");
        continue;
    }
    System.out.println(ans);
    if (ans.satisfiable()) {
        int cnt = 1;
        A4Solution tmp = ans.next();
        // 新增：判断next返回结果是否为空
        while (tmp != null && tmp.satisfiable()) {
            tmp = tmp.next();
            cnt++;
        }
        System.out.println("=========== "+cnt+" 个可满足实例已找到 ============");
        tmp = ans;
        String[] outXml = new String[cnt];
        for ( int i = 0; i < cnt; i++ ) {
            outXml[i] = outputfilepath + "/" + out_fname + (i+1) + ".xml";
            tmp.writeXML(outXml[i]);
            tmp = tmp.next();
        }
    } else {
        System.out.println("当前命令无满足解，跳过实例导出");
    }
}

补充说明 #

地址簿示例可正常运行的原因是其没有高阶约束，默认配置即可完成翻译，不会触发返回null的场景。

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