UPPAAL SMC избежать государственного космического взрыва - PullRequest
Новая
       57

UPPAAL SMC избежать государственного космического взрыва

0 голосов
/ 02 мая 2019

Я пытаюсь запросить более крупную систему с помощью 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 моего шаблона "устройства"

1 Ответ

0 голосов
/ 03 мая 2019

Проблема в другом шаблоне: узкое место связано с оператором выбора, который генерирует 2 ^ 20 = 1048576 ребер.

exponential explosion of edges

Для SMCлучше использовать случайную функцию для генерации всех возможностей на одном ребре:

enter image description here

, где 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[], не будут работать на таких моделях из-за использования random и fint!

...