文章/答案/技术大牛

发布

社区首页 >问答首页 >UPPAAL SMC避免状态空间爆炸

问UPPAAL SMC避免状态空间爆炸
EN

Stack Overflow用户

提问于 2019-05-02 19:29:13

回答 1查看 218关注 0票数 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)

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

Here is the uppaal model of my "device" template

model-checking

state-space

uppaal

回答 1

Stack Overflow用户

回答已采纳

发布于 2019-05-03 18:00:21

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

对于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[]这样的符号查询将不能在这些模型上工作！

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/55951475

复制

相似问题

问UPPAAL SMC避免状态空间爆炸
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问UPPAAL SMC避免状态空间爆炸EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问UPPAAL SMC避免状态空间爆炸
EN