TLA+工具链中Ant构建目标失败问题分析与解决

背景介绍

TLA+是一种用于形式化验证的规范语言，其Java工具链中包含多个Ant构建目标用于测试和验证。近期发现其中两个测试目标test-verify和test-dist-long出现了构建失败的情况，这反映了项目维护过程中常见的一个问题：缺乏持续集成的测试目标容易随着时间推移而失效。

问题分析

test-verify目标失败原因

test-verify目标执行时主要运行两个JPF(Java PathFinder)相关的测试用例：

1. OffHeapDiskFPSetJPFTest测试
2. StateQueueJPFTest测试

这两个测试都因相同的原因失败：JPF框架在初始化过程中抛出了NoClassDefFoundError异常，找不到sun/misc/SharedSecrets类。这实际上是Java版本兼容性问题，因为sun.misc.SharedSecrets是Sun/Oracle JDK的内部API，在新版Java中已被移除或重构。

test-dist-long目标失败原因

test-dist-long目标的失败更为直接，是由于编译错误导致的。错误信息显示：

1. 无法找到tlc2.tool.WorkerMonitor类
2. WorkerMonitor包不存在
3. 无法解析WorkerMonitor变量

这表明代码中引用的WorkerMonitor类已被移除或重构，但相应的测试代码未同步更新。

技术深度解析

JPF框架兼容性问题

Java PathFinder(JPF)是一个基于JVM的模型检查工具。它依赖于特定的JVM内部实现细节，如sun.misc包中的类。随着Java模块系统的引入和内部API的清理，这些依赖在新版Java中变得不可用。

解决方案可能包括：

1. 使用特定版本的Java(如Java 8)运行这些测试
2. 更新JPF版本以支持新版Java
3. 重写测试用例，避免依赖JPF

废弃API的清理问题

WorkerMonitor类的缺失反映了项目中API的演进。在大型项目中，测试代码需要与主代码保持同步，否则很容易出现这种编译时错误。这提示我们需要：

1. 建立更严格的测试覆盖机制
2. 在移除或重构API时同步更新测试代码
3. 考虑使用接口而非具体实现来减少测试的脆弱性

解决方案建议

针对这些问题，可以考虑以下解决方案：

1. 短期方案：为这些测试目标明确指定兼容的Java版本要求
2. 中期方案：更新或替换JPF依赖，使其支持新版Java
3. 长期方案：将这些测试纳入CI流程，防止类似问题再次发生
4. 代码重构：移除对已废弃API的依赖，或提供兼容层

项目维护启示

这一案例给开源项目维护提供了重要启示：

1. 未被CI覆盖的代码容易"腐化"
2. 依赖特定JVM实现的代码存在长期维护风险
3. 测试代码需要与主代码同等重视
4. 定期检查所有构建目标的健康状况很重要

对于TLA+这样的重要形式化工具，保持构建系统的全面健康对项目的长期可持续发展至关重要。