Invalid_argument exception: index out of bounds

[senniraf]

Hi,

I tried to synthesize parameters for the property and PTA in this .zip archive. I get the following error:

 ***************************************************************
 *  IMITATOR 3.2 "Cheese Blueberries"                          *
 *                                                             *
 *                                       Étienne André et al.  *
 *                                                2009 - 2021  *
 *                          LSV, ENS de Cachan & CNRS, France  *
 *                   LIPN, Université Paris 13 & CNRS, France  *
 *  Université de Lorraine, CNRS, Inria, LORIA, Nancy, France  *
 *                                            www.imitator.fr  *
 *                                                             *
 *                                         Build: ?????/?????  *
 *                        Build date: 2021-11-10 12:40:59 UTC  *
 ***************************************************************
 This model is an L/U-PTA:
 - lower-bound parameters {rho_a_geq_2}
 - upper-bound parameters {rho_d_leq_2, rho_c_leq_1}
 Model: `/relaxer/res/models/Double-Path-3-relax.imi`
 Algorithm: safety synthesis
 Merging technique of [AFS13] enabled.
 Starting running algorithm AG…
 
 Computing post^1 from 1 state.
 *** ERROR: `Invalid_argument` exception: `index out of bounds`
 Please (politely) insult the developers.
 *** ERROR: IMITATOR aborted (after 0.002 second)

I'm using the official docker image from docker hub (imitator/imitator:latest). This is also my first time using imitator, so there might be something wrong with the PTA or property file (although I got no syntax errors).

[DylanMarinho]

Dear @senniraf ,

In the property file, you are using the clock x. However, a clock cannot be used in a discrete expression (cf. user manual): only discrete and location predicates are allowed.

I suggest you to modify the model to create a location unreach reachable from A when x>7 and perform your analysis on this new location: if unreach is reachable, A was reachable with x>7.

I enclose you the two files with this modification (but I encourage you to check that this is what you were expecting):
Double-Path-3-relax.imiprop.txt
Double-Path-3-relax.imi.txt

[senniraf]

Thanks for the support. It works now!

Best,
Raffael

[etienneandre]

Thank you Raffael for your interest, and our apologies for not answering earlier! (and many thanks Dylan for answering)
I confirm Dylan's diagnosis and solution.

However, I reopen the issue as the "please insult the developers" error message means there is a bug here, that we need to fix.
Thanks a lot for raising this.