问题标签 [uppaal]
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.
integer - 如何使用 int fint (double) 将双精度值转换为整数，而不会在 Uppaal 中出现“服务器连接丢失”
我想将双精度值转换为整数以在模型的保护中使用它们。为此，我在https://www.it.uu.se/research/group/darts/uppaal/找到了int fint (double)函数download.shtml，现在我使用 uppaal-4.1.24 而不是 uppaal-4.1.19。不幸的是，当我尝试在其中一个模拟器或验证器中执行相应的转换时，我总是收到消息“服务器连接丢失” 。有没有人遇到过类似的问题并知道解决方案？
最好的问候，乔西
java - UPPAAL：Java API 的 ModelDemo（获取内存信息时出错：34，javax.xml.stream.XMLStreamException：ParseError at [row,col]:[1,3]）
我试图让 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 会返回以下日志：
它似乎运行得很好，但最后遇到了错误。（获取内存信息时出错：34）
不幸的是，在预先存在的文件上运行 ModelDemo.java 中的 main 总是会返回一些 xml 解析错误。我已经在使用 Gui 自己创建的文件和演示文件夹中提供的示例上尝试了这个：
（javax.xml.stream.XMLStreamException: ParseError at [row,col]:[1,3] 消息：文档类型声明包含或指向的标记声明必须格式正确。）
任何帮助将不胜感激。提前致谢！
formal-verification - Uppaal - 当条件变为真时如何强制转换？
我希望能够在条件变为真后立即强制转换。
例如，在此示例中，我想在全局变量a变为5时强制从下一个系统从状态S0转换到S1。守卫是不够的，因为在触发转换之前 a 达到 5 后仍然可以递增。我真的需要触发过渡，然后继续增加a。
有没有简单的方法来做到这一点？我尝试在状态中添加不变量，但它会造成死锁。
model-checking - Uppaal - 通道同步 - 在评估警卫之前更新值
我想做以下事情：
最初，我的变量x设置为 0，并且由于防护，此转换不可能触发。我希望能够将 x 的值更新为 1，然后检查b的转换保护以进行同步。我了解 Uppaal 首先进行转换（因此首先检查警卫），然后进行发送者的更新，然后是接收者的更新。
我发现解决此问题的唯一解决方案是使用已提交状态，如下所示：
我首先更新x然后进行同步。
它工作正常，但我想知道它是否存在更好的解决方案而不使用提交状态？
formal-verification - 如果属性不满足，UPPAAL 不会显示跟踪
我正在使用 UPPAAL 4.1.24 对一个由 1 个主进程和 3 个观察者进程组成的简单系统进行建模。主进程使用由观察者进程收听的广播频道。我已启用Options -> Diagnostic Trace -> Some.
现在，每次我通过验证程序的查询检查属性时，我都可以看到跟踪并在 Simulator 选项卡下的 Trace 框中重放它。但是，它仅适用于得到满足的属性。如果不满足查询给定的属性，则不会更新跟踪，并且我看不到该“未满足”属性的跟踪。
任何想法？
verification - UPPAAL 上的反例枚举
下午好，我正在用 UPPAAL 模型检查器做一些实验，我的理解是，当一个属性没有被验证时，验证引擎（verifyta）只能找到以下之一：
- 痕迹
- 最短轨迹（转换次数）
- Quickset Trace（具有最短相对时间的跟踪）。
这很有意义，如果我们认为模型检查关注的是健全性而不是完整性，并且至少存在一个违反特定属性的迹线这一事实意味着该属性不满足。
然而，在我的应用程序的上下文中，我需要找到多个反例来分析它们的结构等。在这个程度上，我想知道是否存在推断违反 TCTL 中定义的特定属性的所有可能跟踪的可能性，给定一个有界搜索空间（即限制搜索图的深度）。此外，如果 UPPAAL 不提供这个机会，您能否指出可能已经实现它的其他工具？
非常感谢！
arrays - 在 Uppaal 中从同一模板声明多个进程
有没有办法实例化从 Uppaal 中的同一个模板获得的多个进程？
例如，目前我写（在System declarations文件中）：
但是我想获得一个更紧凑的形式来这样做（也许成一个数组？），因为我实际上必须创建 50 个进程（而不仅仅是 4 个）。我怎样才能做到这一点？
注意：变量是类型的int[0,1]，我目前在Declarations文件中定义它们如下：
uppaal - 两个紧急位置导致的僵局
一个小例子在模拟过程中，我发现如果一个状态处于紧急位置，另一个状态即将到达紧急位置，就会死锁。而且我想验证时间的上下限，所以如果没有时间我必须设置紧急位置。我该如何解决这种情况？
uppaal - 有什么方法可以知道 uppaal 模型是否识别痕迹？
我正在尝试检查 uppaal 模型是否识别出痕迹。
我必须生成随机跟踪并检查另一个类似模型是否可以执行相同的跟踪。我可以通过使用带有查询的verifyta.exe来进行随机生成：
"模拟 [<= n ; 1] {时钟} "
但是，我不知道 Uppaal 或 Tron 或某些扩展是否能够检查模型是否实际上可以达到与输入相同的轨迹。我将不胜感激任何建议，无论是改变我生成痕迹的方式还是我希望模型识别痕迹的方式。
任何帮助将不胜感激：D