问题标签 [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.
uppaal - 在 Mac OS 中运行 Uppaal 4.1.22 的问题
我在 Mac OS 10.14 上下载并安装了 uppaal 4.1.22。我安装了 Java 8。
打开 uppaal.jar 时，会弹出一个窗口，显示“服务器退出并出现错误 126。检查操作系统。” 关闭窗口后，我无法运行模拟器或验证程序。事实上，当我选择模拟器或验证器时，会弹出相同的窗口。
我该如何解决这个问题？
uppaal - UPPAAL 中的多重同步
如何在 UPPAAL 中模拟多个同步？例如：状态变化在不同的模板中同时触发另外两个状态变化。在同步领域，我只能放一个通道（sync1！或sync！）。我怎样才能结合sync1！和同步2！?
谢谢
uppaal - 检查 Mac OS Catalina 10.15 上的 Uppaal 4.1.23 是否支持 OS 错误
我在 Mac OS 10.15 上安装了 Uppaal 4.1.23，但出现错误。我该怎么办？
uppaal - 找不到可能导致“由超出范围的分配或超出范围的数组查找引起”的原因。错误
当我尝试检查系统是否存在死锁时出现此错误：
验证因错误而中止。这很可能是由超出范围的分配或超出范围的数组查找引起的。
我明白这个错误应该是什么意思（感谢https://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Expressions.shtml），但我真的可以'找不到任何可能发生此问题的情况，并且无法通过玩模拟器来使其发生。我能想到的唯一可能导致这个问题的是我的数组之一，但从我所看到的情况来看，假设我从来没有做任何越界的事情似乎是安全的。
有没有办法找到任何线索来帮助我识别我的问题（更精确的错误、导致此问题的跟踪或类似的东西）？或者我错过了一个细节，这个错误可能是由其他原因引起的？
macos - 在 Mac OS 上安装 Uppaal
我正在尝试在我的 Mac 上安装 Uppaal。我已经安装了 Catalina，并且我知道此处发布的解决方法与授权有关，并且已经完成了此操作。
但是当我运行 Uppaal 脚本时，我收到一条错误消息
错误：无法访问 jarfile ./uppaal.jar
我无法弄清楚问题是什么或如何解决它。Java 是最新的。
请帮忙，我需要这个来完成大学作业
formal-verification - 无法验证 TCTL 属性？
我在 UPPAAL 4.1 版本中构建了这个模板。我们可以在图 1 中看到，存在代理可以执行反射处理的单一路径，但是当我编写给定属性时
E<> 不是（MonitorAgent.ReflexProcessing）
验证者满意。
它不应该满足，因为在 ReflexProcessing 完成的地方存在一条路径。请添加您的建议。在此处输入图像描述
uppaal - UPPAAL-生成一些策略
我已经使用 Uppaal Stratego 有一段时间了。我已经使用 verifyta cli 生成策略，并使用了 --print-strategies pathtoShowStrategy 文件等命令。现在我生成的策略是 416.56 Mb 的文本文件。
我使用 --generate-strategy O 来生成一些策略，并将打印结果保存在文件夹中。下面是我在cli中使用的。我的机器是 Linux 64 位（如果需要的话）
pathToVerifyta/verifyta --print-strategies 文件夹位置/ --generate-strategy 0 pathToModelLocation。
输出文本文件似乎与原始文件一样大，即文件大小相同。我还尝试反转 --print-strategies 和 --generate-strategy 但没有太大帮助。有人能帮帮我吗 ？
uppaal - UPPAAL - 关于频道相关属性的查询
我正在尝试创建使用通道的属性，例如，如果 X 通道信号被传输，那么这意味着 Y 通道应该发送信号作为响应，但是我在制作它时遇到了问题。它会产生一个错误，所以可能是我使用了错误的模板，请指导我应该使用的确切语法是什么。我尝试了 3 种不同的方法，但都失败了，它给出了“服务器异常：类型错误”。下面是我使用 THS 和 SP 表示通道的语法，THComponent 和 Cpacing 表示我的模板/模型。
1- A[ ] THS！暗示SP！
2- A[ ] THComponent.THS 暗示 Cpacing.SP
3- A[ ] THS 暗示 SP
你能指导我确切的语法是什么吗？
谢谢
variables - 如何保存在建模过程中创建的 Uppaal 变量
我用 Uppaal 创建了一个模型，其中几个整数变量随时间变化。现在我想在建模过程中将变量的值保存在某个地方（最好是 xml 或文本文件）。在 Uppaal 文档（https://www.it.uu.se/research/group/darts/uppaal/documentation.shtml）中，我找到了第 13 点中的方法（如何从 Uppaal 导出和解释痕迹？）和已经尝试过Java API方式，希望它可以输出变量以及跟踪。不幸的是，这种方法似乎仅限于跟踪。有谁知道从 Uppaal 保存变量值的方法？
希望的问候，
乔西