UPPAAL SMC 避免状态空间爆炸答案

【问题标题】：UPPAAL SMC avoid State Space ExplosionUPPAAL SMC 避免状态空间爆炸
【发布时间】：2019-05-02 11:29:13
【问题描述】：

我正在尝试使用 UPPAAL SMC 查询更大的系统，结果显示“内存已耗尽”错误消息。从本质上讲，UPPAAL SMC 不应该导致状态空间爆炸，这就是为什么我要问是否可以在不发生状态空间爆炸的情况下使用 SMC 进行查询。

如果我尝试在很多状态下执行以下操作：

UppaalSystem system = engine.getSystem(document, problems);
engine.query(system, "", "E[<=100; 100](max: sum(i : id_t) Device(i).edge1)", queryListener);

我收到以下错误消息：

<html>Memory exhausted. See <br>http://bugsy.grid.aau.dk/bugzilla3/show_bug.cgi?id=63 <br>for more information.</html>

at com.uppaal.engine.Engine.getSystem(Engine.java:352)

是否可以在不调用内存密集型 engine.getSystem() 的情况下查询 Uppaal SMC？

Here is the uppaal model of my "device" template

【问题讨论】：

getSystem 将文档编译成模型——没有这一步它什么也做不了。可能是您的模型使用了许多数组或模板实例，这些实例在实例化时基本上会耗尽内存，或者可能是内存泄漏的一些错误（我很想知道）。您的 query 声明有问题：缺少结束引号。
@mariusm 当然，最后的引号不见了——我在帖子中编辑了它。我用几个测试用例尝试了编译任务（getSystem），但是有超过 20 个模板实例化我得到内存耗尽的错误消息。我会将我的“设备”模板上传到上面的问题中。
20 个进程并不多，我会更加怀疑数组，尤其是多维数组。范围是多少？你能分享你的模型文件吗？
我在这里上传了我的 uppaal 系统：ufile.io/iax8aj30 我用两个模板自动生成了这个系统，因为我想证明模型检查可以在实时环境中提供帮助（例如，云/边缘计算） . “生成器”模拟随机工作负载。这正在使用小示例进行工作和测试，但是如果示例达到示例 uppaal 中所示的大小，则会引发内存耗尽错误。非常感谢你。我真的很欣赏它。
瓶颈在Generator进程：它对20个布尔变量使用select语句，生成2^20=1048576条边，每条边占用一些内存（需要检查多少），但它似乎它的倍数超过了 4GB。如果只使用 SMC，那么使用随机函数枚举所有可能性会更有效，例如：uint32_t n = fint(random(1<<DEVICE_SIZE));，然后填充数组，例如：for (i:id_t) test[i] = (n >> i) & 1;

标签： model-checking state-space uppaal

【解决方案1】：

问题出在不同的模板中：瓶颈在于生成 2^20 = 1048576 条边的 select 语句。

对于 SMC，最好使用随机函数在一条边上生成所有可能性：

其中 randomInit 如下所示：

typedef int[0,(1<<DEVICE_SIZE)-1] uint20_t;

void randomInit(bool& test[DEVICE_SIZE])
{
    uint20_t number = fint(random(1<<DEVICE_SIZE));
    for (i: id_t)
       test[i] = (number >> i) & 1;
}

请注意，由于使用了random 和fint，E<> 和 A[] 等符号查询将无法在此类模型上运行！

【讨论】：

感谢您的帮助@mariusm。几个月前我尝试了 fint() （参见 stackoverflow.com/questions/54460545/…），但很高兴这个功能从 UPPAAL 版本 4.1.22 开始就可以使用。我喜欢通过左右按位移位生成随机数的资源效率。在您的专业帮助下，我的原型已准备好分别进行评估以进行进一步改进。 :-)