问题标签 [uppaal]

我Uppaal用于系统验证。模拟运行得非常好，但是当我使用这个属性进行验证时，A[] not deadlock它给了我以下错误：

那里可能出了什么问题？

我正在运行 Train Gate 示例，并且我想运行验证属性

Pr[<=100] (<> Train(0).Cross)以100 个时间单位表示Train(0)交叉的
概率是多少。

我已将时钟添加到安全状态，如附件所示。

通过运行上面给出的属性，它给了我以下错误；

Location Train(1).Safe [ Train(0).x=19.641971035860478878021240234375 Train(1).x=4.758311911486089229583740234375 Train(2).x=19.416877078358083963394165039062 Train(3).x=19.25746748410165309906005859375 Train(4).x=19.96133429370820522308349609375 Train( 5).x=19.875009718351066112518310546875 #time=20.623387750703841447830200195312 ] Gate.list[0]=4 Gate.list 1 =5 Gate.list[2]=0 Gate.list[3]=2 Gate.list[4]=3 Gate .list[5]=0 Gate.list[6]=0 Gate.len=5 与转换 Train(1).Cross->Train(1).Safe { x >= 3, leave[id]! , 1 } Gate.Occ->Gate.Free { 1 == front(), leave 1 ?, dequeue() }

在倒数第二行中，它说“通过过渡违反了模型健全性”。我一直在寻找（谷歌搜索）这个错误，但到目前为止没有运气，有人可以帮我解决它。

谢谢！

我创建了这个 UPPAAL 规范：https ://pastebin.com/v4AkYUuy

但是在运行查询时：

我得到错误：

我已经搜索了几个小时，但 UPPAAL 没有很好的文档。

人 汽车 火车

我正在验证一个非常小的模型。但我收到内存耗尽消息。我多次更改模型但遇到同样的问题。我认为这个问题是由于使用用户定义的函数或使用选择选项来获取随机数。然后我改变了模型，没有调用函数，也没有使用选择选项，但仍然......我想知道这是 UPPAAL 的问题还是在我的模型中。除了内存耗尽之外没有错误。一旦在该 ctl 属性不起作用后更改了“r1”和“r2”的值。 CTL 适用于增量之前的所有 r1 和 r2 值。

我试图在 UPPAAL 函数中返回一个整数数组。正确的语法是什么？

此代码段不起作用：

如何在 uppaal 中将双精度值转换为整数值？

根据 API 文档（http://www.it.uu.se/research/group/darts/uppaal/help.php?file=System_Descriptions/Expressions.shtml）以下功能可用，但它不起作用：

我正在努力进行一些简单的验证。我有这样的自动机和值 x：

自动机2

当开始处的 x 与 0 不同时，满足 E<> x !=0，但当 x = 0 时，则不满足，满足 E<> x == 0 和 A<> x == 0。但我想对 E<> x !=0 不满意，即使 x 在开始时与 0 不同。

我应该改变什么？验证器是如何工作的？空路径，什么都不执行的时候也是正确的路径吗？所有可能路径的集合也包含这个空路径吗？

所以我试图在我的模型上运行一个非常简单的验证，但是我收到一条消息说属性不满意。

我正在尝试在我的模型中验证是否 Person(0)In最终会出现 Person(0) Out。

人(0).In --> 人(0).Out

即使我在模拟器中手动检查了所有可能性，但我无法获得任何反例来验证（理论上应该满足这个条件）。

我使用的语法是否存在问题，或者 UPPAAL 是否存在此类验证的已知问题？

我正在尝试在 uppaal 中对 ATM 系统进行建模，并且我想使用 json 数组，例如用于 card_ID 和 pin 号的数据库，如下所示： [ { id : 12548, pin: 1244 }] 这可能吗？

我是uppaal的新手。我有一个由不同模型组成的系统。我还声明了一个时钟和一个双变量。

对于我的不变量和守卫，我需要检查这两个值（时钟 t；双 y；不变量：t<=y 或守卫 t==y 或 ty）。

现在在模拟的时候，我有这个错误

这个州的继任者没有很好的定义。SymbolicState:clock: Model.t -> double

我不知道我做错了什么。