clock rate customization for each timed automaton in UPPAAL

[Szpilman2]

Dear UPPAAL Team,

I hope this message finds you well. I would like to inquire if it is possible to change the rate of clocks for each timed automaton individually. When modeling distributed systems, each component typically has its own clock with a specific rate. Could you please advise how I can set the clock rate for each automaton independently?

Thank you very much for your assistance.

Kind regards

[Szpilman2]

could you possibly help me?
thanks you so much.

[mikucionisaau]

There is no specific construct to cover such use-case, so it all has to be modeled.

The clock rates can be specified per location basis, so each location needs a derivative expression if the rate is not 1.

Alternatively, if the clocks are shared, then one can create an array of those clocks and array of rates, and then use forall expression on some extra automaton.

For example:

const int PN = 5; ///< number of processes
typedef int[1,PN] id_t; ///< process identifier
clock x[id_t]; ///< shared clocks, one per prcess
const int rate[id_t] = { 1,2,3,4,5 }; ///< clock rates, one per process, can be non-const

Template declaration:

template Template(clock& x) ///< clock is passed by reference

System declaration:

p(const id_t i) = Template(x[i]);
system p;

Then have this one invariant in some other process, perhaps with just one location:

forall(i : id_t) x[i]' == rate[i]

Note that rates other than 1 and 0 will work only with statistical (SMC) queries.