UPPAAL; RAM and processor capacity

[Hannes]

Hello,

I have modelled a system with UPPAAL. This system has around:
- 36 INT variables [0..10]
- 50 BOOL variables
- 9 INT constants
- 1 Time variable
- 6 broadcast channels, with an array [0..5]
- 2 broadcast channels, with an array [0..41]
- 60 Templates, which are interconnected over synchronizations

I have tried to verify some properties, but due to the size of the system, the state explosion problem shows its effects and
the verification took quite long. I let it run over night, for about 17 hours. It got then stuck with >170.000.000 states in the past waiting list. From there on, I had to cancel the verification (see attachment). I assume, that my RAM or processor capacity is not enough. My PC has:
- 11th Gen Intel(R) Core(TM) i7-11850H @ 2.50GHz   2.50 GHz processors
- 31,7 GB RAM

So I have two questions:
- Is here really the capacity of my PC the problem?
- If yes, does anybody has a rough estimation, which capacity would be necessary for those size of system?

I would really appreciate any help (as you might see, that I am a beginner with UPPAAL). Thank you very much!

Regards,
Hannes

[Marius Mikučionis]

Hello,

On Sunday 3 November 2024 at 12:13:33 UTC+1 Hannes wrote:

Hello,

I have modelled a system with UPPAAL. This system has around:

Your model is probably generating a huge state space. See some worst-case estimates below.

 

- 36 INT variables [0..10]

10^36 = ~ 1e36

 

- 50 BOOL variables

2^50 = ~ 1e15

 

- 9 INT constants

Constants do not occupy significant space.

 

- 1 Time variable

It depends how the clock is used, how many guards and invariants are there.

Most often a clock is involved only in a handful of guards and invariants with concrete constants, then this clock would contribute that much of a factor.

 

- 6 broadcast channels, with an array [0..5]

Channels do not occupy any space, but may help reducing the state space.

 

- 2 broadcast channels, with an array [0..41]

Broadcast channels are especially good at reducing parallelism.

 

- 60 Templates, which are interconnected over synchronizations

Estimate the number locations per process, say 10 and raise that number to the power of 60, which is 1e60.

 

I have tried to verify some properties, but due to the size of the system, the state explosion problem shows its effects and
the verification took quite long. I let it run over night, for about 17 hours. It got then stuck with >170.000.000 states in the past waiting list. From there on, I had to cancel the verification (see attachment). I assume, that my RAM or processor capacity is not enough. My PC has:
- 11th Gen Intel(R) Core(TM) i7-11850H @ 2.50GHz   2.50 GHz processors
- 31,7 GB RAM

So I have two questions:
- Is here really the capacity of my PC the problem?
- If yes, does anybody has a rough estimation, which capacity would be necessary for those size of system?

Yes, but as you can see it is easy to define a problem which is just too hard for any practical computer.

For example, combine all of the numbers above:

1e36 * 1e15 * 1e60 = 1e111

Note that this is just an estimate, the actual number can be much much smaller.

Some common features exploding the state space:

1) processes are asynchronous, communicate through shared variables instead of synchronizing over channels. Some behavior can be reduced by atomic execution through committed locations limiting interleaving. Use channel synchronization to reduce parallel behavior.

2) many non-deterministic choices resulting in many distinct variable values.

3) many details in data variables. Remove variables by introducing non-deterministic choice. Use active variable reduction and reset unused variables, make them const (active clock reduction is already done by UPPAAL, so clocks do not need to be reset). Variables used only in communication can be marked as meta.

4) systems with many clocks may benefit from a more compact state space representation.

5) some odd state space shape may be explored faster by using a different order of exploration.

6) some state space can be explored faster in parts by defining progress measure (sweep line method)

 

I would really appreciate any help (as you might see, that I am a beginner with UPPAAL). Thank you very much!

Make sure to read UPPAAL tutorial, also the documentation behind suggested features as they might behave in unexpected ways.

Best regards,
Marius