UPPAAL SMC 避免状态 Space 爆炸

Question

我正在尝试使用 UPPAAL SMC 查询更大的系统，但它以 "memory exhausted" 错误消息结束。从本质上讲，UPPAAL SMC 不应导致状态 space 爆炸，这就是为什么我问是否可以在不获得状态 space 爆炸的情况下使用 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 SMCengine.getSystem()？

Here is the uppaal model of my "device" template

Answer 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[] 等符号查询将不适用于此类模型

UPPAAL SMC 避免状态 Space 爆炸

UPPAAL SMC avoid State Space Explosion

model-checking

state-space

uppaal