saving learning queries as a file

[Szpilman2]

Dear UPPAAL team,

Hello! I'm interested in saving my learning strategy as a file, but it seems that the saved file doesn't adhere to the strategy file template. Could you please guide me on how to properly save my learning strategy?

Strategy file for strategy teststra = control: A<> m.sofLoc2 is :
ControllerStrategy.json

Strategy file for strategy myStrategy = minE(energy) [<=200] : <> m.sofLoc2 under teststra is:
LearningStrategy.json

as you can see the ControllerStrategy.json file has not structure of ControllerStrategy.json.

Thank you.

[thorulf4]

I think you accidentally uploaded the same file twice as the 2 attachments are the same, but I'll assume that was just a mistake.

But it seems to be working as intended, as we don't expect all strategies to be saved in the same format. Broadly speaking we have two categories of strategies synthesized strategies and learning strategies. These two strategies are stored in different formats I assume that is where your confusion comes from.
Both of these strategy types can be saved and loaded using the saveStrategy or loadStrategy syntax

Synthesized strategies

So symbolic queries like:
control: A<> ...
control: A[] ...
Synthesized strategies are saved in a custom non Json format.

Learning strategies

So queries like:
minE(cost) ...
maxE(reward) ...
Learning strategies are stored in json

[Szpilman2]

Thank you so much. My apologies for the confusion; the files in question are: (I also updated my original question)
ControllerStrategy.json
LearningStrategy.json

also my uppaal model is:

I believe my question might have been a bit unclear. My concern is that the content in "LearningStrategy.json" doesn't seem to constitute a strategy when compared to "ControllerStrategy.json."

in other words I think the content of LearningStrategy.json is not a strategy. and structure of files (they are json formatted or not) is not my concern.

Thank you very much.

[thorulf4]

Ah thanks for clarifying your question! But your concern is correct, your LearningStrategy.json has not learnt anything. Which happens because the error location was never reached during learning. As you're using an exact guard, which means your error state will only be reached when a delay of exactly 5 is chosen which is almost impossibly unlikely

To fix this I would rewrite the error bound using a guard and a urgent channel, which makes 5 an upper bound where a decision must be made (Red area). That way we get to use rate of exponential which has better semantics for your use case. To handle the case where a delay less than 1 I add a Delay action (Blue area).

// Place global declarations here.
urgent broadcast chan ASAP;
clock x, energy;

Also your liveness strategy may also prune all but one action which will also make training produce empty strategies.

[Szpilman2]

Thank you very much for your reply. I have a couple of inquiries:

1. Could you explain the purpose of incorporating the "ASAP" channel in this specific context? Essentially, why is this channel included in the transition? Additionally where should I put "ASAP?" in the model?

2. While the invariant in the initial location (sofLoc1) is 5 (x <= 5), I'm having trouble discerning the precise delay value in the blue area. Based on your previous statement, it appears to be 1, but could you clarify this (that how can i change this to five without getting empty strategy, in other words I would like to have x<=5 as invariant and the upper bound for invariant is fixed.)?

3. Additionally, I believe the energy should be represented by a "hybrid clock" in this scenario. Is my understanding correct?

Thanks a lot.

[thorulf4]

1. ASAP is a channel marked as an urgent which means we cannot delay while the transition is available. Which means we can't delay past 5 as the edge becomes available at x>=5. This will effectively impose a x<=5 invariant ASAP is a channel declared with urgent broadcast chan ASAP; and it is used in the synchronization field on the edge. Documenation on urgent channels
2. This model does not have a specific delay, it uses Rate of Exponential which picks a delay randomly with an exponential distribution where small delays are more likely. This does actually break the x<=5 invariant. If you prefer you can keep the invariant if you're okay with having constrained delays. In this example I use the clock y to force the delay to be 1 time unit
   
3. I'm not entirely sure if you need hybrid clock here. I think It depends what exactly you need to use the model for

[Szpilman2]

Thank you for taking the time to address my question; I highly value your insights and appreciate your assistance.

I think my question was not clear enough so I would like to explain it again. Regarding my scenario, I have two automata, labeled m and n. Automaton m comprises two states, sofLoc1 and sofLoc2. In sofLoc1, we can wait for a maximum of 5 time units (as an invariant). Upon the clock value surpassing 1, a transition to sofLoc2 (the goal state) can be taken. automata m and n are synchronized through use channel. Additionally, there is an automaton to monitor the energy consumption, where automaton n represents specific hardware with each state consuming a certain amount of energy (3 units in this case). in other words energy = 3 * t where t is the time parameter.

While I successfully modeled this scenario, attempting to verify the property minE(energy) [<=10] : <> m.sofLoc2 in UPPAAL resulted in a "time lock error." (visit this) In search of a solution, I came across a fix suggesting the introduction of an error state. I implemented this fix, specifying that when the clock value reaches 5, it should transition to the error state with a controllable transition with guard x==5. However, this led to another time lock error. Subsequently, I changed the controllable transition to uncontrollable, resolving the time lock error but resulting in an empty strategy when attempting to find a strategy for minE(energy) [<=10] : <> m.sofLoc2.

Now, I am seeking guidance on how to address this issue (how to modify automata to get valid strategy). I think modifying the guard from x==5 to x>=5 or removing the x==5 condition, might resolve the problem and yield a valid strategy (non-empty). I've reviewed your previous responses, and while I understand that adding exponential time delay may not be applicable in my scenario, Could you please provide assistance in resolving this matter?

[thorulf4]

Okay, I hope I understand the question better now. I think you get an empty strategy because there is only 1 possible action for the strategy to choose i.e there is only one controllable edge. If you want the strategy to decide if to take the softLoc1 --> softLoc2 transition or delaying you need to make a controllable transition specifically for delaying.