问题标签 [jpf]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
java - 在eclipse和ClassNotFoundException中设置jpf
我正在尝试使 java 路径查找器与我的测试示例一起使用，由于某种原因，使用来自 eclipse 的验证插件似乎不起作用，我正在使用 then run-JPF 方法。JPF 似乎工作，直到我尝试使用一些外部类，如：gov.nasa.jpf.jvm.Verify 他似乎没有找到。我已经尝试将它添加到 run 方法的类路径中，但我仍然遇到同样的问题，我该怎么办？
java - Java Path finder：如何通过命令终端访问它？
我是 Java 新手。我必须检测 java (KLOC) 程序中的错误。为此，我正在使用 Java Path finder。我通过命令行运行它cmd。使用命令
我想知道，我该怎么做：
- 获取比赛条件
- 检测死锁
- 验证控制
- 验证控制 JPF，搜索
- 检查数字扩展名
全部在命令行中？如果可以使用示例回答上述问题，那将非常有帮助。
谢谢
java - How to bypass null pointer exception?#JPF
I am trying to run JPF and encountered a following null pointer exception.
The code that is corresponds to is:
java - 无法运行 jpf 命令：JPF 异常，终止：错误读取类 java.lang.reflect.AnnotatedElement
当我尝试运行 jpf basset 程序时出现以下错误。我能够成功构建 jpf-core 和 jpf-actor。有没有人遇到过这个？我错过了什么吗？感谢您的回复/评论。谢谢。
java - 如何在netbeans中运行JPF。？
我已完成以下所有步骤
- 下载并安装 jpf-core，例如从 Mercurial 存储库
- - - - - - - - 休息一下 - - - - - - - -
- 从这里下载 gov-nasa-jpf-netbeans-runjpf.nbm 文件。
- 从 Netbeans 中转到 Tools->Plugins ( Alt+T后跟Alt+ g)
- 选择已下载选项卡
- 单击添加插件...（Alt+ A）
- 选择在步骤 3 中下载的 gov-nasa-jpf-netbeans-runjpf.nbm 文件
- 选择安装
- 同意许可协议
- 重新启动 Netbeans
现在我必须做什么来运行这个项目？
java - Java 路径查找器 NumericValueChecker
我正在尝试学习 Java 路径查找器 (JPF)。我下载了 JPF 并构建了它。目前我有jpf-core文件夹，其中包含示例 .java 文件及其相应的 .jpf 文件。我的目标是创建一个新的基本 .java 文件并检查此文件中的特定值是否超过了我在 .jpf 文件中指定的最大界限。
在示例文件夹中有一个名为 NumericValueCheck.java 的 .java 文件，这正是我想要的，它按预期工作。（查找值何时超出界限）
NumericValueCheck.java
NumericValueCheck.jpf
但是，我创建了一个新的 .java 文件并将其命名为“ BasicCheck.java ”。这是里面的代码；
这是BasicCheck.jpf中的属性；
javac BasicCheck.java我在一个单独的目录中编译了 BasicCheck.java 。然后我将“BasicCheck.java”和“BasicCheck.jpf”复制到jpf-core 的示例文件夹，其中 NumericValueCheck.java 和 NumericValueCheck.jpf 也在同一个地方。我还将“BasicCheck.class”复制到jpf-core/build/examples“NumericValueCheck.class”也在同一个地方的目录。
但是，当我运行命令时java -jar build/RunJPF.jar src/examples/BasicCheck.jpf，它找不到任何错误。结果是“未检测到错误”。它应该检测到大于上限 60 的 110。
为什么它不起作用？我需要在我的新 BasicCheck.java 或 BasicCheck.jpf 中添加一些额外的东西吗？
提前致谢。
java - JPF 符号字符串未生成预期 PC 的 [Java 路径查找器]
我正在尝试在符号字符串上运行 Jpf，但它没有生成预期的输出。以下是我正在尝试的玩具程序。
.jpf 文件如下：
在嵌套的 if 条件中，我正在打印字符串比较的值，只有当字符串 s1,s2 不等于 s3 时，才应该打印打印语句。我还使用 symbolic.debug=true 打印了 PC
以下是我有疑问的输出片段。这里的输出表明 s1,s2 同时与 s3 相等且不相等。这怎么可能？打印语句也显示“s2.equals(s3)=true”，那么程序不应该进入 if 块。
当我使用 int 而不是 String 时，代码可以工作。如果你能帮助我，那就太好了。如果我的 jpf 配置中缺少某些内容，请告诉我。先感谢您
java - JPF 模拟给出索引数组边界的错误
当我将自己的训练模型提供给 cmd 行 Python 文件时，我使用 Neurospf 模拟，将 NN 转换为 Java 文件中的命令式代码，而不是使用 eclipse 运行代码，然后基本上给出数组绑定索引错误 internal.biases0[k] 不运行 for循环 K=3 但是当我给 K=0 或 1 运行并花很多时间任何人都知道要修复它时。
