I have described a very basic system generating a random number. When switching
to simulation (or verification), uppaal hangs. It seems that UPPAAL allocates a
lot of memory until no more memory is available in the system.
Thanks for your help,
Best regards,
L. Apvrille.
Spec is as follows (available also at the provided URL):
------ spec1.xml -------
<nta>
−
        <declaration>


//Global declarations
const int DEFAULT_INFINITE_SIZE = 1024;
int randomNb;

int min(int a, int b) {
if (a<b) {
return a;
} else {
return b;
}
}

int max(int a, int b) {
if (a>b) {
return a;
} else {
return b;
}
}



int random(int a, int b) {
  return a + ((b - a) * randomNb / (200001));
}


chan rd__ch, wr__ch;
</declaration>
−
        <template>
<name>channel__ch</name>
−
        <location id="id0" x="-64" y="-80">
<name x="-80" y="-56">main_state</name>
</location>
<init ref="id0"/>
−
        <transition>
<source ref="id0"/>
<target ref="id0"/>
<label kind="synchronisation" x="-280" y="-88">wr__ch?</label>
<nail x="-208" y="-232"/>
<nail x="-208" y="104"/>
</transition>
−
        <transition>
<source ref="id0"/>
<target ref="id0"/>
<label kind="synchronisation" x="40" y="-88">rd__ch?</label>
<nail x="64" y="80"/>
<nail x="64" y="-232"/>
</transition>
</template>
−
        <template>
<name>T0_7</name>
<declaration>int x = 3;
int nb__rd;
int nb__wr;
</declaration>
<location id="id1" x="-48" y="-200"/>
−
        <location id="id2" x="-64" y="-280">
<name x="-24" y="-208">id1</name>
</location>
−
        <location id="id3" x="0" y="-136">
<name x="10" y="-131">id2</name>
</location>
−
        <location id="id4" x="0" y="-70">
<name x="10" y="-65">id3</name>
</location>
−
        <location id="id5" x="0" y="5">
<name x="10" y="10">id4</name>
</location>
<init ref="id2"/>
−
        <transition>
<source ref="id1"/>
<target ref="id3"/>
</transition>
−
        <transition>
<source ref="id2"/>
<target ref="id1"/>
<label kind="select" x="-104" y="-272">randomNb : int[0, 2000000000]</label>
<label kind="assignment" x="-88" y="-248">x = random(4, 5)</label>
</transition>
−
        <transition>
<source ref="id3"/>
<target ref="id4"/>
<label kind="assignment" x="10" y="-107">nb__wr = x</label>
</transition>
−
        <transition>
<source ref="id4"/>
<target ref="id4"/>
<label kind="guard" x="0" y="-90">nb__wr>0</label>
<label kind="synchronisation" x="5" y="-80">wr__ch!</label>
<label kind="assignment" x="10" y="-70">nb__wr = nb__wr - 1</label>
<nail x="-30" y="-100"/>
<nail x="30" y="-100"/>
</transition>
−
        <transition>
<source ref="id4"/>
<target ref="id5"/>
<label kind="guard" x="0" y="-52">nb__wr==0</label>
</transition>
</template>
−
        <system>

//Instanciation 
channel__ch__0 = channel__ch();
T0_7__1 = T0_7();
system channel__ch__0,T0_7__1;
</system>
</nta>

I could not reproduce the bug. The simulation and the verifier work well. The
URL was wrong so maybe it is another example. I found spec.xml, not spec1.xml.
Which version of java are you using?

You have to use spec1.xml (on not spec.xml) linked by the provided URL. Our web
server refreshes its page only a few times per day, so, it will probably be
accessible during the afternoon.
The Java version I use is 1.6.0_01-b06

Created an attachment (id=206) [details]
faulty spec

The faulty spec is now attached on the page

When you are using the select statement in UPPAAL, the transitions are
generated when the system is instantiated. It is a shortcut. In your case you
are asking for 2 billion transitions, do not be surprised that you have a
problem with memory.

Then you do not need to declare min & max functions. UPPAAL provides these
expressions: a <? b and a >? b that return respectively the min & max.

There is another problem in your model that is not reported by UPPAAL, namely
you have your randomNb global and you use it in select. This will have no
effect on the variable because the select variable shadows the global variable.
There should be at least a warning about this.

Thanks for your help.
Ok, if I understand, the select option is only a shortcut for transitions, i.e.
it should be used only with close boundaries.
My concern was in fact to be able to generate a random number between two
non-static boundaries (e.g., y = random(x, z + 10)). Is there another solution
to do this? Indeed, the C stdlib rand() function is not supported. Moreover,
how could I settle non-uniform random function (gaussian, or else)?
Thanks also for your remarks on the min() and max() function. Actually, the
UPPAAL code is automatically generated from a UML Toolkit (named TTool), and
the UML diagrams of that toolkit support min() and max functions. Thus, if I
want to use, for example "a <? b", I need to identify this in all integer
expressions and modify them accordingly -> defining min() and max() functions
is much simpler in my case.

The select statement can be used for random assignments like this:
in select: tmp:int[2,10]
in update: a = tmp

UPPAAL is a model-checker and does not support random distributions, all the
values will be generated and all the states explored.

I'm keeping this bug to add a warning in case you mis-use the select statement
as you did by doing "a : int[..]" directly with a global variable.

Well, I don't really agree on random numbers. The proof is that UPPAAL supports
a select facility to ease the modeling of random numbers with static
boundaries. Modeling random numbers with non-static boundaries is also possible
by simply:
(Let's assume you want x = rand(y, z), with z greater then y.
1) You use a state s1 with two outgoing transitions t1 and t2
2) t2 is guarded with [y < z + 1] and goes from s1 to s2.
3) action of t2 is x = y; and then, the next system continues from S2.
4) t1 is guarded with [y < z]. The action is y = y + 1. t1 reloops to s1.

That way, you may model an non-efficient random number generator. I say
"non-efficient" because, at simulation, the first value is more likely to be
selected than other values, etc.. The model-checker should of course work fine
with that approach.

So, adding a random number is clearly compatible with model-checking. Also, my
solution does not provoke memory shortage on the model since only one state and
two transitions are added. So ... a macro for random number generation - with
non-static boundaries - should be possible!

UPPAAL does not support dynamic types in select, you're right. You cannot use
tmp:int[a,b] unless a and b are evaluable at compile time.
What you can do is to have the select range over min(a) max(b) and add the
guard
tmp >= a && tmp <= b to your transition. You will get a "random" value between
a and b.

Select statements that shadow variable declarations are now reported as
warnings.
Fixed in trunk & 4.0.
Dynamic select is a wished feature.

There are several open bugs on select.
Please open a new one if you want the feature of select over dynamic types.