Why doesn't UPPAAL try to take all the paths?

[Lqs66]

I have added a global variable declaration to my model int g.
Then I executed the model in the simulator and I noticed that it always executes along a fixed path.

I found that uninitialized variables are always initialized to 0 by default, which does not match my understanding. Why doesn't the model checker try to traverse all the paths without assigning a random value for g?

[mikucionisaau]

Uppaal initializes all variables with 0 unless it has a special range or initializer.
That's because integer variables are treated as part of a discrete state, it does not have an abstract interpretation engine.
Also such treatment would automatically result in much bigger state spaces than most people expect.

If you want a non-deterministic initalization, then you need to model it with non-deterministic edges.

[Lqs66]

Uppaal initializes all variables with 0 unless it has a special range or initializer. That's because integer variables are treated as part of a discrete state, it does not have an abstract interpretation engine. Also such treatment would automatically result in much bigger state spaces than most people expect.

If you want a non-deterministic initalization, then you need to model it with non-deterministic edges.

Thank you for your reply.