0

我正在尝试使用 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)

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

这是我的“设备”模板的 uppaal 模型

4

1 回答 1

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;
}

请注意，由于使用了E<>和！A[]randomfint

于 2019-05-03T10:00:21.217 回答