Find minimum value in learning queries

[Szpilman2]

Dear UPPAAL team,

I trust this message reaches you in good spirits.

I've developed a model comprising two components: software and hardware. (Attached below are their respective images.)
Software Model:

Hardware Model:

Using the strategy minStra = minE(energy) [<=250] : <> software.End , I've successfully generated a minimum strategy. However, I'm unsure of how to determine the smallest value of energy within the minStra strategy. Could you please provide guidance on this matter?
In other words, I'm seeking clarification on which query to employ to obtain the minimum value of energy when my model reaches the state software.End under minStra strategy? (energy is hybrid clock)

I've also attached my model in here:
OptEngModel_final.zip

Thank you for your assistance.
Best regards,
Peyman

[mikucionisaau]

Try value estimation under the strategy:

E[<=250; 100] (max:energy) under minStra

max: records the maximum value of energy over individual run.
Since energy is monotonically increasing then max:energy will correspond to its last observed value in the run.

Alternatively inspect the energy trajectories:

simulate[<=250; 100]{ energy } under minStra

I would also suggest to add observation expressions to your learning query. For your current query without observable part of the state UPPAAL will treat as if entire state is observable, which is usually unrealistic and it also drowns the signal with a lot of noise in the learning statistics.

[Szpilman2]

Thank you very much for your help. From what I understand, the strategy file provides information about the Q-values. However, I'm uncertain how to determine which of the halves to take based on this file. In other words, how can I use this file to decide whether to proceed from software.start to software.p1 or software.p5?

"(0)":
			{"type":"act->point->val","representation":"simpletree","minimize":1,"regressor":
				{
				"15" : 27.64160000000001,
				"7" : 27.76080077402224
				}
			},

I think this part of strategy will help to answer this question. because in the beginning energy == 0 and this part tells us that taking "15":"software.start->software.p1 { 1, tau, 1 }" is the best choice because the Q-value is less than other. am I right?

I would greatly appreciate your assistance in clarifying this matter.

Thank you once again for your support.

[mikucionisaau]

In this particular case, the strategy does not really differentiate between "15" and "7", i.e. both actions are almost as good (I don't think there is statistically significant difference).
If you follow the numbers, then it says pick the smaller one, i.e. "15".

[Szpilman2]

Dear Marius,

Hello, I hope this message finds you well,

Previously, I set the energy' in each location of the hardware TA to be equal to the Power variable, which is defined as an integer with a value of 4 ([int Power = 4]). Now, I want to assign different energy consumption rates for each location in the hardware TA. Specifically, I want the following rates:

• state: Active --> energy' == 6
• state: Power Saving --> energy' == 1
• state: Tail --> energy' == 18
• state: Using --> energy' == 14

However, I'm unsure how to achieve this with the Power variable. I think I might need an array of power values. You previously mentioned that for learning to occur, the Power value in the software TA needs to be set to a large number. But with these new requirements (different energy rates in each hardware TA location), I'm not sure how to adjust my model. Could you please guide me on how to implement this?

Thank you very much.

[mikucionisaau]

Simply use the power variable in the derivative expression and then the value of the power variable can be adjusted on the incoming edges. Uppaal does not really care about the derivative expression as long as it can compute it. Then I presume the energy variable is going to be used in the minimization learning query and the automaton location (or power variable) to be used in the observable feature part of the query.

The energy variable needs to be declared as hybrid clock in order to use symbolic (A[], E<> etc) queries.