如何在java中实现MCI解析器

Question

我想解析mci文件格式，以便在java中存储petri展开前缀，这样我就可以使用它生成SAT公式。

本文描述了用于存储Petri网展开前缀的MCI文件格式。

在下面，char是一个1字节的字符，而UINT4是一个小的endian(即最小的有效字节位于最低的地址，而其他的字节是按重要性的顺序递增的)4字节的无符号int (Intel是小endian)。

• 条件总数(UINT4)
• 事件总数(UINT4)
• 对于每个事件(从第一次到最后一次)：--原始转换的数目(UINT4)
• 对于每个条件(从第一个到最后一个)：--原始位置(UINT4)的数目--预设事件(UINT4)的数目；如果条件为初始值-空(UINT4)后集事件号(UINT4)的-terminated列表，则为0。
• 对于每个关闭事件--关闭事件的数量(UINT4) --对应事件的数量(UINT4)或NULL(UINT4)，如果相应的事件是虚拟初始事件的话。
• 分离空(UINT4)
• 对于每个配置：-NULL(UINT4)事件编号的-terminated列表。(这是一些古老的模型检查器使用的；PUNF不创建它，只输出终止空(UINT4))。
• 分离空(UINT4)
• 原始网(UINT4)中的总名额数。
• 原始网(UINT4)中的过渡总数
• 位置/转换名称(UINT4)的最大字符串长度(用于解析器中的内存分配)
• 对于原始网中的每个位置：--名称(NULL(CHAR)-terminated字符串)
• 分离空(UINT4)
• 对于原始网中的每个转换：--名称(NULL(CHAR)-terminated字符串)
• 终止NULL(UINT4)。

注意:我已经在C++中得到了实现，但我希望它在java中实现。想知道你的信息。我使用了这么多工具将其转换为java，但没有一种工具能完全工作。因此，我将感谢您guys.More的任何帮助，如果需要的话，我将把代码放在C++中。

Answer 1

我想你是在找DataInputStream。

这应该允许您读取您的个人uint4和字符。