问题标签 [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.
validation - 使用 UPPAAL 或 NuSMV 控制电梯
我是 NuSMV 和 UPPAAL 的新手，正在解决这个问题。任何人都可以提供以下问题的解决方案吗？
对您自己设计的电梯系统的控制系统进行建模和分析，该电梯系统
服务于多个楼层（例如 4 或 5 个）并具有
多个 liX（例如 2 或 3 个），并且多个用户位于
各个楼层并具有个人希望凝胶到不同的
楼层。系统可以：
• 允许用户可以指示在某个楼层需要 liX，
和/或需要上或下和/或被要求去
某个楼层
• 或者用户可以 -- 一旦进入liX -- 请求实际楼层。
• 为了移动门必须关闭。• 不能跳过楼层。• 所有liX 的初始位置是1 楼。 a 电梯
仅由一个按钮控制，通过该按钮可以命令电梯到您所在的楼层。
out-of-memory - 在 UPPAAL 中实例化模板
我正在使用基本门在 UPPAAL 中制作电路。为此，我在系统声明中实例化这些门以制作所需的电路。我在参数部分声明了门的 I/O，然后在系统声明中使用所需的 I/O 变量实例化这些参数值，以制作特定的电路。
假设我想从 2 Xor,2 And, 1 Or gate 做全加器。当我运行模拟时，任何一个门随机启动而不遵循电路顺序，即一段时间或先模拟，第二个异或先模拟。为了避免这种情况，我声明了一些通信通道和一些变量，并将这些通道和变量添加到参数部分，以便以固定序列模拟门。但是在添加通道和变量之后，我遇到了错误-“内存耗尽”。
在模型检查器 Nusmv 中，如果我们在主模块中实例化较小的模块，我们还可以在实例化的同时在 main 中编写一些代码，这样可以最大限度地减少模块实例化中的变量数量。我们可以在乌帕尔做类似的事情吗？有没有办法将一个模板实例化为另一个模板。或任何从基本门制作电路而不会出现内存错误或使用最少参数的提示。我是否采用正确的技术从较小的电路制作大电路。我使用了基于 GUI 的 uppaal。感谢您的时间和帮助
deadlock - UPPAAL 僵局不明确
我正在使用 UPPAAL，我正在尝试为一家鞋厂建模，其中 5 个系统并行运行。如果有人需要，我可以写得更详细，但我不想通过描述模型来浪费任何人的时间。直截了当地解决问题：UPPAAL 死锁状态
在链接中的图片上，自动机无法进行红色过渡。转换的唯一标准是 p >= 4，但正如我所标记的，这应该没问题，因为 p = 21。那么为什么它不能进行过渡呢？您可以在以下链接中找到源代码： https ://drive.google.com/open?id= 1zuige_JBTPA7kZJPwE5cocWCzY6eh8UL 非常感谢任何帮助！
我对死锁的原因特别感兴趣，以及为什么无法进行转换，即使我试图强制转换（对不起，但我没有上传图片的级别:()
Edit1： 由于有些人声称代码不可访问，所以我将粘贴 UPPAAL 的 2 个文件，如下所示：hf_elso_1.xml：
在下面您可以找到我为系统检查创建的查询：
hf_elso_1.q：
model-checking - UPPAAL：检查数组成员
是否可以检查对象是否是 UPPAAL 中数组的元素？
如果我有一个整数数组
我想在验证器中做一个查询，我有类似的东西：
此外，UPPAAL 中是否有字符串类型或字符类型？
提前致谢！
model-checking - 查找 UPPAAL 中的状态和转换总数
我有很大的 UPPAAL 模型。我想分析模型中的状态和转换总数。有什么办法可以找出这些东西。
谢谢和问候
uppaal - UPPAAL：作为函数参数给出的时钟是否具有方法或属性？
我目前正在使用 UPPAAL v.4.1.19 并在帮助中看到可以将时钟作为函数参数给出。但是我找不到有关哪些方法或属性的任何信息，例如。时钟的下限和上限，可用于时钟。
示例函数：
是否有可能获得时钟的下限或在函数中用它做其他事情？
modeling - UPPAAL 中是否存在终止状态？
如何在 UPPAAL 中创建“终止”状态？如果某个状态没有边，则执行将因死锁而停止。如果状态有一个没有任何保护的循环，则执行永远不会停止。在没有死锁（如果有）的情况下停止模拟器执行的最佳方法是什么？
automaton - 我如何在 UPPAAL 中重置我的自动机
我在 UPPAAL 模型检查工具中创建了一些自动机，它们之间有一个对话框。当其中一个发生错误时，必须重置另一个。我不能将所有节点的返回边都放到起始节点，因为我不能为所有可能的错误设置警卫。有没有办法用一个函数或类似的东西来重置自动机？我们可以不通过边去不同的节点吗？我的意思是直接从一个节点跳转到初始节点而不使用边缘。谢谢你！
model-checking - 模型检查中探索状态与使用内存之间的关系
在模型检查中，状态和使用的内存之间可能存在什么关系。我们是否可以在将模型（状态空间）实际实施到模型检查器之前估计它可能使用的总内存。我们可以在实际实现之前粗略估计最小可能的内存吗？除了转换和状态之外，内存利用率取决于哪个因素。
谢谢你
function - Uppaal 模板参数
我正在使用 UPPAAL 4.1.19 并且我正在关注本教程中给出的火车教程。在训练模板中，我将参数放入int[0,N] e, const int id我声明的系统声明Train1=Train(el, 1);中，系统返回“不兼容的参数”错误e1。我不明白为什么它实际上不兼容？我已经N在全局声明中声明了一个等于 5 的常量，以及el，但它似乎仍然不起作用。任何想法？