Unexpected behaviour

[Leonardo Liparulo]

Good morning everyone, i am new to UPPAAL and i am struggling in understanding the behaviour during simulations of an University project: i do not understand why at the end the last enemies on the map don't go to the final states. Is it because of the loops of what i consider the final states? the reason why i created them was to avoid deadlock. please help me. i will share both the xml and the homework.

[Marius Mikučionis]

Hi,

Thanks for the model, I see that it triggers a few GUI bugs!

On Monday, 19 May 2025 at 08:34:54 UTC+2 leol...@gmail.com wrote:

Good morning everyone, i am new to UPPAAL and i am struggling in understanding the behaviour during simulations of an University project: i do not understand why at the end the last enemies on the map don't go to the final states. Is it because of the loops of what i consider the final states? the reason why i created them was to avoid deadlock. please help me. i will share both the xml and the homework.

I am not sure about the situation you are in, but I found a peculiar state (the symbolic trace attached) where enemy4 cannot make a transition to Dead:

 - The transition is grayed out as disabled in the "Enabled Transition" list.

 - When attempting to execute it, the simulator issues  "Internal Error" with "Can't find resource for bundle java.util.PropertyResourceBundle, key badSuccessorNotice.Message"

So this "Internal Error" is a bug where the simulator fails to translate the error into a meaningful message, I am sorry about that, I created a report here.

"badSuccessorNotice" tells me that the state this transition leads to is "bad" in a sense that it violates the target state invariant.

Normally such transitions are simply omitted as formally they are  not part of the transition system (because the invariant of the target state is not satisfied), 

but the simulator still displays them to the user, because it is often a symptom of a modeling error (the model is still accepted, because the model is still formally valid and some users specifically choose to use the target locations to remove unwanted transitions).

In your model such invalid transition is obscured by the fact that the violated target invariant sits at a different process than the transition is taken (one has to examine all locations, not just enemy4) -- I take it as a sign that such behavior was not intended.

So in this case enemy4 transition leading to Dead also has an update `numEnemyInMap--` (also obscured by a poor layout), which brings numEnemyInMap from 1 to 0, which in itself is OK (because numEnemyInMap is simply a signed integer), but then other processes like tur1, tur2, tur3, tur5 and tur6 have an invariant `numEnemyInMap>0` which becomes false and thus disables the transition.

So I hope it explains the behavior of your model. 

If you have a different situation, please attach a symbolic trace so we could examine it closely.

When debugging your model I found the following query useful to generate counter-example traces:

E<> ((enemy1.Dead or enemy1.LeaveMap) + (enemy2.Dead or enemy2.LeaveMap) + (enemy3.Dead or enemy3.LeaveMap) + (enemy4.Dead or enemy4.LeaveMap) + (enemy5.Dead or enemy5.LeaveMap) + (enemy6.Dead or enemy6.LeaveMap)) == 4

With "Options" > "Search Order" > "Random depth first"  and "Options" > "Diagnostic Trace" > "Some" it generates a trace in a second, but then the following property takes a very long while:

E<> ((enemy1.Dead or enemy1.LeaveMap) + (enemy2.Dead or enemy2.LeaveMap) + (enemy3.Dead or enemy3.LeaveMap) + (enemy4.Dead or enemy4.LeaveMap) + (enemy5.Dead or enemy5.LeaveMap) + (enemy6.Dead or enemy6.LeaveMap)) == 5

meaning that it is likely false, which indicates the existence of a counter, and then discovering a violated invariant on that counter.

Best regards,

Marius

[Leonardo Liparulo]

thank you very much, i think i was able to fix that also because of you precious help. I have a new problem right now thought, that can sound silly but i am not really able to solve. How can i generate multiple instances of an enemy without doing it manually for each one? one of the task of the homework is to test the system with 700 enemies, but i don't really want to create them manually if i can avoid that. is there some way of declaring them all in once? thank you

[Marius Mikučionis]

On Monday, 26 May 2025 at 19:49:10 UTC+2 leol...@gmail.com wrote:

thank you very much, i think i was able to fix that also because of you precious help. I have a new problem right now thought, that can sound silly but i am not really able to solve. How can i generate multiple instances of an enemy without doing it manually for each one? one of the task of the homework is to test the system with 700 enemies, but i don't really want to create them manually if i can avoid that. is there some way of declaring them all in once? thank you

Please look at template instantiation: 
https://docs.uppaal.org/language-reference/system-description/system-definition/template-instantiation/

700 is a lot, perhaps you can do some symmetry reduction, see scalar types: 
https://docs.uppaal.org/language-reference/system-description/declarations/types/#scalars