Specifying clock rates on array of clocks using forall and imply results in SIGSEGV

[GameMonkey]

Describe the bug I have an array of clocks where I, on a location, want to specify rates for the clocks using forall and imply. The invariant is on the form (forall (id : task_t) id != active imply worked[id]' == 0). Here, worked is the array of clocks.

When the engine loads the model it results in a segmentation fault.

To Reproduce Steps to reproduce the behavior:

1. Open the model MinExampleError.zip
2. Press F5 or run the model directly via verifyta.

Expected behavior That all clocks but one have a rate of 0.

Version(s) of UPPAAL tested UPPAAL 5.0.0 (rev. 714BA9DB36F49691), 2023-06-21

Desktop (please complete the following information):

• Kubuntu 23.10, Linux laptop 6.5.0-25-generic
• openjdk 17.0.10 2024-01-16,

[mikucionisaau]

I guess the issue is that imply is actually a disjunction in disguise, which is not allowed to be combined with clock expressions, but you found a way to trigger it anyway.

Can you use the following instead?

forall (id : task_t) 
    worked[id]' == (id == active)

This is just a workaround, and at this point I am not sure if implication can be used to manipulate the derivatives conditionally. If we allow it, it's very easy to mess up with multiple derivative definitions and checking for that is going to be non-trivial/expensive, so it's likely to be fixed with an error message that implication is not allowed in the invariant, just like disjunctions over clocks expressions are not allowed.

[GameMonkey]

Yes, that expression actually gives me what I am after, thanks!

In my opinion, imply should not be allowed to define clock rates as there is more than one solution to the expression.

Nonetheless, an error message would still be better than a segfault.