Search code examples
model-checkingstate-spaceuppaal

UPPAAL SMC avoid State Space Explosion

I am trying to query a larger system with UPPAAL SMC and it ends up with a "memory exhausted" error message. By nature, UPPAAL SMC should not result in a state space explosion that's why I am asking if it is possible to query with SMC without getting a state space explosion.

If i try to execute the following with a lots of states:

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

I get following error message:

<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)

Is it possible to query Uppaal SMC without calling the memory intensive engine.getSystem()?

Here is the uppaal model of my "device" template

Solution

  • The issue is in the different template: the bottleneck is with the select statement which generates 2^20 = 1048576 edges.

    exponential explosion of edges

    For SMC it is better to use random function to generate all possibilities on one edge:

    enter image description here

    where randomInit looks like the following:

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

    Note that symbolic queries like E<> and A[] will not work on such models due to the use of random and fint!