问题标签 [pvs]

我想将以下 PVS 翻译成 Coq：

其中类型trans的类型为env -> env -> bool，我编写 Coq 代码如下：

但是，我不知道在 Coq中表示Exists (s : env) 。这个定义的目标是存在一个满足 (P s1 s) 和 (P s s2) 的值s 。我不想使用逻辑，因为我想证明以下定理：

如果我手动运行以下命令，它会返回正确的结果。但是，如果我从 crontab 运行它，它会引发下面提到的错误。

命令：

错误：

LVM_SUPPRESSED_FD_WARNINGS=1不能解决这个问题。

我一直在研究和测试 Quake II 能见度的阅读和使用。在多次尝试实现它之后，我还没有完全管理它。否则，我主要基于这篇文章，另一篇关于 Blogger的文章，并浏览了有关该主题的更多文档，我什至深入研究了 Quake II 源代码本身，但我不太明白哪里出了问题。

在可视化我的 PVS 时，我发现无论我使用什么解包算法，它似乎总是只突出显示随机叶子，通常是被更近的叶子隐藏的叶子，这使得它们不可见。有时我最终会得到应该清晰可见但不可见的叶子。

从文件中反序列化 vis 数据是我的第一个也是唯一一个可检测到的错误：我最初读取偏移量并分别分配位向量。我后来发现 PVS/PHS 偏移量在偏移量中考虑了它们自己。我最终诉诸于逐字读取和分配可见块，使偏移量指向正确的位置。

我对第二季度 PVS 拆包的收获是

• 它是可见簇的行程编码位图
  • 0 表示下一个字节是要跳过多少簇并将其标记为隐藏
  • 否则我们直接从位向量映射（给定到目前为止我们用 RLE 字节累积的偏移量）

至于集群，我构建了一个集群数组，作为一组叶子，当被索引时，为每个集群条目提供一个叶子的链表。

到目前为止，这一切都说得通，对吧？我应该能够：读取 vis 数据，为给定集群解压缩，从给定其自己的集群的叶子的解压缩 PVS 中获取可见集群列表

到目前为止，这不起作用！我对解决方案不知所措。我不知道该怎么办。是否有一些我不了解的概念，我的思路和分析中的一些疏忽？

作为参考，我正在对 quake2 的 base1.bsp 和一些简单区域的自定义导出进行测试。我会发布代码，但我有许可问题和很多需要清理的东西......对不起！