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 attachment 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.