0

我试图让 ModelDemo.java 工作，因为我想使用 Java API。不幸的是，我遇到了错误......

我正在为 linux 使用 Eclipse IDE 版本 2020-06 (4.16.0)、openjdk 11.0.10 2021-01-19 和 uppaal64-4.1.24。我创建了一个包含 ModelDemo.java 文件的项目。我还在 Eclipse 中将 model.jar 和 uppaal.jar 作为外部 JAR 添加到项目的 Classpath 中。

使用 'hardcoded' 参数在 ModelDemo.java 中运行 main 会返回以下日志：

(L0, L0, v=0, x ? 0, y ? 0, z ? 0, x = y, x = z, y = z, )
Exp1: L0 ? L1, (L1, L0, v=1, x ? [0,10], y ? 0, z ? 0, x ? y, x ? z, y = z, )
Exp2: L0 ? L1, (L1, L1, v=1, x ? [0,10], y ? 0, z ? 0, x ? y, x ? z, y = z, )
Exp1: L1 ? L2, (L2, L1, v=2, x ? [5,10], y ? [0,5], z ? 5, x - y ? [5,10], x ? z, y - z ? -5, )
Exp2: L1 ? L2, (L2, L2, v=2, x ? [5,30], y ? [0,20], z ? 5, x - y ? [5,10], x ? z, y - z ? -5, )
Exp2: L2 ? L3, (L2, L3, v=3, x ? [15,30], y ? [10,20], z ? [0,10], x - y ? [5,10], x - z ? [15,30], y - z ? [10,20], )
Exp2: L3 ? L0, (L2, L0, v=4, x ? [15,30], y ? [10,20], z ? [0,10], x - y ? [5,10], x - z ? [15,30], y - z ? [10,20], )
Exp1: L2 ? L3, (L3, L0, v=3, x ? 15, y ? 10, z ? 0, x - y ? [5,10], x - z ? [15,30], y - z ? [10,20], )
Exp1: L3 ? Final, (Final, L0, v=5, x ? 15, y ? 10, z ? 0, x - y ? [5,10], x - z ? [15,30], y - z ? [10,20], )
deadlock
===== Simple check =====
Result: OK
===== SMC check =====
(401 runs) Pr(<> ...) in [0.424048,0.523972]
with confidence 0.95.

Result: OK: [0.424048,0.523972]
===== Custom check ===== 
Result: OK
===== Custom SMC ===== 
(393 runs) Pr(<> ...) in [0.375518,0.475494]
with confidence 0.95.

Result: OK: [0.375518,0.475494]
===== Custom Concrete Simulation ===== 
Result: OK
Plot "Simulations (1)" showing "value" over "time"
Trajectory v: (0.0,2.0) (30.1,2.0)
Trajectory x: (0.0,5.0) (30.1,35.1)
Trajectory y: (0.0,5.0) (30.1,35.1)
Error while getting memory info: 34Error while getting memory info: 34Error while getting memory info: 34

它似乎运行得很好，但最后遇到了错误。（获取内存信息时出错：34）

不幸的是，在预先存在的文件上运行 ModelDemo.java 中的 main 总是会返回一些 xml 解析错误。我已经在使用 Gui 自己创建的文件和演示文件夹中提供的示例上尝试了这个：

javax.xml.stream.XMLStreamException: ParseError at [row,col]:[1,3]
Message: The markup declarations contained or pointed to by the document type declaration must be well-formed.
    at java.xml/com.sun.org.apache.xerces.internal.impl.XMLStreamReaderImpl.next(XMLStreamReaderImpl.java:652)
    at java.xml/com.sun.xml.internal.stream.XMLEventReaderImpl.nextEvent(XMLEventReaderImpl.java:83)
    at com.uppaal.model.io2.XMLReader.next(XMLReader.java:98)
    at com.uppaal.model.io2.XMLReader.begin(XMLReader.java:109)
    at com.uppaal.model.io2.XMLReader.project(XMLReader.java:179)
    at com.uppaal.model.io2.XMLReader.parse(XMLReader.java:85)
    at com.uppaal.model.core2.PrototypeDocument.load(PrototypeDocument.java:235)
    at app.ModelDemo.loadModel(ModelDemo.java:209)
    at app.ModelDemo.main(ModelDemo.java:332)
java.io.IOException: ParseError at [row,col]:[1,3]
Message: The markup declarations contained or pointed to by the document type declaration must be well-formed.
    at com.uppaal.model.core2.PrototypeDocument.load(PrototypeDocument.java:271)
    at app.ModelDemo.loadModel(ModelDemo.java:209)
    at app.ModelDemo.main(ModelDemo.java:332)

（javax.xml.stream.XMLStreamException: ParseError at [row,col]:[1,3] 消息：文档类型声明包含或指向的标记声明必须格式正确。）

任何帮助将不胜感激。提前致谢！

4

1 回答 1

0 
Error while getting memory info: 34

这个错误似乎来自内存使用测量，很奇怪，但它应该是无害的。

javax.xml.stream.XMLStreamException: ParseError at [row,col]:[1,3] Message: The markup declarations contained or pointed to by the document type declaration must be well-formed.

与前两行的 DTD 定义有关。也许使用不同的 Uppaal 版本来创建 XML 文档。demo解决方案是从同一 Uppaal 版本的示例文档之一复制前两行。这不是一个有保证的解决方法（某些标签可能会丢失，或者解析器可能会卡在它不重新识别的特定标签上），但它可能只是工作。

于 2021-02-20T22:55:31.087 回答