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()
?
The issue is in the different template: the bottleneck is with the select statement which generates 2^20 = 1048576 edges.
For SMC it is better to use random function to generate all possibilities on one edge:
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
!