synchronous - UPPAAL中的模型检查同步电路

Question

我正在使用 UPPAAL 模型检查器在门级对同步电路进行建模，我对如何对时钟建模有些困惑，我的目标是验证不违反建立时间和保持时间。我发现一些模型在 appal 模型检查器中将时钟作为测试向量，例如 at=10 相当于上升沿，而 at=20 是下降沿，这使它看起来更像一个测试向量。任何人都可以提出一个关于如何在 UPAAL 中模拟同步电路的基本示例吗？

谢谢

Answer 1

在声明中这样写：

clock t;
broadcast chan rise, fall;

那么 Uppaal 中的同步时钟将如下所示：

然后其他连接的组件应该在边缘上监听rise?并作为同步。fall?