Symbolic State satisfies double should never be called

[Szpilman2]

Dear UPPAAL team,

I hope this message finds you well.

I recently came across your paper titled An Introduction to Schedulability Analysis Using Timed Automata (page 108) and noticed that in the paper, you have treated the WCET (worst case execution time) as a natural number.

However, I was under the impression that WCET is a double. When I attempted to create a model with "double" clock bounds, UPPAAL returned an error message like this:

also my simple model is like this:

(in this case 1.5 (ms) is WCET)

could you possibly help me that how can I use double clock bounds in my guards? (or I may be mistaken in assuming that WCET is a double?)

thank you so much.
best regards.

[mikucionisaau]

The floating point types are supported only in concrete state engine and the symbolic (triggered by query E<>) does not support floating point types due to their dense value domain.

As you can see the paper refers to calligraphic N -- set of natural numbers, i.e. integers, and that's what timed automata assume.

Floating point numbers were added later to support performance analysis, where arbitrary operations a available and are beyond reachability decidability.

If you need to support fractions, then you can find a common denominator of all the constants and scale all of them to produce integer values everywhere.

[Szpilman2]

Thank you very much for your clear and excellent explanation.

Best regards