Error when running AT51 benchmark

[Abdu-Hekal]

The AT51 benchmark defined as follows: globally(implies((x(3)>1) & next((x(3)<=1),0),next(globally(x(3)<=1,interval(0,2.5)),0)). produces the following error:

Index exceeds the number of array elements. Index must not exceed 2751. Error in falsifyFixedModel>robustnessTemporalLogic (line 440) r = r(index); alpha = alpha(index);

Note I have simplified the benchmark by using knowledge that 1 is the lowest gear, replacing with e.g. x(3) > 1 & x(3) <=1 ends up in the optimization problem solved for each reachset which takes too long

[KochdumperNiklas]

I think it should by finally instead of next according to the Remarks in Table 1in https://easychair.org/publications/open/fRB5

[Abdu-Hekal]

Interesting, I have been following the implementation in the repo here which defines it as next. However, they may be internally dealing with it differently. In any case, finally here seems to be a (slightly relaxed) interpretation of next.

I have replaced the next operator with finally accordingly so that the stl is now: globally(implies((x(3)>1) & finally((x(3)<=1),interval(0.001,0.1)),finally(globally(x(3)<=1,interval(0,2.5)),interval(0.001,0.1)))

I get a similar error as before but now in the OR section:

Index exceeds the number of array elements. Index must not exceed 2991. Error in falsifyFixedModel>robustnessTemporalLogic (line 421) if r1(i) > r2(i)

[KochdumperNiklas]

There were indeed some errors in my code. I pushed a fix which hopefully solves the problem. One issue also was that the final time for the simulation was too short. So basically for a specification with nested temporal operators like globally(finally(x(1)<1,interval(0,2.5),interval(0,30)) we require a simulation with final time > 32.5 since the times of the temporal operators add up. We also could determine the required final time directly from the specification (we already have code for that).