问题标签 [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.
synchronous - UPPAAL中的模型检查同步电路
我正在使用 UPPAAL 模型检查器在门级对同步电路进行建模，我对如何对时钟建模有些困惑，我的目标是验证不违反建立时间和保持时间。我发现一些模型在 appal 模型检查器中将时钟作为测试向量，例如 at=10 相当于上升沿，而 at=20 是下降沿，这使它看起来更像一个测试向量。任何人都可以提出一个关于如何在 UPAAL 中模拟同步电路的基本示例吗？
谢谢
java - Uppaal 错误：java.io.IOException：服务器连接丢失
我目前正在研究形式验证，我必须使用 uppaal，这是我的新手。但是如果我运行 uppaal 我得到一个错误
java.io.IOException：服务器连接丢失
有什么办法可以解决吗？我正在使用 ubuntu 16.04 和 openjdk8
我正在查看以下帖子
UPPAAL 错误 - java.io.IOException：服务器连接丢失
但我仍然无法找出解决方案
在这方面的任何帮助将不胜感激！
uppaal - 有没有办法为 UPPAAL 全局中的每个状态指定最长时间？
我想指定所有状态不应长于指定时间。我可以通过逐个州指定它来做到这一点，但人类可以忘记一个。我需要一个全球解决方案。我的意思是“每个州的最大时间”属性。
deadlock - 系统包含死锁 - 如何找到它？(UPPAAL)
我用 UPPAAL 建立了一个模型，并使用验证器检查死锁。答案是：物业不满意。因此存在死锁。
UPPAAL 中是否有办法报告有关死锁的更详细信息，例如特定情况下所有变量的状态和当前值？
formal-verification - UPPAAL 中的状态空间爆炸
我在 UPPAAL 中模拟了两个触发器的定时模型，当我尝试验证一些属性时，我达到了 6M 状态并且我的笔记本电脑内存不足，消耗了大约 5Go，谁能告诉它是 UPPAAL 可以的近似状态数处理 ？以及在 UPPAAL 中处理状态爆炸的可能技术是什么？
谢谢
formal-verification - UPPAAL 整数变量规范
有时在 UPPAAL 中，我发现了一个整数变量的示例，它采用两个值，例如 int x:=1-0，这到底是什么意思？像 x 先取“1”然后取“0”还是 X 只是两个值的数组？
谢谢
properties - 不是乌帕尔的大门
我在 uppaal 中建立了具有传播延迟的简单非门模型。但我无法证明一个属性。附上自动机的截图。Xinp 是输入，xout 是输出。3在这里用作传播延迟。
此属性工作正常，经过 3 个时间单位后，输出变为输入的否定。
这个属性应该是不可满足的，以便我可以验证非门在传播延迟之后和 3 个时间单位输出之前不是根据非门工作。但是这个属性并不是不能满足的。
谢谢
properties - 在 UPPAAL 中检查变量相对于时间的值
我想在属性“如果在时间 t 的输入为 0 并且在时间 t+1 的输入为 1 则系统重置将是 1 ”属性中写下这条语句我是这样写的，
xin(t)==0 && xin(t+1)==1 --> 重置==1。
但它显示错误“预期功能”。我怎样才能写一个函数。
谢谢
templates - UPPAAL 中的通道声明
当我在模板部分声明通道时，为什么 UPPAAL 编译器不会抛出错误？如果我做对了，没有其他模板可以访问这些通道，因此通道声明仅在整个声明部分中才有意义。还是我忽略了什么？
谢谢！
PS我想通过同步通道对“内部”模板通信进行建模，并希望在模板中声明一个通道可能是一种解决方案。上面的问题似乎更容易提出和回答:)