1

我的问题是我可以在 Uppaal 中生成一个随机数吗？

我想从一系列值中生成一个数字。更重要的是，我想生成的不仅仅是整数，我还想生成双精度值。

例如：双 [7.25,18.3]

我发现这个问题在谈论同样的问题。我尝试过这个。但是，我收到此错误：语法错误意外 T_SELECT。

它不起作用。我是 Uppaal 世界的新手，如果您能提供任何帮助，我将不胜感激。

问候，

4

1 回答 1

3

这是 Uppaal 中一个常见且被误解的问题。

简单的回答：

    double val; // declaration
    val = random(18.3-7.25)+7.25; // use in update, works in SMC (Uppaal v4.1)

详细回答：

  1. Uppaal 支持符号分析和统计分析，处理方法和可能性完全不同。所以必须首先决定需要什么样的分析。通常从简单的符号分析开始，然后增加随机特征，有时还需要对随机行为进行符号检查。

  2. 在符号分析（查询A[]、A<>、E<>等E[]）中，随机是非确定性的同义词，即如果模型包含一些“随机”行为，那么验证应该以任何方式检查所有这些行为。因此，这种行为被建模为边缘之间的非确定性选择。通过在声明临时变量的边上使用 select 语句很容易在整数范围内设置一组边，其值可用于保护、同步和更新。符号分析仅支持整数数据类型（没有浮点类型，如double）和时钟上的连续范围（由保护和不变量中的约束指定）。

  3. 统计分析（通过蒙特卡洛模拟，查询，如，，，等Pr[...](<> p)）除了数据类型外，还支持类型和浮点函数，如，，，（均匀分布）等。时钟变量也可以被视为浮点类型，除了它们的导数默认设置为 1（可以在允许 ODE 的不变量中更改 - 常微分方程）。E[...](max: var)simulatedoublesincossqrtrandom(MAX)[0, MAX)random_normal(mean, dev)int

  4. random如果浮点变量不影响/约束模型行为，并且仅充当状态空间上的成本函数，则可以创建具有浮点运算（包括 ）的模型并仍然应用符号分析。以下是实现这一目标的系统规则：

    a) ODE 中使用的时钟必须声明为hybrid clock类型。

    b)hybrid clock并且double类型变量不能出现在保护和不变约束中。hybrid clock在不变量中的 s 上只允许 ODE 。

于 2016-06-14T07:47:59.627 回答